WEBVTT Kind: captions Language: en 00:00:00.030 --> 00:00:03.800 align:start position:0% hey<00:00:00.599> everyone<00:00:00.989> how's<00:00:01.550> it<00:00:02.550> going<00:00:02.850> they<00:00:03.570> already 00:00:03.800 --> 00:00:03.810 align:start position:0% hey everyone how's it going they already 00:00:03.810 --> 00:00:05.720 align:start position:0% hey everyone how's it going they already started<00:00:04.170> my<00:00:04.319> clock<00:00:04.680> so<00:00:04.890> I'm<00:00:05.040> just<00:00:05.220> gonna<00:00:05.370> start 00:00:05.720 --> 00:00:05.730 align:start position:0% started my clock so I'm just gonna start 00:00:05.730 --> 00:00:09.980 align:start position:0% started my clock so I'm just gonna start -<00:00:06.649> so<00:00:07.649> we<00:00:07.770> got<00:00:07.890> talk<00:00:08.700> today<00:00:08.849> about<00:00:08.940> CBC<00:00:09.630> Casper 00:00:09.980 --> 00:00:09.990 align:start position:0% - so we got talk today about CBC Casper 00:00:09.990 --> 00:00:12.259 align:start position:0% - so we got talk today about CBC Casper design<00:00:10.320> philosophy<00:00:11.160> it's<00:00:11.550> mostly<00:00:11.940> really 00:00:12.259 --> 00:00:12.269 align:start position:0% design philosophy it's mostly really 00:00:12.269 --> 00:00:15.919 align:start position:0% design philosophy it's mostly really about<00:00:12.599> design<00:00:13.219> methodology<00:00:14.690> and<00:00:15.690> I'm<00:00:15.809> gonna 00:00:15.919 --> 00:00:15.929 align:start position:0% about design methodology and I'm gonna 00:00:15.929 --> 00:00:18.890 align:start position:0% about design methodology and I'm gonna walk<00:00:16.139> you<00:00:16.379> through<00:00:16.800> some<00:00:17.130> of<00:00:17.190> the<00:00:17.869> stuff<00:00:18.869> that 00:00:18.890 --> 00:00:18.900 align:start position:0% walk you through some of the stuff that 00:00:18.900 --> 00:00:21.109 align:start position:0% walk you through some of the stuff that goes<00:00:19.050> on<00:00:19.260> in<00:00:19.320> CBC<00:00:19.770> Casper<00:00:20.189> land<00:00:20.400> in<00:00:20.640> terms<00:00:20.910> of 00:00:21.109 --> 00:00:21.119 align:start position:0% goes on in CBC Casper land in terms of 00:00:21.119 --> 00:00:23.420 align:start position:0% goes on in CBC Casper land in terms of the<00:00:21.390> methodology<00:00:22.199> that<00:00:22.529> we<00:00:22.680> use<00:00:22.949> to<00:00:23.130> develop 00:00:23.420 --> 00:00:23.430 align:start position:0% the methodology that we use to develop 00:00:23.430 --> 00:00:26.450 align:start position:0% the methodology that we use to develop and<00:00:24.199> define<00:00:25.199> distributed<00:00:25.800> systems<00:00:26.070> protocols 00:00:26.450 --> 00:00:26.460 align:start position:0% and define distributed systems protocols 00:00:26.460 --> 00:00:29.540 align:start position:0% and define distributed systems protocols I'm<00:00:27.300> gonna<00:00:27.810> talk<00:00:28.019> about<00:00:28.289> it<00:00:28.500> first<00:00:29.189> is<00:00:29.429> like 00:00:29.540 --> 00:00:29.550 align:start position:0% I'm gonna talk about it first is like 00:00:29.550 --> 00:00:31.550 align:start position:0% I'm gonna talk about it first is like what<00:00:29.880> is<00:00:30.029> carpi<00:00:30.779> construction<00:00:31.199> and<00:00:31.380> I'm<00:00:31.439> gonna 00:00:31.550 --> 00:00:31.560 align:start position:0% what is carpi construction and I'm gonna 00:00:31.560 --> 00:00:34.010 align:start position:0% what is carpi construction and I'm gonna talk<00:00:31.740> about<00:00:32.040> domain<00:00:32.669> theory<00:00:33.239> and<00:00:33.510> then<00:00:33.630> like 00:00:34.010 --> 00:00:34.020 align:start position:0% talk about domain theory and then like 00:00:34.020 --> 00:00:35.990 align:start position:0% talk about domain theory and then like this<00:00:34.260> kind<00:00:34.590> of<00:00:34.649> defined<00:00:35.160> in<00:00:35.309> this<00:00:35.460> stuff<00:00:35.790> it's 00:00:35.990 --> 00:00:36.000 align:start position:0% this kind of defined in this stuff it's 00:00:36.000 --> 00:00:37.910 align:start position:0% this kind of defined in this stuff it's gonna<00:00:36.120> be<00:00:36.329> kind<00:00:36.660> of<00:00:36.719> a<00:00:36.840> trip<00:00:37.079> it's<00:00:37.230> gonna<00:00:37.800> be 00:00:37.910 --> 00:00:37.920 align:start position:0% gonna be kind of a trip it's gonna be 00:00:37.920 --> 00:00:39.889 align:start position:0% gonna be kind of a trip it's gonna be pretty<00:00:38.040> cool<00:00:38.280> and<00:00:38.550> then<00:00:39.270> I'll<00:00:39.390> talk<00:00:39.570> and<00:00:39.840> I'll 00:00:39.889 --> 00:00:39.899 align:start position:0% pretty cool and then I'll talk and I'll 00:00:39.899 --> 00:00:41.660 align:start position:0% pretty cool and then I'll talk and I'll give<00:00:40.050> some<00:00:40.079> examples<00:00:40.230> are<00:00:40.649> like<00:00:40.739> actual<00:00:41.100> CBC 00:00:41.660 --> 00:00:41.670 align:start position:0% give some examples are like actual CBC 00:00:41.670 --> 00:00:45.260 align:start position:0% give some examples are like actual CBC design<00:00:42.090> in<00:00:42.360> CBC<00:00:42.750> Casper<00:00:43.110> and<00:00:43.340> some<00:00:44.340> of<00:00:44.460> the<00:00:44.610> you 00:00:45.260 --> 00:00:45.270 align:start position:0% design in CBC Casper and some of the you 00:00:45.270 --> 00:00:47.479 align:start position:0% design in CBC Casper and some of the you know<00:00:45.469> stuff<00:00:46.469> that<00:00:46.500> happens<00:00:47.070> and<00:00:47.250> to<00:00:47.309> give<00:00:47.430> you 00:00:47.479 --> 00:00:47.489 align:start position:0% know stuff that happens and to give you 00:00:47.489 --> 00:00:50.990 align:start position:0% know stuff that happens and to give you a<00:00:47.550> kind<00:00:47.700> of<00:00:47.730> a<00:00:47.820> taste<00:00:48.059> of<00:00:48.680> the<00:00:49.760> methodology<00:00:50.760> and 00:00:50.990 --> 00:00:51.000 align:start position:0% a kind of a taste of the methodology and 00:00:51.000 --> 00:00:52.240 align:start position:0% a kind of a taste of the methodology and [Music] 00:00:52.240 --> 00:00:52.250 align:start position:0% [Music] 00:00:52.250 --> 00:00:54.590 align:start position:0% [Music] you<00:00:53.250> know<00:00:53.340> like<00:00:53.550> the<00:00:53.699> the<00:00:53.879> kind<00:00:54.270> of<00:00:54.300> approach 00:00:54.590 --> 00:00:54.600 align:start position:0% you know like the the kind of approach 00:00:54.600 --> 00:00:56.479 align:start position:0% you know like the the kind of approach that<00:00:54.629> we<00:00:54.930> have<00:00:54.960> that<00:00:55.410> kind<00:00:55.559> of<00:00:55.590> sets<00:00:56.219> apart<00:00:56.430> a 00:00:56.479 --> 00:00:56.489 align:start position:0% that we have that kind of sets apart a 00:00:56.489 --> 00:00:59.810 align:start position:0% that we have that kind of sets apart a CBC<00:00:56.820> Casper<00:00:57.210> from<00:00:57.510> you<00:00:57.840> know<00:00:57.960> other<00:00:58.820> because 00:00:59.810 --> 00:00:59.820 align:start position:0% CBC Casper from you know other because 00:00:59.820 --> 00:01:03.319 align:start position:0% CBC Casper from you know other because there's<00:00:59.969> a<00:01:00.030> protocol<00:01:00.359> research<00:01:01.520> and<00:01:02.520> finally 00:01:03.319 --> 00:01:03.329 align:start position:0% there's a protocol research and finally 00:01:03.329 --> 00:01:04.609 align:start position:0% there's a protocol research and finally you<00:01:03.570> know<00:01:03.660> the<00:01:03.750> last<00:01:03.899> bit<00:01:04.110> of<00:01:04.140> my<00:01:04.229> talk<00:01:04.439> I'll 00:01:04.609 --> 00:01:04.619 align:start position:0% you know the last bit of my talk I'll 00:01:04.619 --> 00:01:06.469 align:start position:0% you know the last bit of my talk I'll just<00:01:04.799> to<00:01:04.890> remind<00:01:05.760> you<00:01:05.909> all<00:01:06.060> that<00:01:06.090> where<00:01:06.360> the 00:01:06.469 --> 00:01:06.479 align:start position:0% just to remind you all that where the 00:01:06.479 --> 00:01:07.730 align:start position:0% just to remind you all that where the resources<00:01:06.869> are<00:01:07.049> show<00:01:07.290> you<00:01:07.380> some<00:01:07.560> new 00:01:07.730 --> 00:01:07.740 align:start position:0% resources are show you some new 00:01:07.740 --> 00:01:13.000 align:start position:0% resources are show you some new resources<00:01:08.100> and<00:01:09.260> make<00:01:10.260> some<00:01:10.439> announcements<00:01:11.119> so 00:01:13.000 --> 00:01:13.010 align:start position:0% resources and make some announcements so 00:01:13.010 --> 00:01:15.530 align:start position:0% resources and make some announcements so let's<00:01:14.010> talk<00:01:14.130> about<00:01:14.340> design<00:01:14.640> methods<00:01:15.060> in<00:01:15.180> CBC 00:01:15.530 --> 00:01:15.540 align:start position:0% let's talk about design methods in CBC 00:01:15.540 --> 00:01:17.600 align:start position:0% let's talk about design methods in CBC Casper<00:01:15.900> the<00:01:16.470> number<00:01:16.710> one<00:01:16.920> kind<00:01:17.250> of<00:01:17.400> like 00:01:17.600 --> 00:01:17.610 align:start position:0% Casper the number one kind of like 00:01:17.610 --> 00:01:20.630 align:start position:0% Casper the number one kind of like design<00:01:18.110> methodology<00:01:19.110> in<00:01:19.229> CBC<00:01:19.530> Casper<00:01:19.860> is<00:01:20.009> the 00:01:20.630 --> 00:01:20.640 align:start position:0% design methodology in CBC Casper is the 00:01:20.640 --> 00:01:22.460 align:start position:0% design methodology in CBC Casper is the correct<00:01:21.119> by<00:01:21.299> construction<00:01:21.960> design<00:01:22.290> a 00:01:22.460 --> 00:01:22.470 align:start position:0% correct by construction design a 00:01:22.470 --> 00:01:25.429 align:start position:0% correct by construction design a protocol<00:01:23.009> design<00:01:23.630> methodology<00:01:24.630> the<00:01:25.140> idea 00:01:25.429 --> 00:01:25.439 align:start position:0% protocol design methodology the idea 00:01:25.439 --> 00:01:27.170 align:start position:0% protocol design methodology the idea with<00:01:25.799> correct<00:01:26.250> right<00:01:26.369> construction<00:01:26.909> is<00:01:27.030> that 00:01:27.170 --> 00:01:27.180 align:start position:0% with correct right construction is that 00:01:27.180 --> 00:01:30.319 align:start position:0% with correct right construction is that like<00:01:27.360> the<00:01:28.049> process<00:01:28.560> by<00:01:29.130> which<00:01:29.159> you<00:01:29.850> decide 00:01:30.319 --> 00:01:30.329 align:start position:0% like the process by which you decide 00:01:30.329 --> 00:01:33.140 align:start position:0% like the process by which you decide what<00:01:30.659> program<00:01:31.110> you<00:01:31.259> write<00:01:31.610> should<00:01:32.610> guarantee 00:01:33.140 --> 00:01:33.150 align:start position:0% what program you write should guarantee 00:01:33.150 --> 00:01:34.850 align:start position:0% what program you write should guarantee that<00:01:33.750> that<00:01:33.900> program<00:01:34.200> has<00:01:34.380> the<00:01:34.409> properties 00:01:34.850 --> 00:01:34.860 align:start position:0% that that program has the properties 00:01:34.860 --> 00:01:37.940 align:start position:0% that that program has the properties that<00:01:34.890> you<00:01:34.979> want<00:01:35.280> like<00:01:36.060> the<00:01:36.210> very<00:01:36.650> process<00:01:37.650> that 00:01:37.940 --> 00:01:37.950 align:start position:0% that you want like the very process that 00:01:37.950 --> 00:01:40.730 align:start position:0% that you want like the very process that you<00:01:38.070> use<00:01:38.369> to<00:01:38.759> specify<00:01:39.140> the<00:01:40.140> protocol<00:01:40.500> should 00:01:40.730 --> 00:01:40.740 align:start position:0% you use to specify the protocol should 00:01:40.740 --> 00:01:43.730 align:start position:0% you use to specify the protocol should guarantee<00:01:41.700> that<00:01:42.119> the<00:01:42.240> protocol<00:01:42.689> has<00:01:43.409> the 00:01:43.730 --> 00:01:43.740 align:start position:0% guarantee that the protocol has the 00:01:43.740 --> 00:01:45.469 align:start position:0% guarantee that the protocol has the properties<00:01:44.100> that<00:01:44.130> you<00:01:44.250> want<00:01:44.520> so<00:01:45.000> somehow<00:01:45.270> like 00:01:45.469 --> 00:01:45.479 align:start position:0% properties that you want so somehow like 00:01:45.479 --> 00:01:48.230 align:start position:0% properties that you want so somehow like the<00:01:45.810> way<00:01:46.020> you<00:01:46.079> decide<00:01:46.710> what<00:01:47.100> like<00:01:47.280> formats<00:01:47.970> to 00:01:48.230 --> 00:01:48.240 align:start position:0% the way you decide what like formats to 00:01:48.240 --> 00:01:51.350 align:start position:0% the way you decide what like formats to use<00:01:48.479> or<00:01:48.780> what<00:01:48.930> like<00:01:49.220> the<00:01:50.220> protocol<00:01:50.729> is<00:01:50.970> in 00:01:51.350 --> 00:01:51.360 align:start position:0% use or what like the protocol is in 00:01:51.360 --> 00:01:53.620 align:start position:0% use or what like the protocol is in terms<00:01:51.509> of<00:01:51.659> like<00:01:51.780> the<00:01:51.930> data<00:01:52.110> and<00:01:52.439> the<00:01:52.560> behavior 00:01:53.620 --> 00:01:53.630 align:start position:0% terms of like the data and the behavior 00:01:53.630 --> 00:01:55.999 align:start position:0% terms of like the data and the behavior you<00:01:54.630> know<00:01:54.750> that<00:01:55.020> happens<00:01:55.470> somehow<00:01:55.770> like<00:01:55.950> the 00:01:55.999 --> 00:01:56.009 align:start position:0% you know that happens somehow like the 00:01:56.009 --> 00:01:57.050 align:start position:0% you know that happens somehow like the definitions<00:01:56.460> don't<00:01:56.579> come<00:01:56.700> out<00:01:56.790> of<00:01:56.909> nowhere 00:01:57.050 --> 00:01:57.060 align:start position:0% definitions don't come out of nowhere 00:01:57.060 --> 00:01:59.420 align:start position:0% definitions don't come out of nowhere and<00:01:57.560> there's<00:01:58.560> like<00:01:58.710> a<00:01:58.740> process<00:01:59.250> by<00:01:59.399> which 00:01:59.420 --> 00:01:59.430 align:start position:0% and there's like a process by which 00:01:59.430 --> 00:02:01.880 align:start position:0% and there's like a process by which stuff<00:02:00.000> gets<00:02:00.149> defined<00:02:00.420> and<00:02:00.780> it's<00:02:01.290> called<00:02:01.560> you 00:02:01.880 --> 00:02:01.890 align:start position:0% stuff gets defined and it's called you 00:02:01.890 --> 00:02:02.810 align:start position:0% stuff gets defined and it's called you know<00:02:01.950> your<00:02:02.100> first<00:02:02.219> eyes<00:02:02.369> are<00:02:02.490> called<00:02:02.610> correct 00:02:02.810 --> 00:02:02.820 align:start position:0% know your first eyes are called correct 00:02:02.820 --> 00:02:06.770 align:start position:0% know your first eyes are called correct by<00:02:02.909> construction<00:02:03.270> if<00:02:04.549> you<00:02:05.549> know<00:02:05.670> the<00:02:05.939> process 00:02:06.770 --> 00:02:06.780 align:start position:0% by construction if you know the process 00:02:06.780 --> 00:02:08.930 align:start position:0% by construction if you know the process that<00:02:07.049> you<00:02:07.740> use<00:02:07.950> to<00:02:08.099> define<00:02:08.310> the<00:02:08.459> thing<00:02:08.640> somehow 00:02:08.930 --> 00:02:08.940 align:start position:0% that you use to define the thing somehow 00:02:08.940 --> 00:02:11.280 align:start position:0% that you use to define the thing somehow is<00:02:09.090> guarantees<00:02:10.050> that 00:02:11.280 --> 00:02:11.290 align:start position:0% is guarantees that 00:02:11.290 --> 00:02:13.140 align:start position:0% is guarantees that definition<00:02:12.219> that<00:02:12.310> comes<00:02:12.519> out<00:02:12.700> is<00:02:12.849> correct 00:02:13.140 --> 00:02:13.150 align:start position:0% definition that comes out is correct 00:02:13.150 --> 00:02:15.509 align:start position:0% definition that comes out is correct this<00:02:13.900> is<00:02:14.079> kind<00:02:14.230> of<00:02:14.260> as<00:02:14.379> opposed<00:02:14.709> to<00:02:14.860> the<00:02:15.189> trial 00:02:15.509 --> 00:02:15.519 align:start position:0% this is kind of as opposed to the trial 00:02:15.519 --> 00:02:17.610 align:start position:0% this is kind of as opposed to the trial and<00:02:15.730> error<00:02:15.879> approach<00:02:16.150> where<00:02:16.989> you<00:02:17.170> will<00:02:17.409> like 00:02:17.610 --> 00:02:17.620 align:start position:0% and error approach where you will like 00:02:17.620 --> 00:02:19.709 align:start position:0% and error approach where you will like try<00:02:18.010> something<00:02:18.730> and<00:02:18.909> then<00:02:19.030> analyze<00:02:19.420> it<00:02:19.450> and 00:02:19.709 --> 00:02:19.719 align:start position:0% try something and then analyze it and 00:02:19.719 --> 00:02:22.530 align:start position:0% try something and then analyze it and then<00:02:19.780> you<00:02:20.439> might<00:02:20.620> it<00:02:21.579> might<00:02:21.819> work<00:02:22.030> am<00:02:22.209> I<00:02:22.329> not 00:02:22.530 --> 00:02:22.540 align:start position:0% then you might it might work am I not 00:02:22.540 --> 00:02:24.509 align:start position:0% then you might it might work am I not you'll<00:02:22.810> maybe<00:02:23.170> get<00:02:23.409> lucky<00:02:23.560> and<00:02:23.950> maybe<00:02:24.250> and<00:02:24.430> if 00:02:24.509 --> 00:02:24.519 align:start position:0% you'll maybe get lucky and maybe and if 00:02:24.519 --> 00:02:25.830 align:start position:0% you'll maybe get lucky and maybe and if not<00:02:24.730> they<00:02:24.909> may<00:02:25.030> you<00:02:25.090> learn<00:02:25.239> something<00:02:25.689> and 00:02:25.830 --> 00:02:25.840 align:start position:0% not they may you learn something and 00:02:25.840 --> 00:02:27.809 align:start position:0% not they may you learn something and just<00:02:25.900> keep<00:02:26.409> trying<00:02:26.590> until<00:02:26.950> maybe<00:02:27.370> you'll<00:02:27.609> find 00:02:27.809 --> 00:02:27.819 align:start position:0% just keep trying until maybe you'll find 00:02:27.819 --> 00:02:29.610 align:start position:0% just keep trying until maybe you'll find something<00:02:28.030> so<00:02:28.750> this<00:02:28.870> is<00:02:28.959> very<00:02:29.319> different 00:02:29.610 --> 00:02:29.620 align:start position:0% something so this is very different 00:02:29.620 --> 00:02:31.830 align:start position:0% something so this is very different approach<00:02:30.250> right<00:02:30.549> because<00:02:30.819> instead<00:02:31.060> of<00:02:31.120> like 00:02:31.830 --> 00:02:31.840 align:start position:0% approach right because instead of like 00:02:31.840 --> 00:02:34.170 align:start position:0% approach right because instead of like we<00:02:31.959> never<00:02:32.079> really<00:02:32.500> have<00:02:33.220> the<00:02:33.549> trial<00:02:33.879> and<00:02:34.030> error 00:02:34.170 --> 00:02:34.180 align:start position:0% we never really have the trial and error 00:02:34.180 --> 00:02:36.660 align:start position:0% we never really have the trial and error we<00:02:34.450> just<00:02:34.659> have<00:02:34.810> like<00:02:34.989> a<00:02:35.200> lot<00:02:35.769> of<00:02:35.950> time<00:02:36.189> defining 00:02:36.660 --> 00:02:36.670 align:start position:0% we just have like a lot of time defining 00:02:36.670 --> 00:02:38.699 align:start position:0% we just have like a lot of time defining stuff<00:02:37.150> and<00:02:37.450> then<00:02:37.540> like<00:02:37.750> once<00:02:37.959> the<00:02:38.200> definition 00:02:38.699 --> 00:02:38.709 align:start position:0% stuff and then like once the definition 00:02:38.709 --> 00:02:40.259 align:start position:0% stuff and then like once the definition pops<00:02:38.950> out<00:02:39.129> it's<00:02:39.340> like<00:02:39.430> correct<00:02:39.879> by 00:02:40.259 --> 00:02:40.269 align:start position:0% pops out it's like correct by 00:02:40.269 --> 00:02:41.369 align:start position:0% pops out it's like correct by construction<00:02:40.780> and<00:02:40.930> so<00:02:41.019> there's<00:02:41.139> no<00:02:41.260> like 00:02:41.369 --> 00:02:41.379 align:start position:0% construction and so there's no like 00:02:41.379 --> 00:02:43.470 align:start position:0% construction and so there's no like error<00:02:42.010> but<00:02:42.700> in<00:02:42.790> some<00:02:42.909> way<00:02:43.000> like<00:02:43.209> you<00:02:43.299> know<00:02:43.389> it 00:02:43.470 --> 00:02:43.480 align:start position:0% error but in some way like you know it 00:02:43.480 --> 00:02:45.509 align:start position:0% error but in some way like you know it takes<00:02:43.659> us<00:02:43.780> a<00:02:43.810> lot<00:02:44.739> longer<00:02:44.889> to<00:02:45.129> come<00:02:45.280> out<00:02:45.370> with<00:02:45.489> a 00:02:45.509 --> 00:02:45.519 align:start position:0% takes us a lot longer to come out with a 00:02:45.519 --> 00:02:48.420 align:start position:0% takes us a lot longer to come out with a full<00:02:45.700> definition<00:02:46.709> but<00:02:47.709> when<00:02:47.889> it<00:02:48.010> when<00:02:48.159> it<00:02:48.250> pops 00:02:48.420 --> 00:02:48.430 align:start position:0% full definition but when it when it pops 00:02:48.430 --> 00:02:50.159 align:start position:0% full definition but when it when it pops out<00:02:48.639> you<00:02:48.939> know<00:02:49.389> we<00:02:49.569> know<00:02:49.689> it's<00:02:49.870> correct<00:02:50.019> by 00:02:50.159 --> 00:02:50.169 align:start position:0% out you know we know it's correct by 00:02:50.169 --> 00:02:53.220 align:start position:0% out you know we know it's correct by construction<00:02:51.480> and<00:02:52.480> we<00:02:52.629> don't<00:02:52.810> worry<00:02:52.959> at<00:02:53.109> all 00:02:53.220 --> 00:02:53.230 align:start position:0% construction and we don't worry at all 00:02:53.230 --> 00:02:57.240 align:start position:0% construction and we don't worry at all about<00:02:53.790> mmm<00:02:55.200> mistakes<00:02:56.200> in<00:02:56.409> the<00:02:56.560> specification 00:02:57.240 --> 00:02:57.250 align:start position:0% about mmm mistakes in the specification 00:02:57.250 --> 00:03:01.309 align:start position:0% about mmm mistakes in the specification in<00:02:57.489> the<00:02:57.579> same<00:02:57.730> way<00:02:58.919> so<00:02:59.919> there's<00:03:00.250> two<00:03:00.459> basically 00:03:01.309 --> 00:03:01.319 align:start position:0% in the same way so there's two basically 00:03:01.319 --> 00:03:03.210 align:start position:0% in the same way so there's two basically kinds<00:03:02.319> of<00:03:02.439> correct<00:03:02.650> by<00:03:02.769> construction 00:03:03.210 --> 00:03:03.220 align:start position:0% kinds of correct by construction 00:03:03.220 --> 00:03:04.679 align:start position:0% kinds of correct by construction software<00:03:03.790> design<00:03:04.000> that<00:03:04.209> I'm<00:03:04.269> kind<00:03:04.450> of<00:03:04.480> aware 00:03:04.679 --> 00:03:04.689 align:start position:0% software design that I'm kind of aware 00:03:04.689 --> 00:03:07.890 align:start position:0% software design that I'm kind of aware of<00:03:04.810> one<00:03:04.989> of<00:03:05.049> them<00:03:05.139> is<00:03:05.260> you<00:03:05.799> know<00:03:05.889> you<00:03:06.900> you 00:03:07.890 --> 00:03:07.900 align:start position:0% of one of them is you know you you 00:03:07.900 --> 00:03:12.300 align:start position:0% of one of them is you know you you define<00:03:08.620> like<00:03:08.829> a<00:03:08.859> a<00:03:09.220> proof<00:03:10.919> may<00:03:11.919> be<00:03:11.980> a<00:03:12.040> type 00:03:12.300 --> 00:03:12.310 align:start position:0% define like a a proof may be a type 00:03:12.310 --> 00:03:15.599 align:start position:0% define like a a proof may be a type system<00:03:12.730> and<00:03:12.849> some<00:03:13.030> proofs<00:03:13.299> over<00:03:14.340> broad<00:03:15.340> class 00:03:15.599 --> 00:03:15.609 align:start position:0% system and some proofs over broad class 00:03:15.609 --> 00:03:17.640 align:start position:0% system and some proofs over broad class of<00:03:15.639> four<00:03:16.299> over<00:03:16.449> calls<00:03:16.659> or<00:03:16.900> broad<00:03:17.290> classic 00:03:17.640 --> 00:03:17.650 align:start position:0% of four over calls or broad classic 00:03:17.650 --> 00:03:20.430 align:start position:0% of four over calls or broad classic programs<00:03:17.979> and<00:03:18.220> then<00:03:18.909> you<00:03:19.030> in<00:03:19.659> your<00:03:19.930> design 00:03:20.430 --> 00:03:20.440 align:start position:0% programs and then you in your design 00:03:20.440 --> 00:03:22.860 align:start position:0% programs and then you in your design process<00:03:20.470> choose<00:03:21.280> your<00:03:21.819> protocol<00:03:22.359> your<00:03:22.569> your 00:03:22.860 --> 00:03:22.870 align:start position:0% process choose your protocol your your 00:03:22.870 --> 00:03:25.619 align:start position:0% process choose your protocol your your protocol<00:03:23.349> to<00:03:23.859> be<00:03:23.889> part<00:03:24.250> of<00:03:24.280> that<00:03:24.340> set<00:03:24.609> so<00:03:24.879> that 00:03:25.619 --> 00:03:25.629 align:start position:0% protocol to be part of that set so that 00:03:25.629 --> 00:03:27.089 align:start position:0% protocol to be part of that set so that you<00:03:25.930> know<00:03:26.139> when<00:03:26.379> you<00:03:26.470> choose<00:03:26.709> it<00:03:26.859> that<00:03:27.010> it's 00:03:27.089 --> 00:03:27.099 align:start position:0% you know when you choose it that it's 00:03:27.099 --> 00:03:31.589 align:start position:0% you know when you choose it that it's gonna<00:03:27.220> satisfy<00:03:27.459> the<00:03:28.109> theorem<00:03:29.109> that<00:03:30.510> you<00:03:31.510> know 00:03:31.589 --> 00:03:31.599 align:start position:0% gonna satisfy the theorem that you know 00:03:31.599 --> 00:03:34.199 align:start position:0% gonna satisfy the theorem that you know is<00:03:31.720> is<00:03:32.500> is<00:03:32.769> inhabited<00:03:33.489> by<00:03:33.519> this<00:03:33.609> much<00:03:33.879> broader 00:03:34.199 --> 00:03:34.209 align:start position:0% is is is inhabited by this much broader 00:03:34.209 --> 00:03:36.960 align:start position:0% is is is inhabited by this much broader set<00:03:34.629> of<00:03:34.659> protocols<00:03:35.440> so<00:03:36.280> if<00:03:36.669> we<00:03:36.729> have<00:03:36.819> like<00:03:36.909> a 00:03:36.960 --> 00:03:36.970 align:start position:0% set of protocols so if we have like a 00:03:36.970 --> 00:03:38.460 align:start position:0% set of protocols so if we have like a you<00:03:37.269> know<00:03:37.299> family<00:03:37.780> of<00:03:37.870> protocols<00:03:38.049> they<00:03:38.379> all 00:03:38.460 --> 00:03:38.470 align:start position:0% you know family of protocols they all 00:03:38.470 --> 00:03:40.349 align:start position:0% you know family of protocols they all satisfy<00:03:38.680> a<00:03:38.889> theorem<00:03:39.220> and<00:03:39.400> we<00:03:39.879> like<00:03:40.030> pick 00:03:40.349 --> 00:03:40.359 align:start position:0% satisfy a theorem and we like pick 00:03:40.359 --> 00:03:42.270 align:start position:0% satisfy a theorem and we like pick protocols<00:03:40.989> or<00:03:41.109> construct<00:03:41.590> them<00:03:41.769> in<00:03:41.889> a<00:03:41.949> way<00:03:42.069> to 00:03:42.270 --> 00:03:42.280 align:start position:0% protocols or construct them in a way to 00:03:42.280 --> 00:03:43.530 align:start position:0% protocols or construct them in a way to guarantee<00:03:42.430> that<00:03:42.609> it<00:03:42.819> part<00:03:43.180> of<00:03:43.209> the<00:03:43.299> family 00:03:43.530 --> 00:03:43.540 align:start position:0% guarantee that it part of the family 00:03:43.540 --> 00:03:46.020 align:start position:0% guarantee that it part of the family then<00:03:44.049> we<00:03:44.139> can<00:03:44.260> in<00:03:45.220> a<00:03:45.310> correct<00:03:45.669> by<00:03:45.729> construction 00:03:46.020 --> 00:03:46.030 align:start position:0% then we can in a correct by construction 00:03:46.030 --> 00:03:49.500 align:start position:0% then we can in a correct by construction way<00:03:46.329> get<00:03:47.049> a<00:03:47.079> protocol<00:03:47.560> that<00:03:47.620> has<00:03:48.510> that 00:03:49.500 --> 00:03:49.510 align:start position:0% way get a protocol that has that 00:03:49.510 --> 00:03:51.839 align:start position:0% way get a protocol that has that property<00:03:49.810> that<00:03:50.260> you<00:03:50.829> know<00:03:50.919> the<00:03:51.069> theorem<00:03:51.400> shows 00:03:51.839 --> 00:03:51.849 align:start position:0% property that you know the theorem shows 00:03:51.849 --> 00:03:54.089 align:start position:0% property that you know the theorem shows for<00:03:52.120> the<00:03:52.180> family<00:03:52.479> and<00:03:53.079> then<00:03:53.199> the<00:03:53.290> other<00:03:53.379> kind 00:03:54.089 --> 00:03:54.099 align:start position:0% for the family and then the other kind 00:03:54.099 --> 00:03:56.460 align:start position:0% for the family and then the other kind of<00:03:54.159> approaches<00:03:54.549> that<00:03:55.019> the<00:03:56.019> protocols<00:03:56.409> are 00:03:56.460 --> 00:03:56.470 align:start position:0% of approaches that the protocols are 00:03:56.470 --> 00:03:57.300 align:start position:0% of approaches that the protocols are specified<00:03:56.829> in<00:03:56.859> a<00:03:57.010> way<00:03:57.069> that<00:03:57.220> actually 00:03:57.300 --> 00:03:57.310 align:start position:0% specified in a way that actually 00:03:57.310 --> 00:03:58.649 align:start position:0% specified in a way that actually generates<00:03:57.849> a<00:03:57.909> proof<00:03:58.090> of<00:03:58.209> their<00:03:58.329> correctness 00:03:58.649 --> 00:03:58.659 align:start position:0% generates a proof of their correctness 00:03:58.659 --> 00:04:02.069 align:start position:0% generates a proof of their correctness so<00:03:59.560> you<00:04:00.220> know<00:04:00.310> the<00:04:00.489> you<00:04:01.329> generate<00:04:01.930> the 00:04:02.069 --> 00:04:02.079 align:start position:0% so you know the you generate the 00:04:02.079 --> 00:04:04.740 align:start position:0% so you know the you generate the protocol<00:04:02.799> and<00:04:03.099> the<00:04:03.340> proof<00:04:03.579> like<00:04:04.060> a<00:04:04.090> new<00:04:04.359> proof 00:04:04.740 --> 00:04:04.750 align:start position:0% protocol and the proof like a new proof 00:04:04.750 --> 00:04:08.159 align:start position:0% protocol and the proof like a new proof for<00:04:05.049> every<00:04:05.199> proton<00:04:05.879> and<00:04:06.879> and<00:04:07.659> they<00:04:07.780> don't<00:04:08.019> do 00:04:08.159 --> 00:04:08.169 align:start position:0% for every proton and and they don't do 00:04:08.169 --> 00:04:13.740 align:start position:0% for every proton and and they don't do any<00:04:08.319> of<00:04:08.379> that<00:04:10.889> it<00:04:11.889> sounds<00:04:12.250> hard<00:04:12.489> and<00:04:12.759> I've<00:04:13.509> ever 00:04:13.740 --> 00:04:13.750 align:start position:0% any of that it sounds hard and I've ever 00:04:13.750 --> 00:04:14.819 align:start position:0% any of that it sounds hard and I've ever heard<00:04:13.900> of<00:04:13.959> people<00:04:14.049> doing<00:04:14.319> it<00:04:14.590> and<00:04:14.620> like 00:04:14.819 --> 00:04:14.829 align:start position:0% heard of people doing it and like 00:04:14.829 --> 00:04:16.409 align:start position:0% heard of people doing it and like programming<00:04:15.310> languages<00:04:15.669> and<00:04:15.790> compilers<00:04:16.030> but 00:04:16.409 --> 00:04:16.419 align:start position:0% programming languages and compilers but 00:04:16.419 --> 00:04:19.110 align:start position:0% programming languages and compilers but it<00:04:16.870> hasn't<00:04:17.079> showed<00:04:17.320> up<00:04:17.440> for<00:04:17.590> me<00:04:17.680> yet<00:04:17.829> so<00:04:18.579> what<00:04:19.060> I 00:04:19.110 --> 00:04:19.120 align:start position:0% it hasn't showed up for me yet so what I 00:04:19.120 --> 00:04:21.269 align:start position:0% it hasn't showed up for me yet so what I do<00:04:19.209> here<00:04:19.510> is<00:04:19.539> basically<00:04:19.750> we<00:04:20.109> we<00:04:20.739> do<00:04:21.130> is<00:04:21.190> we 00:04:21.269 --> 00:04:21.279 align:start position:0% do here is basically we we do is we 00:04:21.279 --> 00:04:24.870 align:start position:0% do here is basically we we do is we define<00:04:23.219> large<00:04:24.219> family 00:04:24.870 --> 00:04:24.880 align:start position:0% define large family 00:04:24.880 --> 00:04:27.210 align:start position:0% define large family of<00:04:24.940> protocols<00:04:25.510> and<00:04:25.990> we<00:04:26.140> prove<00:04:26.800> things<00:04:26.950> about 00:04:27.210 --> 00:04:27.220 align:start position:0% of protocols and we prove things about 00:04:27.220 --> 00:04:29.760 align:start position:0% of protocols and we prove things about them<00:04:27.510> and<00:04:28.510> then<00:04:28.690> we<00:04:28.720> and<00:04:29.260> then<00:04:29.350> we<00:04:29.440> and<00:04:29.650> then<00:04:29.680> we 00:04:29.760 --> 00:04:29.770 align:start position:0% them and then we and then we and then we 00:04:29.770 --> 00:04:31.820 align:start position:0% them and then we and then we and then we choose<00:04:30.100> specific<00:04:30.670> protocols<00:04:31.120> out<00:04:31.390> of<00:04:31.570> them 00:04:31.820 --> 00:04:31.830 align:start position:0% choose specific protocols out of them 00:04:31.830 --> 00:04:34.770 align:start position:0% choose specific protocols out of them which<00:04:32.830> will<00:04:33.190> there<00:04:33.880> by<00:04:34.120> virtue<00:04:34.150> of<00:04:34.510> being<00:04:34.570> in 00:04:34.770 --> 00:04:34.780 align:start position:0% which will there by virtue of being in 00:04:34.780 --> 00:04:38.040 align:start position:0% which will there by virtue of being in those<00:04:35.080> families<00:04:35.440> have<00:04:35.650> these<00:04:35.860> properties<00:04:37.050> so 00:04:38.040 --> 00:04:38.050 align:start position:0% those families have these properties so 00:04:38.050 --> 00:04:40.350 align:start position:0% those families have these properties so now<00:04:38.560> we're<00:04:38.710> gonna<00:04:38.830> switch<00:04:39.160> over<00:04:39.400> to<00:04:39.430> this<00:04:39.670> very 00:04:40.350 --> 00:04:40.360 align:start position:0% now we're gonna switch over to this very 00:04:40.360 --> 00:04:43.590 align:start position:0% now we're gonna switch over to this very related<00:04:40.840> topic<00:04:41.700> but<00:04:42.700> going<00:04:43.030> off<00:04:43.210> into<00:04:43.450> the 00:04:43.590 --> 00:04:43.600 align:start position:0% related topic but going off into the 00:04:43.600 --> 00:04:46.530 align:start position:0% related topic but going off into the math<00:04:43.780> deep<00:04:44.050> end<00:04:44.230> so<00:04:45.070> domain<00:04:46.030> theory<00:04:46.390> is<00:04:46.510> a 00:04:46.530 --> 00:04:46.540 align:start position:0% math deep end so domain theory is a 00:04:46.540 --> 00:04:49.980 align:start position:0% math deep end so domain theory is a field<00:04:46.780> of<00:04:46.870> mathematics<00:04:47.380> that<00:04:47.470> studies<00:04:48.840> it's<00:04:49.840> a 00:04:49.980 --> 00:04:49.990 align:start position:0% field of mathematics that studies it's a 00:04:49.990 --> 00:04:53.010 align:start position:0% field of mathematics that studies it's a you<00:04:50.740> know<00:04:50.800> a<00:04:51.160> it<00:04:51.910> studies<00:04:52.270> the<00:04:52.300> semantics<00:04:52.870> of 00:04:53.010 --> 00:04:53.020 align:start position:0% you know a it studies the semantics of 00:04:53.020 --> 00:04:56.460 align:start position:0% you know a it studies the semantics of programming<00:04:53.080> languages<00:04:54.390> but<00:04:55.390> really<00:04:55.930> the 00:04:56.460 --> 00:04:56.470 align:start position:0% programming languages but really the 00:04:56.470 --> 00:04:57.660 align:start position:0% programming languages but really the reason<00:04:56.710> why<00:04:56.770> is<00:04:56.890> super<00:04:57.100> interesting<00:04:57.400> to<00:04:57.490> me 00:04:57.660 --> 00:04:57.670 align:start position:0% reason why is super interesting to me 00:04:57.670 --> 00:05:01.440 align:start position:0% reason why is super interesting to me and<00:04:58.000> it<00:04:59.010> just<00:05:00.010> invites<00:05:00.850> really<00:05:01.090> useful<00:05:01.330> for 00:05:01.440 --> 00:05:01.450 align:start position:0% and it just invites really useful for 00:05:01.450 --> 00:05:02.340 align:start position:0% and it just invites really useful for understanding<00:05:02.050> the<00:05:02.110> correct<00:05:02.290> by 00:05:02.340 --> 00:05:02.350 align:start position:0% understanding the correct by 00:05:02.350 --> 00:05:03.930 align:start position:0% understanding the correct by construction<00:05:02.620> process<00:05:03.010> is<00:05:03.160> because<00:05:03.790> it 00:05:03.930 --> 00:05:03.940 align:start position:0% construction process is because it 00:05:03.940 --> 00:05:05.790 align:start position:0% construction process is because it provides<00:05:03.970> us<00:05:04.540> a<00:05:04.660> language<00:05:04.870> for<00:05:05.290> talking<00:05:05.500> about 00:05:05.790 --> 00:05:05.800 align:start position:0% provides us a language for talking about 00:05:05.800 --> 00:05:07.350 align:start position:0% provides us a language for talking about partial<00:05:06.550> definitions 00:05:07.350 --> 00:05:07.360 align:start position:0% partial definitions 00:05:07.360 --> 00:05:10.020 align:start position:0% partial definitions you<00:05:07.900> know<00:05:07.990> incomplete<00:05:08.620> definitions<00:05:09.220> partial 00:05:10.020 --> 00:05:10.030 align:start position:0% you know incomplete definitions partial 00:05:10.030 --> 00:05:13.470 align:start position:0% you know incomplete definitions partial protocol<00:05:10.720> specifications<00:05:11.820> and<00:05:12.820> and<00:05:13.120> and<00:05:13.390> we 00:05:13.470 --> 00:05:13.480 align:start position:0% protocol specifications and and and we 00:05:13.480 --> 00:05:16.320 align:start position:0% protocol specifications and and and we can<00:05:14.130> understand<00:05:15.130> what<00:05:15.310> it<00:05:15.430> means<00:05:15.550> to<00:05:15.940> have<00:05:16.270> a 00:05:16.320 --> 00:05:16.330 align:start position:0% can understand what it means to have a 00:05:16.330 --> 00:05:18.840 align:start position:0% can understand what it means to have a process<00:05:16.900> of<00:05:17.020> defining<00:05:17.350> something<00:05:17.710> as<00:05:18.130> opposed 00:05:18.840 --> 00:05:18.850 align:start position:0% process of defining something as opposed 00:05:18.850 --> 00:05:20.160 align:start position:0% process of defining something as opposed to<00:05:18.940> just<00:05:19.060> having<00:05:19.150> something<00:05:19.510> that's<00:05:19.630> outright 00:05:20.160 --> 00:05:20.170 align:start position:0% to just having something that's outright 00:05:20.170 --> 00:05:22.950 align:start position:0% to just having something that's outright fully<00:05:20.620> defined<00:05:21.040> as<00:05:21.280> you<00:05:22.150> might<00:05:22.330> have<00:05:22.480> in<00:05:22.690> set 00:05:22.950 --> 00:05:22.960 align:start position:0% fully defined as you might have in set 00:05:22.960 --> 00:05:26.310 align:start position:0% fully defined as you might have in set theory<00:05:24.300> so<00:05:25.300> like<00:05:25.510> you<00:05:25.960> know<00:05:25.990> you<00:05:26.080> should<00:05:26.290> think 00:05:26.310 --> 00:05:26.320 align:start position:0% theory so like you know you should think 00:05:26.320 --> 00:05:28.050 align:start position:0% theory so like you know you should think of<00:05:26.590> domain<00:05:26.920> theory<00:05:27.280> as<00:05:27.370> something<00:05:27.610> that<00:05:27.640> arose 00:05:28.050 --> 00:05:28.060 align:start position:0% of domain theory as something that arose 00:05:28.060 --> 00:05:32.010 align:start position:0% of domain theory as something that arose out<00:05:28.600> of<00:05:28.720> people's<00:05:30.330> feelings<00:05:31.330> that<00:05:31.630> set<00:05:31.840> theory 00:05:32.010 --> 00:05:32.020 align:start position:0% out of people's feelings that set theory 00:05:32.020 --> 00:05:34.290 align:start position:0% out of people's feelings that set theory was<00:05:32.140> inadequate<00:05:32.620> for<00:05:32.770> dealing<00:05:33.100> with<00:05:33.300> programs 00:05:34.290 --> 00:05:34.300 align:start position:0% was inadequate for dealing with programs 00:05:34.300 --> 00:05:36.210 align:start position:0% was inadequate for dealing with programs and<00:05:34.570> the<00:05:34.990> semantics<00:05:35.470> of<00:05:35.590> programs<00:05:35.980> especially 00:05:36.210 --> 00:05:36.220 align:start position:0% and the semantics of programs especially 00:05:36.220 --> 00:05:38.130 align:start position:0% and the semantics of programs especially recursive<00:05:36.970> programs<00:05:37.360> and<00:05:37.600> like<00:05:37.810> a<00:05:37.840> lazy 00:05:38.130 --> 00:05:38.140 align:start position:0% recursive programs and like a lazy 00:05:38.140 --> 00:05:41.850 align:start position:0% recursive programs and like a lazy evaluation<00:05:39.540> mmm<00:05:40.570> but<00:05:40.690> I'm<00:05:40.780> not<00:05:41.290> an<00:05:41.410> expert<00:05:41.620> in 00:05:41.850 --> 00:05:41.860 align:start position:0% evaluation mmm but I'm not an expert in 00:05:41.860 --> 00:05:43.950 align:start position:0% evaluation mmm but I'm not an expert in domain<00:05:42.100> theory<00:05:42.340> but<00:05:42.970> there<00:05:43.450> are<00:05:43.540> some<00:05:43.720> things 00:05:43.950 --> 00:05:43.960 align:start position:0% domain theory but there are some things 00:05:43.960 --> 00:05:45.090 align:start position:0% domain theory but there are some things that<00:05:44.050> I've<00:05:44.200> learned<00:05:44.470> from<00:05:44.590> domain<00:05:44.890> theory 00:05:45.090 --> 00:05:45.100 align:start position:0% that I've learned from domain theory 00:05:45.100 --> 00:05:47.340 align:start position:0% that I've learned from domain theory that<00:05:45.250> I<00:05:45.340> find<00:05:45.690> super<00:05:46.690> useful<00:05:46.840> for<00:05:47.050> thinking 00:05:47.340 --> 00:05:47.350 align:start position:0% that I find super useful for thinking 00:05:47.350 --> 00:05:50.100 align:start position:0% that I find super useful for thinking about<00:05:47.440> a<00:05:48.150> bunch<00:05:49.150> of<00:05:49.240> stuff<00:05:49.390> including<00:05:49.600> correct 00:05:50.100 --> 00:05:50.110 align:start position:0% about a bunch of stuff including correct 00:05:50.110 --> 00:05:51.990 align:start position:0% about a bunch of stuff including correct by<00:05:50.200> construction<00:05:50.560> protocol<00:05:50.950> design<00:05:51.190> so 00:05:51.990 --> 00:05:52.000 align:start position:0% by construction protocol design so 00:05:52.000 --> 00:05:55.410 align:start position:0% by construction protocol design so there's<00:05:52.180> a<00:05:52.240> really<00:05:52.420> really<00:05:53.520> you<00:05:54.520> know<00:05:54.610> kind<00:05:55.300> of 00:05:55.410 --> 00:05:55.420 align:start position:0% there's a really really you know kind of 00:05:55.420 --> 00:05:59.310 align:start position:0% there's a really really you know kind of core<00:05:56.020> notation<00:05:56.650> in<00:05:57.210> in<00:05:58.210> domain<00:05:58.540> theory<00:05:58.780> to<00:05:59.080> use 00:05:59.310 --> 00:05:59.320 align:start position:0% core notation in in domain theory to use 00:05:59.320 --> 00:06:02.190 align:start position:0% core notation in in domain theory to use this<00:05:59.650> like<00:06:00.370> and<00:06:01.360> to<00:06:01.510> define<00:06:01.840> this<00:06:02.140> thing 00:06:02.190 --> 00:06:02.200 align:start position:0% this like and to define this thing 00:06:02.200 --> 00:06:04.680 align:start position:0% this like and to define this thing called<00:06:02.590> undefined<00:06:03.100> so<00:06:03.850> this<00:06:03.970> bottom<00:06:04.300> notation 00:06:04.680 --> 00:06:04.690 align:start position:0% called undefined so this bottom notation 00:06:04.690 --> 00:06:06.960 align:start position:0% called undefined so this bottom notation means<00:06:04.810> undefined<00:06:05.380> and<00:06:05.650> it's<00:06:06.160> like<00:06:06.280> defined<00:06:06.730> to 00:06:06.960 --> 00:06:06.970 align:start position:0% means undefined and it's like defined to 00:06:06.970 --> 00:06:10.110 align:start position:0% means undefined and it's like defined to be<00:06:07.120> the<00:06:07.300> most<00:06:07.450> undefined<00:06:07.960> thing<00:06:08.230> it<00:06:08.530> is<00:06:09.250> the 00:06:10.110 --> 00:06:10.120 align:start position:0% be the most undefined thing it is the 00:06:10.120 --> 00:06:12.030 align:start position:0% be the most undefined thing it is the most<00:06:10.390> undefined<00:06:10.930> thing<00:06:11.140> in<00:06:11.320> this<00:06:11.440> partial 00:06:12.030 --> 00:06:12.040 align:start position:0% most undefined thing in this partial 00:06:12.040 --> 00:06:15.600 align:start position:0% most undefined thing in this partial order<00:06:12.370> of<00:06:12.550> defined<00:06:13.140> admits<00:06:14.140> like<00:06:14.380> if<00:06:14.770> I<00:06:15.220> if<00:06:15.490> I 00:06:15.600 --> 00:06:15.610 align:start position:0% order of defined admits like if I if I 00:06:15.610 --> 00:06:17.220 align:start position:0% order of defined admits like if I if I say<00:06:15.790> nothing<00:06:16.120> about<00:06:16.240> my<00:06:16.330> protocol<00:06:16.810> then<00:06:17.050> like 00:06:17.220 --> 00:06:17.230 align:start position:0% say nothing about my protocol then like 00:06:17.230 --> 00:06:20.550 align:start position:0% say nothing about my protocol then like I<00:06:17.350> have<00:06:17.440> left<00:06:18.310> it<00:06:18.430> completely<00:06:18.520> undefined<00:06:19.560> and 00:06:20.550 --> 00:06:20.560 align:start position:0% I have left it completely undefined and 00:06:20.560 --> 00:06:22.050 align:start position:0% I have left it completely undefined and then<00:06:20.740> somehow<00:06:21.130> that's<00:06:21.370> like<00:06:21.520> the<00:06:21.790> most 00:06:22.050 --> 00:06:22.060 align:start position:0% then somehow that's like the most 00:06:22.060 --> 00:06:23.850 align:start position:0% then somehow that's like the most undefined<00:06:22.660> that<00:06:22.750> I<00:06:22.840> could<00:06:22.990> leave<00:06:23.140> it<00:06:23.170> and<00:06:23.740> as 00:06:23.850 --> 00:06:23.860 align:start position:0% undefined that I could leave it and as 00:06:23.860 --> 00:06:25.980 align:start position:0% undefined that I could leave it and as soon<00:06:24.010> as<00:06:24.100> I<00:06:24.160> say<00:06:24.400> stuff<00:06:24.640> I<00:06:24.850> it<00:06:25.630> becomes<00:06:25.840> more 00:06:25.980 --> 00:06:25.990 align:start position:0% soon as I say stuff I it becomes more 00:06:25.990 --> 00:06:28.290 align:start position:0% soon as I say stuff I it becomes more defined<00:06:26.490> and<00:06:27.490> we<00:06:27.610> could<00:06:27.730> talk<00:06:27.910> about<00:06:28.060> in 00:06:28.290 --> 00:06:28.300 align:start position:0% defined and we could talk about in 00:06:28.300 --> 00:06:30.450 align:start position:0% defined and we could talk about in reason<00:06:28.600> formally<00:06:29.050> about<00:06:29.290> this<00:06:29.860> order<00:06:30.310> of 00:06:30.450 --> 00:06:30.460 align:start position:0% reason formally about this order of 00:06:30.460 --> 00:06:31.830 align:start position:0% reason formally about this order of defined<00:06:30.790> earnest<00:06:31.030> and<00:06:31.180> this<00:06:31.300> process<00:06:31.600> of 00:06:31.830 --> 00:06:31.840 align:start position:0% defined earnest and this process of 00:06:31.840 --> 00:06:33.690 align:start position:0% defined earnest and this process of defining<00:06:32.200> stuff<00:06:32.470> and<00:06:32.710> you<00:06:33.100> know<00:06:33.190> having<00:06:33.430> a 00:06:33.690 --> 00:06:33.700 align:start position:0% defining stuff and you know having a 00:06:33.700 --> 00:06:36.750 align:start position:0% defining stuff and you know having a certain<00:06:34.030> stages<00:06:34.240> a<00:06:34.510> partial<00:06:35.229> definition<00:06:35.760> and 00:06:36.750 --> 00:06:36.760 align:start position:0% certain stages a partial definition and 00:06:36.760 --> 00:06:38.100 align:start position:0% certain stages a partial definition and then<00:06:36.910> getting<00:06:37.150> in<00:06:37.300> more<00:06:37.450> and<00:06:37.510> more 00:06:38.100 --> 00:06:38.110 align:start position:0% then getting in more and more 00:06:38.110 --> 00:06:43.110 align:start position:0% then getting in more and more learn<00:06:38.200> more<00:06:39.600> defined<00:06:40.600> protocols<00:06:41.050> so<00:06:41.860> if<00:06:42.250> a<00:06:42.520> is 00:06:43.110 --> 00:06:43.120 align:start position:0% learn more defined protocols so if a is 00:06:43.120 --> 00:06:45.450 align:start position:0% learn more defined protocols so if a is a<00:06:43.300> definition<00:06:43.840> that<00:06:43.990> can<00:06:44.140> be<00:06:44.290> reached<00:06:45.070> from<00:06:45.250> a 00:06:45.450 --> 00:06:45.460 align:start position:0% a definition that can be reached from a 00:06:45.460 --> 00:06:48.540 align:start position:0% a definition that can be reached from a definition<00:06:46.000> B<00:06:46.780> by<00:06:47.380> replacing<00:06:47.680> an<00:06:48.070> undefined 00:06:48.540 --> 00:06:48.550 align:start position:0% definition B by replacing an undefined 00:06:48.550 --> 00:06:50.850 align:start position:0% definition B by replacing an undefined term<00:06:48.820> and<00:06:49.000> B<00:06:49.150> with<00:06:49.780> something<00:06:50.110> that's<00:06:50.260> defined 00:06:50.850 --> 00:06:50.860 align:start position:0% term and B with something that's defined 00:06:50.860 --> 00:06:53.550 align:start position:0% term and B with something that's defined or<00:06:51.490> something<00:06:51.760> else<00:06:51.910> then<00:06:52.660> a<00:06:52.870> is<00:06:53.170> gonna<00:06:53.290> be<00:06:53.380> is 00:06:53.550 --> 00:06:53.560 align:start position:0% or something else then a is gonna be is 00:06:53.560 --> 00:06:56.850 align:start position:0% or something else then a is gonna be is more<00:06:53.920> defined<00:06:54.190> than<00:06:54.370> B<00:06:54.690> so<00:06:55.690> basically<00:06:56.470> like<00:06:56.710> if 00:06:56.850 --> 00:06:56.860 align:start position:0% more defined than B so basically like if 00:06:56.860 --> 00:06:57.900 align:start position:0% more defined than B so basically like if I<00:06:56.950> have<00:06:57.100> a<00:06:57.130> definition<00:06:57.610> it's<00:06:57.700> got<00:06:57.820> some 00:06:57.900 --> 00:06:57.910 align:start position:0% I have a definition it's got some 00:06:57.910 --> 00:06:59.490 align:start position:0% I have a definition it's got some undefined<00:06:58.300> term<00:06:58.510> in<00:06:58.660> it<00:06:58.750> and<00:06:58.900> I<00:06:58.990> can<00:06:59.140> replace 00:06:59.490 --> 00:06:59.500 align:start position:0% undefined term in it and I can replace 00:06:59.500 --> 00:07:01.350 align:start position:0% undefined term in it and I can replace it<00:06:59.530> to<00:07:00.160> get<00:07:00.280> some<00:07:00.400> other<00:07:00.520> definition<00:07:00.910> then 00:07:01.350 --> 00:07:01.360 align:start position:0% it to get some other definition then 00:07:01.360 --> 00:07:02.790 align:start position:0% it to get some other definition then that<00:07:01.510> other<00:07:01.600> definition<00:07:02.050> is<00:07:02.140> more<00:07:02.410> defined 00:07:02.790 --> 00:07:02.800 align:start position:0% that other definition is more defined 00:07:02.800 --> 00:07:06.300 align:start position:0% that other definition is more defined than<00:07:02.980> this<00:07:03.220> like<00:07:03.370> initial<00:07:03.790> definition<00:07:04.360> so<00:07:05.350> I'm 00:07:06.300 --> 00:07:06.310 align:start position:0% than this like initial definition so I'm 00:07:06.310 --> 00:07:09.930 align:start position:0% than this like initial definition so I'm gonna<00:07:06.490> give<00:07:06.640> some<00:07:06.670> examples<00:07:08.220> so<00:07:09.220> here<00:07:09.700> we<00:07:09.790> go 00:07:09.930 --> 00:07:09.940 align:start position:0% gonna give some examples so here we go 00:07:09.940 --> 00:07:12.330 align:start position:0% gonna give some examples so here we go you<00:07:10.540> know<00:07:10.630> bottom<00:07:11.110> times<00:07:11.350> bottom<00:07:11.440> is<00:07:11.950> more 00:07:12.330 --> 00:07:12.340 align:start position:0% you know bottom times bottom is more 00:07:12.340 --> 00:07:14.400 align:start position:0% you know bottom times bottom is more defined<00:07:12.670> than<00:07:12.850> bottom<00:07:13.270> because<00:07:14.140> you<00:07:14.260> can 00:07:14.400 --> 00:07:14.410 align:start position:0% defined than bottom because you can 00:07:14.410 --> 00:07:15.720 align:start position:0% defined than bottom because you can replace<00:07:14.740> bottom<00:07:15.100> with<00:07:15.220> bottom<00:07:15.490> times<00:07:15.640> bottom 00:07:15.720 --> 00:07:15.730 align:start position:0% replace bottom with bottom times bottom 00:07:15.730 --> 00:07:19.890 align:start position:0% replace bottom with bottom times bottom and<00:07:16.620> therefore<00:07:18.000> you<00:07:19.000> know<00:07:19.090> you<00:07:19.150> can<00:07:19.360> define 00:07:19.890 --> 00:07:19.900 align:start position:0% and therefore you know you can define 00:07:19.900 --> 00:07:21.540 align:start position:0% and therefore you know you can define something<00:07:20.380> there's<00:07:20.890> clearly<00:07:21.160> under<00:07:21.370> find 00:07:21.540 --> 00:07:21.550 align:start position:0% something there's clearly under find 00:07:21.550 --> 00:07:24.120 align:start position:0% something there's clearly under find bottom<00:07:21.880> to<00:07:22.330> be<00:07:22.540> this<00:07:23.380> thing<00:07:23.680> bottom<00:07:23.980> times 00:07:24.120 --> 00:07:24.130 align:start position:0% bottom to be this thing bottom times 00:07:24.130 --> 00:07:26.250 align:start position:0% bottom to be this thing bottom times bottom<00:07:24.220> which<00:07:24.550> is<00:07:24.960> still<00:07:25.960> not<00:07:25.990> totally 00:07:26.250 --> 00:07:26.260 align:start position:0% bottom which is still not totally 00:07:26.260 --> 00:07:28.560 align:start position:0% bottom which is still not totally defined<00:07:26.710> but<00:07:27.250> it's<00:07:27.400> more<00:07:27.700> defined<00:07:28.150> than<00:07:28.330> just 00:07:28.560 --> 00:07:28.570 align:start position:0% defined but it's more defined than just 00:07:28.570 --> 00:07:32.280 align:start position:0% defined but it's more defined than just bottom<00:07:29.670> you<00:07:30.670> know<00:07:30.760> bottom<00:07:31.270> times<00:07:31.570> empty<00:07:32.080> set 00:07:32.280 --> 00:07:32.290 align:start position:0% bottom you know bottom times empty set 00:07:32.290 --> 00:07:33.420 align:start position:0% bottom you know bottom times empty set is<00:07:32.320> more<00:07:32.620> defined<00:07:32.890> than<00:07:32.950> bottom<00:07:33.220> times<00:07:33.370> bottom 00:07:33.420 --> 00:07:33.430 align:start position:0% is more defined than bottom times bottom 00:07:33.430 --> 00:07:36.650 align:start position:0% is more defined than bottom times bottom because<00:07:33.970> you<00:07:34.120> can<00:07:34.300> replace<00:07:35.110> bottom<00:07:35.890> with 00:07:36.650 --> 00:07:36.660 align:start position:0% because you can replace bottom with 00:07:36.660 --> 00:07:39.510 align:start position:0% because you can replace bottom with empty<00:07:37.660> sets<00:07:37.900> and<00:07:38.050> get<00:07:38.560> from<00:07:39.070> bottom<00:07:39.370> times 00:07:39.510 --> 00:07:39.520 align:start position:0% empty sets and get from bottom times 00:07:39.520 --> 00:07:40.860 align:start position:0% empty sets and get from bottom times bottom<00:07:39.580> to<00:07:39.940> bottom<00:07:40.030> times<00:07:40.300> everything 00:07:40.860 --> 00:07:40.870 align:start position:0% bottom to bottom times everything 00:07:40.870 --> 00:07:44.720 align:start position:0% bottom to bottom times everything what<00:07:41.650> about<00:07:42.090> empty<00:07:43.090> set<00:07:43.270> times<00:07:43.570> bottom<00:07:43.810> vs. 00:07:44.720 --> 00:07:44.730 align:start position:0% what about empty set times bottom vs. 00:07:44.730 --> 00:07:47.310 align:start position:0% what about empty set times bottom vs. bottom<00:07:45.730> bottom<00:07:46.180> well<00:07:46.660> you<00:07:46.990> know<00:07:47.080> you<00:07:47.140> can 00:07:47.310 --> 00:07:47.320 align:start position:0% bottom bottom well you know you can 00:07:47.320 --> 00:07:48.540 align:start position:0% bottom bottom well you know you can place<00:07:47.470> the<00:07:47.590> first<00:07:47.770> bottom<00:07:48.040> with<00:07:48.130> an<00:07:48.220> empty<00:07:48.400> set 00:07:48.540 --> 00:07:48.550 align:start position:0% place the first bottom with an empty set 00:07:48.550 --> 00:07:50.940 align:start position:0% place the first bottom with an empty set and<00:07:48.700> so<00:07:48.850> the<00:07:49.270> thing<00:07:49.630> on<00:07:49.720> the<00:07:49.750> left<00:07:49.840> is<00:07:50.080> more 00:07:50.940 --> 00:07:50.950 align:start position:0% and so the thing on the left is more 00:07:50.950 --> 00:07:52.740 align:start position:0% and so the thing on the left is more defined<00:07:51.220> than<00:07:51.430> the<00:07:51.520> thing<00:07:51.670> on<00:07:51.760> the<00:07:51.820> right<00:07:51.910> but 00:07:52.740 --> 00:07:52.750 align:start position:0% defined than the thing on the right but 00:07:52.750 --> 00:07:54.360 align:start position:0% defined than the thing on the right but the<00:07:52.870> next<00:07:53.260> example<00:07:53.650> is<00:07:53.800> a<00:07:53.860> little<00:07:54.070> trickier 00:07:54.360 --> 00:07:54.370 align:start position:0% the next example is a little trickier 00:07:54.370 --> 00:07:57.660 align:start position:0% the next example is a little trickier because<00:07:55.020> it's<00:07:56.020> not<00:07:56.830> more<00:07:57.070> defined<00:07:57.430> than<00:07:57.550> the 00:07:57.660 --> 00:07:57.670 align:start position:0% because it's not more defined than the 00:07:57.670 --> 00:08:00.870 align:start position:0% because it's not more defined than the thing<00:07:57.880> on<00:07:58.000> the<00:07:58.090> left<00:07:58.300> sorry<00:07:59.140> the<00:07:59.740> empty<00:08:00.670> set 00:08:00.870 --> 00:08:00.880 align:start position:0% thing on the left sorry the empty set 00:08:00.880 --> 00:08:03.830 align:start position:0% thing on the left sorry the empty set times<00:08:01.270> bottom<00:08:01.540> is<00:08:01.900> not<00:08:02.380> more<00:08:02.560> defined<00:08:02.860> then 00:08:03.830 --> 00:08:03.840 align:start position:0% times bottom is not more defined then 00:08:03.840 --> 00:08:07.560 align:start position:0% times bottom is not more defined then empty<00:08:04.840> set<00:08:05.020> times<00:08:05.850> bottom<00:08:06.850> times<00:08:07.150> empty<00:08:07.390> set 00:08:07.560 --> 00:08:07.570 align:start position:0% empty set times bottom times empty set 00:08:07.570 --> 00:08:10.770 align:start position:0% empty set times bottom times empty set because<00:08:07.750> you<00:08:08.560> can't<00:08:08.770> replace<00:08:08.920> the<00:08:09.160> bottom<00:08:09.780> to 00:08:10.770 --> 00:08:10.780 align:start position:0% because you can't replace the bottom to 00:08:10.780 --> 00:08:12.930 align:start position:0% because you can't replace the bottom to get<00:08:11.160> empty<00:08:12.160> set<00:08:12.280> times<00:08:12.430> bottom<00:08:12.580> because 00:08:12.930 --> 00:08:12.940 align:start position:0% get empty set times bottom because 00:08:12.940 --> 00:08:14.070 align:start position:0% get empty set times bottom because there's<00:08:13.060> already<00:08:13.210> in<00:08:13.390> it<00:08:13.510> empty<00:08:13.780> set<00:08:13.900> in<00:08:13.960> that 00:08:14.070 --> 00:08:14.080 align:start position:0% there's already in it empty set in that 00:08:14.080 --> 00:08:16.080 align:start position:0% there's already in it empty set in that position<00:08:14.200> so<00:08:14.800> you<00:08:15.280> know<00:08:15.400> basically<00:08:15.760> what 00:08:16.080 --> 00:08:16.090 align:start position:0% position so you know basically what 00:08:16.090 --> 00:08:17.760 align:start position:0% position so you know basically what we're<00:08:16.660> doing<00:08:16.690> is<00:08:16.870> replacing<00:08:17.110> the<00:08:17.350> bottoms<00:08:17.650> on 00:08:17.760 --> 00:08:17.770 align:start position:0% we're doing is replacing the bottoms on 00:08:17.770 --> 00:08:18.990 align:start position:0% we're doing is replacing the bottoms on the<00:08:17.860> right<00:08:18.010> to<00:08:18.280> see<00:08:18.430> if<00:08:18.490> we<00:08:18.580> can<00:08:18.670> get<00:08:18.790> the<00:08:18.850> thing 00:08:18.990 --> 00:08:19.000 align:start position:0% the right to see if we can get the thing 00:08:19.000 --> 00:08:21.660 align:start position:0% the right to see if we can get the thing on<00:08:19.090> the<00:08:19.150> left<00:08:19.210> and<00:08:19.630> if<00:08:19.960> we<00:08:20.080> can't<00:08:20.410> then<00:08:20.680> it's 00:08:21.660 --> 00:08:21.670 align:start position:0% on the left and if we can't then it's 00:08:21.670 --> 00:08:22.650 align:start position:0% on the left and if we can't then it's not<00:08:21.790> more<00:08:22.000> to<00:08:22.120> fine<00:08:22.300> then 00:08:22.650 --> 00:08:22.660 align:start position:0% not more to fine then 00:08:22.660 --> 00:08:24.870 align:start position:0% not more to fine then and<00:08:22.750> if<00:08:23.200> it<00:08:23.350> if<00:08:23.680> we<00:08:23.860> can<00:08:24.100> then<00:08:24.370> it<00:08:24.460> is<00:08:24.550> more<00:08:24.790> to 00:08:24.870 --> 00:08:24.880 align:start position:0% and if it if we can then it is more to 00:08:24.880 --> 00:08:27.450 align:start position:0% and if it if we can then it is more to find<00:08:25.090> them<00:08:25.270> so<00:08:26.110> at<00:08:26.500> the<00:08:26.710> end<00:08:26.830> of<00:08:26.890> the<00:08:27.010> day<00:08:27.190> where 00:08:27.450 --> 00:08:27.460 align:start position:0% find them so at the end of the day where 00:08:27.460 --> 00:08:30.330 align:start position:0% find them so at the end of the day where we<00:08:27.550> kind<00:08:27.760> of<00:08:27.820> get<00:08:28.030> is<00:08:28.350> this<00:08:29.350> picture<00:08:30.190> this 00:08:30.330 --> 00:08:30.340 align:start position:0% we kind of get is this picture this 00:08:30.340 --> 00:08:33.320 align:start position:0% we kind of get is this picture this partial<00:08:30.790> order<00:08:31.060> of<00:08:31.240> the<00:08:31.660> defined<00:08:32.440> Earnest<00:08:32.770> of 00:08:33.320 --> 00:08:33.330 align:start position:0% partial order of the defined Earnest of 00:08:33.330 --> 00:08:37.290 align:start position:0% partial order of the defined Earnest of these<00:08:34.330> terms<00:08:35.110> so<00:08:35.380> like<00:08:36.220> bottom<00:08:36.760> is<00:08:36.940> the<00:08:37.150> most 00:08:37.290 --> 00:08:37.300 align:start position:0% these terms so like bottom is the most 00:08:37.300 --> 00:08:39.000 align:start position:0% these terms so like bottom is the most undefined<00:08:37.960> bottom<00:08:38.470> times<00:08:38.620> bottom<00:08:38.680> is<00:08:38.950> a 00:08:39.000 --> 00:08:39.010 align:start position:0% undefined bottom times bottom is a 00:08:39.010 --> 00:08:42.690 align:start position:0% undefined bottom times bottom is a little<00:08:39.190> more<00:08:39.430> defined<00:08:40.620> these<00:08:41.620> two<00:08:41.890> terms<00:08:42.250> left 00:08:42.690 --> 00:08:42.700 align:start position:0% little more defined these two terms left 00:08:42.700 --> 00:08:44.340 align:start position:0% little more defined these two terms left and<00:08:42.880> right<00:08:43.060> there<00:08:43.390> no<00:08:43.750> more<00:08:43.960> defined<00:08:44.229> than 00:08:44.340 --> 00:08:44.350 align:start position:0% and right there no more defined than 00:08:44.350 --> 00:08:46.140 align:start position:0% and right there no more defined than each<00:08:44.470> other<00:08:44.680> even<00:08:44.920> though<00:08:45.190> they<00:08:45.310> have<00:08:45.490> a<00:08:45.520> term 00:08:46.140 --> 00:08:46.150 align:start position:0% each other even though they have a term 00:08:46.150 --> 00:08:49.560 align:start position:0% each other even though they have a term that<00:08:46.420> is<00:08:46.600> in<00:08:47.110> common<00:08:47.950> I<00:08:48.130> mean<00:08:48.160> a<00:08:48.460> term<00:08:48.730> that<00:08:48.760> if 00:08:49.560 --> 00:08:49.570 align:start position:0% that is in common I mean a term that if 00:08:49.570 --> 00:08:51.850 align:start position:0% that is in common I mean a term that if both<00:08:50.020> of<00:08:50.050> them<00:08:50.320> can<00:08:50.560> define 00:08:51.850 --> 00:08:51.860 align:start position:0% both of them can define 00:08:51.860 --> 00:08:54.310 align:start position:0% both of them can define that<00:08:52.280> you<00:08:52.490> know<00:08:52.580> a<00:08:53.060> term<00:08:53.600> that<00:08:53.750> inhabits<00:08:54.140> both 00:08:54.310 --> 00:08:54.320 align:start position:0% that you know a term that inhabits both 00:08:54.320 --> 00:08:57.430 align:start position:0% that you know a term that inhabits both of<00:08:54.470> these<00:08:54.560> partial<00:08:54.860> definitions<00:08:55.630> and<00:08:56.630> so<00:08:57.230> kind 00:08:57.430 --> 00:08:57.440 align:start position:0% of these partial definitions and so kind 00:08:57.440 --> 00:08:59.440 align:start position:0% of these partial definitions and so kind of<00:08:57.530> you<00:08:57.890> know<00:08:58.010> what<00:08:58.430> we<00:08:58.550> do<00:08:58.730> in<00:08:58.940> the<00:08:59.120> correct<00:08:59.360> by 00:08:59.440 --> 00:08:59.450 align:start position:0% of you know what we do in the correct by 00:08:59.450 --> 00:09:00.940 align:start position:0% of you know what we do in the correct by construction<00:08:59.780> process<00:09:00.170> is<00:09:00.320> we<00:09:00.440> move<00:09:00.680> from 00:09:00.940 --> 00:09:00.950 align:start position:0% construction process is we move from 00:09:00.950 --> 00:09:03.490 align:start position:0% construction process is we move from less<00:09:01.280> defined<00:09:01.640> protocol<00:09:02.260> specifications<00:09:03.260> to 00:09:03.490 --> 00:09:03.500 align:start position:0% less defined protocol specifications to 00:09:03.500 --> 00:09:05.920 align:start position:0% less defined protocol specifications to more<00:09:03.770> defined<00:09:04.160> protocol<00:09:04.490> specifications<00:09:05.150> we 00:09:05.920 --> 00:09:05.930 align:start position:0% more defined protocol specifications we 00:09:05.930 --> 00:09:10.540 align:start position:0% more defined protocol specifications we have<00:09:06.760> a<00:09:08.020> kind<00:09:09.020> of<00:09:09.080> process<00:09:09.530> of<00:09:09.860> we<00:09:10.280> say 00:09:10.540 --> 00:09:10.550 align:start position:0% have a kind of process of we say 00:09:10.550 --> 00:09:11.920 align:start position:0% have a kind of process of we say something<00:09:10.970> about<00:09:11.210> the<00:09:11.360> protocol<00:09:11.690> that<00:09:11.810> we 00:09:11.920 --> 00:09:11.930 align:start position:0% something about the protocol that we 00:09:11.930 --> 00:09:13.660 align:start position:0% something about the protocol that we prove<00:09:12.170> things<00:09:12.290> about<00:09:12.530> protocol<00:09:12.860> so<00:09:13.640> that 00:09:13.660 --> 00:09:13.670 align:start position:0% prove things about protocol so that 00:09:13.670 --> 00:09:15.190 align:start position:0% prove things about protocol so that later<00:09:14.030> when<00:09:14.270> we<00:09:14.300> continue<00:09:14.780> to<00:09:14.870> define<00:09:15.080> the 00:09:15.190 --> 00:09:15.200 align:start position:0% later when we continue to define the 00:09:15.200 --> 00:09:17.730 align:start position:0% later when we continue to define the protocol<00:09:15.560> the<00:09:16.070> things<00:09:16.310> that<00:09:16.490> we<00:09:16.610> proved 00:09:17.730 --> 00:09:17.740 align:start position:0% protocol the things that we proved 00:09:17.740 --> 00:09:19.870 align:start position:0% protocol the things that we proved continue<00:09:18.740> to<00:09:18.830> holds<00:09:19.160> because<00:09:19.400> all<00:09:19.580> of<00:09:19.610> the 00:09:19.870 --> 00:09:19.880 align:start position:0% continue to holds because all of the 00:09:19.880 --> 00:09:21.790 align:start position:0% continue to holds because all of the later<00:09:20.180> definitions<00:09:20.810> are<00:09:20.930> just<00:09:21.080> a<00:09:21.200> they're 00:09:21.790 --> 00:09:21.800 align:start position:0% later definitions are just a they're 00:09:21.800 --> 00:09:23.530 align:start position:0% later definitions are just a they're just<00:09:21.980> a<00:09:22.040> refinement<00:09:22.790> of<00:09:22.880> the<00:09:23.000> previous 00:09:23.530 --> 00:09:23.540 align:start position:0% just a refinement of the previous 00:09:23.540 --> 00:09:26.950 align:start position:0% just a refinement of the previous definition<00:09:23.680> you<00:09:24.680> know<00:09:24.800> so<00:09:25.340> you<00:09:26.120> know<00:09:26.210> so<00:09:26.660> the 00:09:26.950 --> 00:09:26.960 align:start position:0% definition you know so you know so the 00:09:26.960 --> 00:09:29.560 align:start position:0% definition you know so you know so the the<00:09:27.260> kind<00:09:27.500> of<00:09:27.880> theorems<00:09:28.880> that<00:09:29.030> we<00:09:29.120> have<00:09:29.330> for 00:09:29.560 --> 00:09:29.570 align:start position:0% the kind of theorems that we have for 00:09:29.570 --> 00:09:31.120 align:start position:0% the kind of theorems that we have for less<00:09:29.780> defined<00:09:30.140> versions<00:09:30.500> of<00:09:30.680> the<00:09:30.770> protocol 00:09:31.120 --> 00:09:31.130 align:start position:0% less defined versions of the protocol 00:09:31.130 --> 00:09:32.710 align:start position:0% less defined versions of the protocol spec<00:09:31.370> are<00:09:31.520> going<00:09:31.640> to<00:09:31.700> hold<00:09:31.970> for<00:09:32.210> more<00:09:32.390> defined 00:09:32.710 --> 00:09:32.720 align:start position:0% spec are going to hold for more defined 00:09:32.720 --> 00:09:34.240 align:start position:0% spec are going to hold for more defined versions<00:09:33.020> of<00:09:33.140> the<00:09:33.230> spec<00:09:33.410> and<00:09:33.560> this<00:09:33.980> kind<00:09:34.190> of 00:09:34.240 --> 00:09:34.250 align:start position:0% versions of the spec and this kind of 00:09:34.250 --> 00:09:37.180 align:start position:0% versions of the spec and this kind of starts<00:09:35.120> to<00:09:35.180> make<00:09:35.870> you<00:09:35.930> feel<00:09:36.230> why<00:09:36.470> we<00:09:36.800> have<00:09:36.950> like 00:09:37.180 --> 00:09:37.190 align:start position:0% starts to make you feel why we have like 00:09:37.190 --> 00:09:38.770 align:start position:0% starts to make you feel why we have like this<00:09:37.310> correct<00:09:37.580> by<00:09:37.670> construction<00:09:38.090> protocol 00:09:38.770 --> 00:09:38.780 align:start position:0% this correct by construction protocol 00:09:38.780 --> 00:09:41.020 align:start position:0% this correct by construction protocol design<00:09:39.560> because<00:09:39.920> at<00:09:40.340> some<00:09:40.640> point<00:09:40.850> we're<00:09:40.970> gonna 00:09:41.020 --> 00:09:41.030 align:start position:0% design because at some point we're gonna 00:09:41.030 --> 00:09:43.600 align:start position:0% design because at some point we're gonna have<00:09:41.150> a<00:09:41.540> partial<00:09:42.260> spec<00:09:42.500> and<00:09:42.740> some<00:09:43.100> proofs<00:09:43.340> and 00:09:43.600 --> 00:09:43.610 align:start position:0% have a partial spec and some proofs and 00:09:43.610 --> 00:09:45.910 align:start position:0% have a partial spec and some proofs and then<00:09:44.360> there's<00:09:44.540> no<00:09:44.660> way<00:09:44.870> for<00:09:44.930> us<00:09:45.170> to<00:09:45.230> define 00:09:45.910 --> 00:09:45.920 align:start position:0% then there's no way for us to define 00:09:45.920 --> 00:09:48.070 align:start position:0% then there's no way for us to define that<00:09:46.100> spec<00:09:46.400> more<00:09:46.670> that<00:09:47.540> will<00:09:47.720> kill<00:09:47.930> those 00:09:48.070 --> 00:09:48.080 align:start position:0% that spec more that will kill those 00:09:48.080 --> 00:09:54.570 align:start position:0% that spec more that will kill those proofs<00:09:50.170> so<00:09:52.600> basically<00:09:53.600> like<00:09:53.960> our<00:09:54.110> kind<00:09:54.320> of 00:09:54.570 --> 00:09:54.580 align:start position:0% proofs so basically like our kind of 00:09:54.580 --> 00:09:57.220 align:start position:0% proofs so basically like our kind of strategies<00:09:55.580> to<00:09:55.610> like<00:09:56.120> deliberately<00:09:56.720> give<00:09:57.050> and 00:09:57.220 --> 00:09:57.230 align:start position:0% strategies to like deliberately give and 00:09:57.230 --> 00:10:00.790 align:start position:0% strategies to like deliberately give and Peru<00:09:57.440> or<00:09:57.740> give<00:09:58.750> partial<00:09:59.750> specifications<00:10:00.590> and 00:10:00.790 --> 00:10:00.800 align:start position:0% Peru or give partial specifications and 00:10:00.800 --> 00:10:01.720 align:start position:0% Peru or give partial specifications and prove<00:10:01.040> things<00:10:01.190> about<00:10:01.490> partial 00:10:01.720 --> 00:10:01.730 align:start position:0% prove things about partial 00:10:01.730 --> 00:10:03.970 align:start position:0% prove things about partial specifications<00:10:02.480> so<00:10:03.170> that<00:10:03.200> we<00:10:03.440> can<00:10:03.590> have<00:10:03.770> a<00:10:03.800> lot 00:10:03.970 --> 00:10:03.980 align:start position:0% specifications so that we can have a lot 00:10:03.980 --> 00:10:06.580 align:start position:0% specifications so that we can have a lot of<00:10:04.010> flexibility<00:10:04.670> in<00:10:04.880> our<00:10:05.600> iteration<00:10:06.440> and 00:10:06.580 --> 00:10:06.590 align:start position:0% of flexibility in our iteration and 00:10:06.590 --> 00:10:09.160 align:start position:0% of flexibility in our iteration and design<00:10:06.920> because<00:10:07.760> we<00:10:07.790> can<00:10:08.120> continue<00:10:08.780> to<00:10:08.900> define 00:10:09.160 --> 00:10:09.170 align:start position:0% design because we can continue to define 00:10:09.170 --> 00:10:10.600 align:start position:0% design because we can continue to define from<00:10:09.410> that<00:10:09.620> point<00:10:09.860> in<00:10:10.130> many<00:10:10.400> different 00:10:10.600 --> 00:10:10.610 align:start position:0% from that point in many different 00:10:10.610 --> 00:10:12.550 align:start position:0% from that point in many different directions<00:10:10.850> without<00:10:11.810> having<00:10:12.020> to<00:10:12.110> worry<00:10:12.350> and 00:10:12.550 --> 00:10:12.560 align:start position:0% directions without having to worry and 00:10:12.560 --> 00:10:16.750 align:start position:0% directions without having to worry and go<00:10:12.710> back<00:10:12.920> about<00:10:13.390> you<00:10:14.390> know<00:10:15.550> verifying<00:10:16.550> and 00:10:16.750 --> 00:10:16.760 align:start position:0% go back about you know verifying and 00:10:16.760 --> 00:10:20.200 align:start position:0% go back about you know verifying and changing<00:10:17.120> proofs<00:10:17.390> that<00:10:18.340> you<00:10:19.340> know<00:10:19.460> because<00:10:20.030> of 00:10:20.200 --> 00:10:20.210 align:start position:0% changing proofs that you know because of 00:10:20.210 --> 00:10:21.730 align:start position:0% changing proofs that you know because of the<00:10:20.330> change<00:10:20.630> in<00:10:20.780> the<00:10:20.840> protocol<00:10:21.200> so<00:10:21.440> like<00:10:21.560> a<00:10:21.620> lot 00:10:21.730 --> 00:10:21.740 align:start position:0% the change in the protocol so like a lot 00:10:21.740 --> 00:10:22.900 align:start position:0% the change in the protocol so like a lot of<00:10:21.770> the<00:10:21.890> time<00:10:22.010> when<00:10:22.160> you<00:10:22.220> have<00:10:22.340> a<00:10:22.370> protocol<00:10:22.760> and 00:10:22.900 --> 00:10:22.910 align:start position:0% of the time when you have a protocol and 00:10:22.910 --> 00:10:23.830 align:start position:0% of the time when you have a protocol and you<00:10:22.940> make<00:10:23.090> a<00:10:23.120> change<00:10:23.360> you're<00:10:23.570> gonna<00:10:23.630> have<00:10:23.780> to 00:10:23.830 --> 00:10:23.840 align:start position:0% you make a change you're gonna have to 00:10:23.840 --> 00:10:25.000 align:start position:0% you make a change you're gonna have to like<00:10:23.990> change<00:10:24.020> the<00:10:24.500> proofs<00:10:24.710> that<00:10:24.770> you<00:10:24.920> have 00:10:25.000 --> 00:10:25.010 align:start position:0% like change the proofs that you have 00:10:25.010 --> 00:10:27.100 align:start position:0% like change the proofs that you have about<00:10:25.160> protocol<00:10:25.550> but<00:10:26.120> if<00:10:26.240> you<00:10:26.390> instead<00:10:26.840> has 00:10:27.100 --> 00:10:27.110 align:start position:0% about protocol but if you instead has 00:10:27.110 --> 00:10:29.620 align:start position:0% about protocol but if you instead has some<00:10:27.700> partial<00:10:28.700> definition<00:10:29.150> of<00:10:29.270> the<00:10:29.330> protocol 00:10:29.620 --> 00:10:29.630 align:start position:0% some partial definition of the protocol 00:10:29.630 --> 00:10:31.720 align:start position:0% some partial definition of the protocol that<00:10:29.780> you<00:10:29.840> had<00:10:29.930> two<00:10:30.020> proofs<00:10:30.260> from<00:10:30.380> which<00:10:31.040> you 00:10:31.720 --> 00:10:31.730 align:start position:0% that you had two proofs from which you 00:10:31.730 --> 00:10:32.950 align:start position:0% that you had two proofs from which you could<00:10:31.880> change<00:10:32.150> and<00:10:32.480> you<00:10:32.570> can<00:10:32.690> make<00:10:32.840> your 00:10:32.950 --> 00:10:32.960 align:start position:0% could change and you can make your 00:10:32.960 --> 00:10:34.390 align:start position:0% could change and you can make your change<00:10:33.230> to<00:10:33.470> your<00:10:33.560> protocol<00:10:33.920> by<00:10:34.040> just<00:10:34.220> read 00:10:34.390 --> 00:10:34.400 align:start position:0% change to your protocol by just read 00:10:34.400 --> 00:10:36.790 align:start position:0% change to your protocol by just read continuing<00:10:35.300> to<00:10:35.390> define<00:10:35.750> the<00:10:36.380> protocol<00:10:36.770> just 00:10:36.790 --> 00:10:36.800 align:start position:0% continuing to define the protocol just 00:10:36.800 --> 00:10:38.920 align:start position:0% continuing to define the protocol just like<00:10:37.100> in<00:10:37.190> a<00:10:37.250> different<00:10:37.370> way<00:10:37.640> from<00:10:37.700> before<00:10:38.240> then 00:10:38.920 --> 00:10:38.930 align:start position:0% like in a different way from before then 00:10:38.930 --> 00:10:40.390 align:start position:0% like in a different way from before then you<00:10:39.050> can<00:10:39.230> you<00:10:39.500> know<00:10:39.560> not<00:10:39.890> have<00:10:40.190> this 00:10:40.390 --> 00:10:40.400 align:start position:0% you can you know not have this 00:10:40.400 --> 00:10:42.850 align:start position:0% you can you know not have this additional<00:10:40.790> proof<00:10:40.970> obligation<00:10:41.620> because<00:10:42.620> you 00:10:42.850 --> 00:10:42.860 align:start position:0% additional proof obligation because you 00:10:42.860 --> 00:10:45.790 align:start position:0% additional proof obligation because you just<00:10:43.510> have<00:10:44.510> proven<00:10:45.020> it<00:10:45.170> for<00:10:45.410> a<00:10:45.440> much<00:10:45.590> broader 00:10:45.790 --> 00:10:45.800 align:start position:0% just have proven it for a much broader 00:10:45.800 --> 00:10:48.430 align:start position:0% just have proven it for a much broader class<00:10:46.070> of<00:10:46.220> things<00:10:46.490> which<00:10:47.480> are<00:10:47.720> kind<00:10:48.020> of<00:10:48.080> the 00:10:48.430 --> 00:10:48.440 align:start position:0% class of things which are kind of the 00:10:48.440 --> 00:10:50.800 align:start position:0% class of things which are kind of the things<00:10:48.770> that<00:10:49.100> inhabit<00:10:49.730> this<00:10:49.940> less<00:10:50.360> well 00:10:50.800 --> 00:10:50.810 align:start position:0% things that inhabit this less well 00:10:50.810 --> 00:10:54.340 align:start position:0% things that inhabit this less well specified<00:10:51.530> definition<00:10:52.280> of<00:10:52.370> the<00:10:52.430> protocol<00:10:53.350> so 00:10:54.340 --> 00:10:54.350 align:start position:0% specified definition of the protocol so 00:10:54.350 --> 00:10:57.400 align:start position:0% specified definition of the protocol so let's<00:10:55.240> so<00:10:56.240> you<00:10:56.480> know<00:10:56.690> I<00:10:56.720> think<00:10:57.020> we<00:10:57.140> can<00:10:57.230> get<00:10:57.380> a 00:10:57.400 --> 00:10:57.410 align:start position:0% let's so you know I think we can get a 00:10:57.410 --> 00:11:02.180 align:start position:0% let's so you know I think we can get a lot<00:10:57.680> of<00:10:58.690> flexibility<00:10:59.690> in<00:10:59.840> design 00:11:02.180 --> 00:11:02.190 align:start position:0% lot of flexibility in design 00:11:02.190 --> 00:11:04.610 align:start position:0% lot of flexibility in design because<00:11:02.580> we<00:11:02.730> because<00:11:03.300> of<00:11:03.330> this<00:11:03.590> because<00:11:04.590> of 00:11:04.610 --> 00:11:04.620 align:start position:0% because we because of this because of 00:11:04.620 --> 00:11:08.960 align:start position:0% because we because of this because of this<00:11:04.740> approach<00:11:05.070> i<00:11:05.340> so<00:11:06.330> here<00:11:06.480> is<00:11:06.860> some<00:11:07.970> actual 00:11:08.960 --> 00:11:08.970 align:start position:0% this approach i so here is some actual 00:11:08.970 --> 00:11:11.120 align:start position:0% this approach i so here is some actual like<00:11:09.510> partial<00:11:10.050> order<00:11:10.230> of<00:11:10.320> defining<00:11:10.770> this<00:11:10.980> in 00:11:11.120 --> 00:11:11.130 align:start position:0% like partial order of defining this in 00:11:11.130 --> 00:11:12.860 align:start position:0% like partial order of defining this in like<00:11:11.340> some<00:11:11.580> definitions<00:11:12.210> that<00:11:12.390> we<00:11:12.480> have<00:11:12.630> in 00:11:12.860 --> 00:11:12.870 align:start position:0% like some definitions that we have in 00:11:12.870 --> 00:11:16.370 align:start position:0% like some definitions that we have in the<00:11:13.500> casper<00:11:14.160> cbc<00:11:14.580> casper<00:11:14.880> world<00:11:15.120> so<00:11:15.930> we<00:11:16.200> have 00:11:16.370 --> 00:11:16.380 align:start position:0% the casper cbc casper world so we have 00:11:16.380 --> 00:11:19.670 align:start position:0% the casper cbc casper world so we have this<00:11:17.540> minimal<00:11:18.540> cbc<00:11:18.960> casper<00:11:19.290> family<00:11:19.590> of 00:11:19.670 --> 00:11:19.680 align:start position:0% this minimal cbc casper family of 00:11:19.680 --> 00:11:23.500 align:start position:0% this minimal cbc casper family of protocols<00:11:20.630> which<00:11:21.630> is<00:11:21.810> like<00:11:22.020> the 00:11:23.500 --> 00:11:23.510 align:start position:0% protocols which is like the 00:11:23.510 --> 00:11:25.250 align:start position:0% protocols which is like the specification<00:11:24.510> it's<00:11:24.630> like<00:11:24.720> the<00:11:24.810> easiest<00:11:24.930> to 00:11:25.250 --> 00:11:25.260 align:start position:0% specification it's like the easiest to 00:11:25.260 --> 00:11:27.200 align:start position:0% specification it's like the easiest to understand<00:11:25.710> the<00:11:25.920> smallest<00:11:26.250> the<00:11:26.550> few<00:11:26.730> fewest 00:11:27.200 --> 00:11:27.210 align:start position:0% understand the smallest the few fewest 00:11:27.210 --> 00:11:31.430 align:start position:0% understand the smallest the few fewest parts<00:11:27.830> and<00:11:28.830> we<00:11:29.450> defined<00:11:30.450> terms<00:11:31.110> in<00:11:31.410> that 00:11:31.430 --> 00:11:31.440 align:start position:0% parts and we defined terms in that 00:11:31.440 --> 00:11:33.320 align:start position:0% parts and we defined terms in that specification<00:11:32.280> to<00:11:32.430> define<00:11:32.730> like<00:11:32.880> the<00:11:33.000> binary 00:11:33.320 --> 00:11:33.330 align:start position:0% specification to define like the binary 00:11:33.330 --> 00:11:34.400 align:start position:0% specification to define like the binary consensus<00:11:33.690> for<00:11:33.810> all<00:11:34.020> the<00:11:34.110> block<00:11:34.260> chain 00:11:34.400 --> 00:11:34.410 align:start position:0% consensus for all the block chain 00:11:34.410 --> 00:11:36.950 align:start position:0% consensus for all the block chain consensus<00:11:34.830> protocol<00:11:35.480> and<00:11:36.480> other<00:11:36.720> cuz<00:11:36.840> it's 00:11:36.950 --> 00:11:36.960 align:start position:0% consensus protocol and other cuz it's 00:11:36.960 --> 00:11:38.090 align:start position:0% consensus protocol and other cuz it's protocols<00:11:37.350> that<00:11:37.440> you've<00:11:37.590> seen<00:11:37.830> if<00:11:37.980> you've 00:11:38.090 --> 00:11:38.100 align:start position:0% protocols that you've seen if you've 00:11:38.100 --> 00:11:40.880 align:start position:0% protocols that you've seen if you've watched<00:11:38.700> me<00:11:38.940> present<00:11:39.270> on<00:11:39.390> cbc<00:11:39.720> casper<00:11:40.050> over 00:11:40.880 --> 00:11:40.890 align:start position:0% watched me present on cbc casper over 00:11:40.890 --> 00:11:44.180 align:start position:0% watched me present on cbc casper over the<00:11:41.130> years<00:11:41.750> and<00:11:42.750> so<00:11:43.170> all<00:11:43.440> of<00:11:43.500> these<00:11:43.770> protocols 00:11:44.180 --> 00:11:44.190 align:start position:0% the years and so all of these protocols 00:11:44.190 --> 00:11:46.700 align:start position:0% the years and so all of these protocols these<00:11:44.640> three<00:11:44.940> protocols<00:11:45.480> the<00:11:46.110> binary 00:11:46.700 --> 00:11:46.710 align:start position:0% these three protocols the binary 00:11:46.710 --> 00:11:49.040 align:start position:0% these three protocols the binary consensus<00:11:47.130> protocol<00:11:47.520> the<00:11:47.760> integer<00:11:48.210> and<00:11:48.480> the 00:11:49.040 --> 00:11:49.050 align:start position:0% consensus protocol the integer and the 00:11:49.050 --> 00:11:54.290 align:start position:0% consensus protocol the integer and the friendly<00:11:49.680> ghost<00:11:49.920> they're<00:11:50.490> all<00:11:52.880> more<00:11:53.880> defined 00:11:54.290 --> 00:11:54.300 align:start position:0% friendly ghost they're all more defined 00:11:54.300 --> 00:11:56.230 align:start position:0% friendly ghost they're all more defined than<00:11:54.630> the<00:11:54.720> minimal<00:11:55.110> CBC<00:11:55.590> casper 00:11:56.230 --> 00:11:56.240 align:start position:0% than the minimal CBC casper 00:11:56.240 --> 00:11:59.660 align:start position:0% than the minimal CBC casper specification<00:11:57.240> and<00:11:57.590> they<00:11:58.590> all<00:11:58.860> satisfy<00:11:59.370> the 00:11:59.660 --> 00:11:59.670 align:start position:0% specification and they all satisfy the 00:11:59.670 --> 00:12:01.790 align:start position:0% specification and they all satisfy the same<00:11:59.880> proof<00:12:00.180> as<00:12:00.450> the<00:12:00.990> minimal<00:12:01.290> CBC<00:12:01.620> caste 00:12:01.790 --> 00:12:01.800 align:start position:0% same proof as the minimal CBC caste 00:12:01.800 --> 00:12:07.400 align:start position:0% same proof as the minimal CBC caste respect<00:12:02.190> and<00:12:03.320> these<00:12:04.320> these<00:12:04.920> all<00:12:06.260> therefore<00:12:07.260> we 00:12:07.400 --> 00:12:07.410 align:start position:0% respect and these these all therefore we 00:12:07.410 --> 00:12:08.900 align:start position:0% respect and these these all therefore we kind<00:12:07.800> of<00:12:07.890> benefit<00:12:08.310> from<00:12:08.400> that<00:12:08.520> proof<00:12:08.730> and<00:12:08.850> we 00:12:08.900 --> 00:12:08.910 align:start position:0% kind of benefit from that proof and we 00:12:08.910 --> 00:12:10.550 align:start position:0% kind of benefit from that proof and we don't<00:12:09.060> need<00:12:09.240> to<00:12:09.330> look<00:12:09.450> back<00:12:09.660> much<00:12:09.990> when<00:12:10.320> we<00:12:10.380> do 00:12:10.550 --> 00:12:10.560 align:start position:0% don't need to look back much when we do 00:12:10.560 --> 00:12:13.160 align:start position:0% don't need to look back much when we do when<00:12:11.280> we're<00:12:11.430> defining<00:12:11.640> forward<00:12:12.180> from<00:12:12.900> this 00:12:13.160 --> 00:12:13.170 align:start position:0% when we're defining forward from this 00:12:13.170 --> 00:12:14.600 align:start position:0% when we're defining forward from this minimal<00:12:13.470> CBC<00:12:13.770> Casper<00:12:14.040> family<00:12:14.280> we<00:12:14.370> don't<00:12:14.460> need 00:12:14.600 --> 00:12:14.610 align:start position:0% minimal CBC Casper family we don't need 00:12:14.610 --> 00:12:16.490 align:start position:0% minimal CBC Casper family we don't need to<00:12:14.700> look<00:12:14.880> back<00:12:15.150> and<00:12:15.450> ask<00:12:15.930> about<00:12:16.260> what<00:12:16.350> that 00:12:16.490 --> 00:12:16.500 align:start position:0% to look back and ask about what that 00:12:16.500 --> 00:12:20.330 align:start position:0% to look back and ask about what that proof<00:12:16.710> will<00:12:16.920> continue<00:12:17.460> to<00:12:17.520> be<00:12:17.610> satisfied<00:12:19.340> but 00:12:20.330 --> 00:12:20.340 align:start position:0% proof will continue to be satisfied but 00:12:20.340 --> 00:12:22.280 align:start position:0% proof will continue to be satisfied but you<00:12:20.700> know<00:12:20.790> this<00:12:21.030> this<00:12:21.300> this<00:12:21.660> family<00:12:22.200> of 00:12:22.280 --> 00:12:22.290 align:start position:0% you know this this this family of 00:12:22.290 --> 00:12:25.910 align:start position:0% you know this this this family of protocols<00:12:22.470> actually<00:12:23.070> has<00:12:23.810> a<00:12:24.810> full<00:12:25.770> note 00:12:25.910 --> 00:12:25.920 align:start position:0% protocols actually has a full note 00:12:25.920 --> 00:12:27.260 align:start position:0% protocols actually has a full note condition<00:12:26.340> it<00:12:26.460> requires<00:12:26.760> that<00:12:26.970> all<00:12:27.090> the 00:12:27.260 --> 00:12:27.270 align:start position:0% condition it requires that all the 00:12:27.270 --> 00:12:29.450 align:start position:0% condition it requires that all the messages<00:12:27.540> all<00:12:27.870> the<00:12:27.900> nodes<00:12:28.200> processes<00:12:28.890> all<00:12:29.070> the 00:12:29.450 --> 00:12:29.460 align:start position:0% messages all the nodes processes all the 00:12:29.460 --> 00:12:31.130 align:start position:0% messages all the nodes processes all the justifications<00:12:30.090> of<00:12:30.150> all<00:12:30.270> their<00:12:30.360> messages<00:12:30.690> and 00:12:31.130 --> 00:12:31.140 align:start position:0% justifications of all their messages and 00:12:31.140 --> 00:12:33.230 align:start position:0% justifications of all their messages and so<00:12:31.740> that's<00:12:31.920> actually<00:12:32.220> not<00:12:32.340> super<00:12:32.700> useful<00:12:32.730> for 00:12:33.230 --> 00:12:33.240 align:start position:0% so that's actually not super useful for 00:12:33.240 --> 00:12:35.720 align:start position:0% so that's actually not super useful for example<00:12:33.780> for<00:12:34.020> sharding<00:12:34.320> and<00:12:34.500> so<00:12:34.920> we<00:12:35.430> don't 00:12:35.720 --> 00:12:35.730 align:start position:0% example for sharding and so we don't 00:12:35.730 --> 00:12:37.430 align:start position:0% example for sharding and so we don't actually<00:12:35.910> want<00:12:36.240> to<00:12:36.330> have<00:12:36.390> to<00:12:36.630> define<00:12:36.960> sharding 00:12:37.430 --> 00:12:37.440 align:start position:0% actually want to have to define sharding 00:12:37.440 --> 00:12:41.200 align:start position:0% actually want to have to define sharding as<00:12:37.560> a<00:12:39.260> further<00:12:40.260> definition<00:12:40.860> of<00:12:41.010> this 00:12:41.200 --> 00:12:41.210 align:start position:0% as a further definition of this 00:12:41.210 --> 00:12:43.520 align:start position:0% as a further definition of this specification<00:12:42.210> because<00:12:42.870> it's<00:12:43.020> a<00:12:43.170> full<00:12:43.350> it 00:12:43.520 --> 00:12:43.530 align:start position:0% specification because it's a full it 00:12:43.530 --> 00:12:45.770 align:start position:0% specification because it's a full it requires<00:12:43.950> it's<00:12:44.160> full<00:12:44.310> note<00:12:44.460> condition<00:12:44.850> and<00:12:45.150> so 00:12:45.770 --> 00:12:45.780 align:start position:0% requires it's full note condition and so 00:12:45.780 --> 00:12:47.090 align:start position:0% requires it's full note condition and so actually<00:12:45.960> what<00:12:46.200> we<00:12:46.290> do<00:12:46.410> instead<00:12:46.620> is<00:12:46.770> we<00:12:46.950> have 00:12:47.090 --> 00:12:47.100 align:start position:0% actually what we do instead is we have 00:12:47.100 --> 00:12:50.150 align:start position:0% actually what we do instead is we have like<00:12:47.280> this<00:12:47.430> other<00:12:48.140> spec<00:12:49.140> which<00:12:49.740> is<00:12:49.860> like<00:12:50.040> this 00:12:50.150 --> 00:12:50.160 align:start position:0% like this other spec which is like this 00:12:50.160 --> 00:12:54.100 align:start position:0% like this other spec which is like this like<00:12:50.370> client<00:12:50.880> spec<00:12:51.530> which<00:12:52.550> you<00:12:53.550> know<00:12:53.640> where 00:12:54.100 --> 00:12:54.110 align:start position:0% like client spec which you know where 00:12:54.110 --> 00:12:56.270 align:start position:0% like client spec which you know where clients<00:12:55.110> don't<00:12:55.230> need<00:12:55.380> to<00:12:55.440> have<00:12:55.590> all<00:12:55.830> of<00:12:56.100> the 00:12:56.270 --> 00:12:56.280 align:start position:0% clients don't need to have all of the 00:12:56.280 --> 00:12:59.660 align:start position:0% clients don't need to have all of the just<00:12:57.000> all<00:12:57.300> of<00:12:57.570> the<00:12:58.160> resolve<00:12:59.160> all<00:12:59.280> the<00:12:59.370> pointers 00:12:59.660 --> 00:12:59.670 align:start position:0% just all of the resolve all the pointers 00:12:59.670 --> 00:13:02.570 align:start position:0% just all of the resolve all the pointers and<00:12:59.820> all<00:12:59.910> their<00:13:00.030> messages<00:13:00.330> and<00:13:00.540> so<00:13:01.380> we<00:13:01.590> and<00:13:02.430> we 00:13:02.570 --> 00:13:02.580 align:start position:0% and all their messages and so we and we 00:13:02.580 --> 00:13:05.420 align:start position:0% and all their messages and so we and we define<00:13:02.940> the<00:13:03.710> started<00:13:04.710> watching<00:13:05.040> says 00:13:05.420 --> 00:13:05.430 align:start position:0% define the started watching says 00:13:05.430 --> 00:13:07.370 align:start position:0% define the started watching says protocol<00:13:05.790> spec<00:13:06.060> as<00:13:06.270> an<00:13:06.660> instance<00:13:07.050> of<00:13:07.200> this 00:13:07.370 --> 00:13:07.380 align:start position:0% protocol spec as an instance of this 00:13:07.380 --> 00:13:09.380 align:start position:0% protocol spec as an instance of this like<00:13:07.590> CB<00:13:07.890> light<00:13:08.160> client<00:13:08.460> CBC<00:13:08.880> family 00:13:09.380 --> 00:13:09.390 align:start position:0% like CB light client CBC family 00:13:09.390 --> 00:13:11.000 align:start position:0% like CB light client CBC family protocols<00:13:09.810> which<00:13:09.990> all<00:13:10.110> satisfy<00:13:10.590> the<00:13:10.650> same 00:13:11.000 --> 00:13:11.010 align:start position:0% protocols which all satisfy the same 00:13:11.010 --> 00:13:12.440 align:start position:0% protocols which all satisfy the same because<00:13:11.520> that's<00:13:11.700> a<00:13:11.730> safety<00:13:11.910> proof<00:13:12.150> and 00:13:12.440 --> 00:13:12.450 align:start position:0% because that's a safety proof and 00:13:12.450 --> 00:13:14.790 align:start position:0% because that's a safety proof and actually<00:13:12.960> there's<00:13:13.140> like<00:13:13.320> a<00:13:13.350> more<00:13:13.680> abstract 00:13:14.790 --> 00:13:14.800 align:start position:0% actually there's like a more abstract 00:13:14.800 --> 00:13:17.019 align:start position:0% actually there's like a more abstract family<00:13:15.800> of<00:13:15.889> protocols<00:13:16.279> which<00:13:16.339> is<00:13:16.550> you<00:13:16.910> know 00:13:17.019 --> 00:13:17.029 align:start position:0% family of protocols which is you know 00:13:17.029 --> 00:13:18.999 align:start position:0% family of protocols which is you know considerably<00:13:17.779> harder<00:13:17.990> to<00:13:18.259> communicate<00:13:18.470> than 00:13:18.999 --> 00:13:19.009 align:start position:0% considerably harder to communicate than 00:13:19.009 --> 00:13:22.090 align:start position:0% considerably harder to communicate than the<00:13:19.129> minimal<00:13:19.459> one<00:13:19.660> but<00:13:20.660> which<00:13:20.839> is<00:13:21.230> less 00:13:22.090 --> 00:13:22.100 align:start position:0% the minimal one but which is less 00:13:22.100 --> 00:13:23.650 align:start position:0% the minimal one but which is less defined<00:13:22.490> than<00:13:22.699> both<00:13:22.910> the<00:13:23.180> light<00:13:23.329> client 00:13:23.650 --> 00:13:23.660 align:start position:0% defined than both the light client 00:13:23.660 --> 00:13:26.050 align:start position:0% defined than both the light client protocol<00:13:24.050> and<00:13:24.290> the<00:13:24.829> minimal<00:13:25.430> CBC<00:13:25.759> Casper 00:13:26.050 --> 00:13:26.060 align:start position:0% protocol and the minimal CBC Casper 00:13:26.060 --> 00:13:29.470 align:start position:0% protocol and the minimal CBC Casper protocol<00:13:26.449> and<00:13:26.690> so<00:13:27.379> like<00:13:27.589> if<00:13:27.800> we<00:13:28.240> with<00:13:29.240> with 00:13:29.470 --> 00:13:29.480 align:start position:0% protocol and so like if we with with 00:13:29.480 --> 00:13:31.329 align:start position:0% protocol and so like if we with with this<00:13:29.629> kind<00:13:29.810> of<00:13:29.870> set<00:13:30.139> up<00:13:30.259> what<00:13:30.500> we<00:13:30.620> think<00:13:30.860> what 00:13:31.329 --> 00:13:31.339 align:start position:0% this kind of set up what we think what 00:13:31.339 --> 00:13:34.600 align:start position:0% this kind of set up what we think what this<00:13:31.550> does<00:13:31.730> is<00:13:31.879> it<00:13:32.000> gives<00:13:32.120> us<00:13:32.300> a<00:13:33.610> little 00:13:34.600 --> 00:13:34.610 align:start position:0% this does is it gives us a little 00:13:34.610 --> 00:13:37.449 align:start position:0% this does is it gives us a little roadmap<00:13:35.149> of<00:13:35.360> like<00:13:35.689> starting<00:13:36.379> from<00:13:36.500> where<00:13:36.769> like 00:13:37.449 --> 00:13:37.459 align:start position:0% roadmap of like starting from where like 00:13:37.459 --> 00:13:38.889 align:start position:0% roadmap of like starting from where like what<00:13:37.639> is<00:13:37.759> defined<00:13:37.910> and<00:13:38.269> what<00:13:38.329> properties<00:13:38.779> do 00:13:38.889 --> 00:13:38.899 align:start position:0% what is defined and what properties do 00:13:38.899 --> 00:13:40.179 align:start position:0% what is defined and what properties do you<00:13:38.930> have<00:13:39.139> and<00:13:39.350> if<00:13:39.410> you<00:13:39.500> go<00:13:39.649> downstream<00:13:40.040> from 00:13:40.179 --> 00:13:40.189 align:start position:0% you have and if you go downstream from 00:13:40.189 --> 00:13:41.889 align:start position:0% you have and if you go downstream from there<00:13:40.399> and<00:13:40.490> continue<00:13:40.759> to<00:13:40.879> find<00:13:41.029> stuff<00:13:41.300> you 00:13:41.889 --> 00:13:41.899 align:start position:0% there and continue to find stuff you 00:13:41.899 --> 00:13:44.170 align:start position:0% there and continue to find stuff you know<00:13:41.990> what<00:13:42.680> would<00:13:43.399> you<00:13:43.519> get<00:13:43.639> to<00:13:43.670> benefit<00:13:44.029> from 00:13:44.170 --> 00:13:44.180 align:start position:0% know what would you get to benefit from 00:13:44.180 --> 00:13:48.519 align:start position:0% know what would you get to benefit from and<00:13:44.480> so<00:13:45.290> it<00:13:45.439> can<00:13:46.189> be<00:13:46.279> really<00:13:47.230> you<00:13:48.230> know<00:13:48.290> I<00:13:48.470> think 00:13:48.519 --> 00:13:48.529 align:start position:0% and so it can be really you know I think 00:13:48.529 --> 00:13:51.759 align:start position:0% and so it can be really you know I think this<00:13:49.399> kind<00:13:49.519> of<00:13:49.610> notion<00:13:49.970> of<00:13:50.269> a<00:13:50.680> disorder<00:13:51.680> of 00:13:51.759 --> 00:13:51.769 align:start position:0% this kind of notion of a disorder of 00:13:51.769 --> 00:13:54.009 align:start position:0% this kind of notion of a disorder of define<00:13:52.069> Innes<00:13:52.339> and<00:13:52.490> of<00:13:52.790> progressively<00:13:53.480> giving 00:13:54.009 --> 00:13:54.019 align:start position:0% define Innes and of progressively giving 00:13:54.019 --> 00:13:55.090 align:start position:0% define Innes and of progressively giving more<00:13:54.199> and<00:13:54.230> more<00:13:54.439> defined<00:13:54.680> protocol 00:13:55.090 --> 00:13:55.100 align:start position:0% more and more defined protocol 00:13:55.100 --> 00:13:59.379 align:start position:0% more and more defined protocol specifications<00:13:55.959> is<00:13:56.959> very<00:13:57.199> very<00:13:58.269> very<00:13:59.269> very 00:13:59.379 --> 00:13:59.389 align:start position:0% specifications is very very very very 00:13:59.389 --> 00:14:01.360 align:start position:0% specifications is very very very very much<00:14:00.079> what<00:14:00.290> we're<00:14:00.410> doing<00:14:00.680> in<00:14:00.829> correct<00:14:01.279> by 00:14:01.360 --> 00:14:01.370 align:start position:0% much what we're doing in correct by 00:14:01.370 --> 00:14:03.730 align:start position:0% much what we're doing in correct by construction<00:14:01.639> protocol<00:14:02.060> design<00:14:02.740> because 00:14:03.730 --> 00:14:03.740 align:start position:0% construction protocol design because 00:14:03.740 --> 00:14:05.679 align:start position:0% construction protocol design because we're<00:14:04.040> engaged<00:14:04.339> in<00:14:04.790> the<00:14:04.879> process<00:14:05.089> of<00:14:05.360> defining 00:14:05.679 --> 00:14:05.689 align:start position:0% we're engaged in the process of defining 00:14:05.689 --> 00:14:08.590 align:start position:0% we're engaged in the process of defining something<00:14:06.050> and<00:14:06.350> we<00:14:07.029> start<00:14:08.029> we<00:14:08.180> don't<00:14:08.420> have<00:14:08.569> a 00:14:08.590 --> 00:14:08.600 align:start position:0% something and we start we don't have a 00:14:08.600 --> 00:14:10.569 align:start position:0% something and we start we don't have a full<00:14:08.810> definition<00:14:08.930> but<00:14:09.709> we<00:14:09.829> want<00:14:10.100> to<00:14:10.279> get<00:14:10.430> to<00:14:10.550> a 00:14:10.569 --> 00:14:10.579 align:start position:0% full definition but we want to get to a 00:14:10.579 --> 00:14:11.920 align:start position:0% full definition but we want to get to a point<00:14:10.730> where<00:14:10.910> we<00:14:11.000> do<00:14:11.120> have<00:14:11.269> a<00:14:11.300> definition<00:14:11.810> that 00:14:11.920 --> 00:14:11.930 align:start position:0% point where we do have a definition that 00:14:11.930 --> 00:14:13.600 align:start position:0% point where we do have a definition that satisfies<00:14:12.350> certain<00:14:12.470> properties<00:14:12.620> and<00:14:13.310> we<00:14:13.459> want 00:14:13.600 --> 00:14:13.610 align:start position:0% satisfies certain properties and we want 00:14:13.610 --> 00:14:14.710 align:start position:0% satisfies certain properties and we want to<00:14:13.670> know<00:14:13.759> that<00:14:13.790> the<00:14:14.029> process<00:14:14.389> that<00:14:14.509> which<00:14:14.629> we 00:14:14.710 --> 00:14:14.720 align:start position:0% to know that the process that which we 00:14:14.720 --> 00:14:16.449 align:start position:0% to know that the process that which we follow<00:14:14.930> will<00:14:15.560> guarantee<00:14:15.829> that<00:14:16.129> we<00:14:16.220> have<00:14:16.339> those 00:14:16.449 --> 00:14:16.459 align:start position:0% follow will guarantee that we have those 00:14:16.459 --> 00:14:20.559 align:start position:0% follow will guarantee that we have those properties<00:14:17.680> and<00:14:18.680> so<00:14:19.279> you<00:14:19.339> know<00:14:19.519> which<00:14:19.639> we<00:14:19.880> try 00:14:20.559 --> 00:14:20.569 align:start position:0% properties and so you know which we try 00:14:20.569 --> 00:14:23.019 align:start position:0% properties and so you know which we try to<00:14:20.600> have<00:14:20.930> it's<00:14:21.560> kind<00:14:21.800> of<00:14:21.889> a<00:14:22.100> disciplined 00:14:23.019 --> 00:14:23.029 align:start position:0% to have it's kind of a disciplined 00:14:23.029 --> 00:14:26.110 align:start position:0% to have it's kind of a disciplined approach<00:14:23.120> for<00:14:23.569> getting<00:14:23.600> them<00:14:24.639> one<00:14:25.639> step<00:14:25.970> at<00:14:26.089> a 00:14:26.110 --> 00:14:26.120 align:start position:0% approach for getting them one step at a 00:14:26.120 --> 00:14:26.410 align:start position:0% approach for getting them one step at a time 00:14:26.410 --> 00:14:26.420 align:start position:0% time 00:14:26.420 --> 00:14:27.850 align:start position:0% time and<00:14:26.689> where<00:14:26.959> we<00:14:27.170> don't<00:14:27.290> really<00:14:27.470> have<00:14:27.649> to<00:14:27.740> look 00:14:27.850 --> 00:14:27.860 align:start position:0% and where we don't really have to look 00:14:27.860 --> 00:14:32.530 align:start position:0% and where we don't really have to look back<00:14:28.899> so<00:14:30.310> but<00:14:31.310> you<00:14:31.490> know<00:14:31.579> it's<00:14:31.790> not<00:14:32.060> always<00:14:32.300> as 00:14:32.530 --> 00:14:32.540 align:start position:0% back so but you know it's not always as 00:14:32.540 --> 00:14:33.910 align:start position:0% back so but you know it's not always as straightforward<00:14:32.779> sometimes<00:14:33.290> we<00:14:33.589> have<00:14:33.740> like 00:14:33.910 --> 00:14:33.920 align:start position:0% straightforward sometimes we have like 00:14:33.920 --> 00:14:36.220 align:start position:0% straightforward sometimes we have like alternative<00:14:34.579> choices<00:14:34.970> of<00:14:35.180> what<00:14:35.449> how<00:14:35.810> exactly 00:14:36.220 --> 00:14:36.230 align:start position:0% alternative choices of what how exactly 00:14:36.230 --> 00:14:38.439 align:start position:0% alternative choices of what how exactly to<00:14:36.439> define<00:14:36.709> stuff<00:14:36.949> and<00:14:37.220> even<00:14:37.970> to<00:14:38.060> get<00:14:38.180> the<00:14:38.300> same 00:14:38.439 --> 00:14:38.449 align:start position:0% to define stuff and even to get the same 00:14:38.449 --> 00:14:42.160 align:start position:0% to define stuff and even to get the same goal<00:14:38.779> so<00:14:39.380> it's<00:14:40.180> you<00:14:41.180> know<00:14:41.300> I<00:14:41.329> painted<00:14:41.810> a<00:14:41.899> pretty 00:14:42.160 --> 00:14:42.170 align:start position:0% goal so it's you know I painted a pretty 00:14:42.170 --> 00:14:44.470 align:start position:0% goal so it's you know I painted a pretty simple<00:14:42.439> picture<00:14:42.740> but<00:14:42.920> the<00:14:43.130> reality<00:14:43.610> is<00:14:43.670> more 00:14:44.470 --> 00:14:44.480 align:start position:0% simple picture but the reality is more 00:14:44.480 --> 00:14:46.360 align:start position:0% simple picture but the reality is more complex<00:14:44.560> for<00:14:45.560> example<00:14:45.829> for<00:14:45.980> validated 00:14:46.360 --> 00:14:46.370 align:start position:0% complex for example for validated 00:14:46.370 --> 00:14:48.670 align:start position:0% complex for example for validated rotation<00:14:46.759> the<00:14:47.509> easy<00:14:47.899> thing<00:14:48.110> to<00:14:48.199> do<00:14:48.319> in<00:14:48.529> terms 00:14:48.670 --> 00:14:48.680 align:start position:0% rotation the easy thing to do in terms 00:14:48.680 --> 00:14:51.610 align:start position:0% rotation the easy thing to do in terms of<00:14:48.829> the<00:14:48.949> protocol<00:14:50.439> specification<00:14:51.439> and<00:14:51.529> the 00:14:51.610 --> 00:14:51.620 align:start position:0% of the protocol specification and the 00:14:51.620 --> 00:14:53.740 align:start position:0% of the protocol specification and the proof<00:14:51.800> obligations<00:14:52.279> is<00:14:52.430> to<00:14:52.459> just<00:14:52.699> launch<00:14:53.420> lots 00:14:53.740 --> 00:14:53.750 align:start position:0% proof obligations is to just launch lots 00:14:53.750 --> 00:14:55.449 align:start position:0% proof obligations is to just launch lots of<00:14:53.870> instances<00:14:54.199> of<00:14:54.500> these<00:14:54.589> protocols<00:14:55.310> that 00:14:55.449 --> 00:14:55.459 align:start position:0% of instances of these protocols that 00:14:55.459 --> 00:14:57.610 align:start position:0% of instances of these protocols that have<00:14:55.639> new<00:14:55.850> validator<00:14:56.209> sets<00:14:56.449> and<00:14:56.630> that<00:14:57.380> really 00:14:57.610 --> 00:14:57.620 align:start position:0% have new validator sets and that really 00:14:57.620 --> 00:15:00.009 align:start position:0% have new validator sets and that really can<00:14:57.860> work<00:14:58.069> in<00:14:58.279> some<00:14:58.399> cases<00:14:58.779> but<00:14:59.779> there<00:14:59.930> are 00:15:00.009 --> 00:15:00.019 align:start position:0% can work in some cases but there are 00:15:00.019 --> 00:15:01.540 align:start position:0% can work in some cases but there are also<00:15:00.110> cases<00:15:00.350> where<00:15:00.680> we<00:15:00.860> want<00:15:01.100> to<00:15:01.189> define 00:15:01.540 --> 00:15:01.550 align:start position:0% also cases where we want to define 00:15:01.550 --> 00:15:03.460 align:start position:0% also cases where we want to define protocols<00:15:02.059> that<00:15:02.269> do<00:15:02.360> validate<00:15:02.750> a<00:15:02.779> rotation<00:15:03.230> in 00:15:03.460 --> 00:15:03.470 align:start position:0% protocols that do validate a rotation in 00:15:03.470 --> 00:15:05.679 align:start position:0% protocols that do validate a rotation in a<00:15:03.829> way<00:15:03.920> that<00:15:04.100> is<00:15:04.189> outside<00:15:04.610> of<00:15:04.670> the<00:15:04.880> minimal<00:15:05.269> CBC 00:15:05.679 --> 00:15:05.689 align:start position:0% a way that is outside of the minimal CBC 00:15:05.689 --> 00:15:07.660 align:start position:0% a way that is outside of the minimal CBC Casper<00:15:06.050> framework 00:15:07.660 --> 00:15:07.670 align:start position:0% Casper framework 00:15:07.670 --> 00:15:10.720 align:start position:0% Casper framework and<00:15:07.910> whenever<00:15:08.630> we<00:15:08.809> do<00:15:09.220> this<00:15:10.220> kind<00:15:10.430> of<00:15:10.459> design 00:15:10.720 --> 00:15:10.730 align:start position:0% and whenever we do this kind of design 00:15:10.730 --> 00:15:12.429 align:start position:0% and whenever we do this kind of design that's<00:15:10.939> outside<00:15:11.360> of<00:15:11.569> the<00:15:11.660> of<00:15:11.990> the<00:15:12.110> framework 00:15:12.429 --> 00:15:12.439 align:start position:0% that's outside of the of the framework 00:15:12.439 --> 00:15:14.199 align:start position:0% that's outside of the of the framework we<00:15:13.100> need<00:15:13.220> to<00:15:13.339> do<00:15:13.399> we<00:15:13.550> create<00:15:13.759> new<00:15:14.000> proof 00:15:14.199 --> 00:15:14.209 align:start position:0% we need to do we create new proof 00:15:14.209 --> 00:15:17.530 align:start position:0% we need to do we create new proof obligations<00:15:14.839> and<00:15:15.019> so<00:15:15.680> we<00:15:16.670> sometimes<00:15:17.269> have<00:15:17.509> to 00:15:17.530 --> 00:15:17.540 align:start position:0% obligations and so we sometimes have to 00:15:17.540 --> 00:15:20.019 align:start position:0% obligations and so we sometimes have to have<00:15:17.809> a<00:15:17.839> choice<00:15:18.079> between<00:15:18.399> you<00:15:19.399> know<00:15:19.490> do<00:15:19.759> we<00:15:19.850> do 00:15:20.019 --> 00:15:20.029 align:start position:0% have a choice between you know do we do 00:15:20.029 --> 00:15:21.249 align:start position:0% have a choice between you know do we do we<00:15:20.089> design<00:15:20.420> things<00:15:20.689> and<00:15:20.870> way<00:15:21.019> to<00:15:21.079> take 00:15:21.249 --> 00:15:21.259 align:start position:0% we design things and way to take 00:15:21.259 --> 00:15:24.490 align:start position:0% we design things and way to take advantage<00:15:21.350> of<00:15:21.740> existing<00:15:22.509> proofs<00:15:23.509> or<00:15:23.779> do<00:15:24.350> we 00:15:24.490 --> 00:15:24.500 align:start position:0% advantage of existing proofs or do we 00:15:24.500 --> 00:15:27.189 align:start position:0% advantage of existing proofs or do we come<00:15:24.889> up<00:15:24.949> with<00:15:25.189> a<00:15:25.220> new<00:15:25.490> system<00:15:26.269> on<00:15:26.720> a<00:15:26.899> broader 00:15:27.189 --> 00:15:27.199 align:start position:0% come up with a new system on a broader 00:15:27.199 --> 00:15:28.480 align:start position:0% come up with a new system on a broader family<00:15:27.500> that 00:15:28.480 --> 00:15:28.490 align:start position:0% family that 00:15:28.490 --> 00:15:32.620 align:start position:0% family that or<00:15:28.940> that<00:15:29.810> have<00:15:30.110> other<00:15:30.410> proofs<00:15:30.740> and<00:15:31.010> it's<00:15:31.880> it's 00:15:32.620 --> 00:15:32.630 align:start position:0% or that have other proofs and it's it's 00:15:32.630 --> 00:15:33.970 align:start position:0% or that have other proofs and it's it's it's<00:15:32.900> tricky<00:15:33.230> because<00:15:33.350> like<00:15:33.590> on<00:15:33.680> the<00:15:33.770> one<00:15:33.860> hand 00:15:33.970 --> 00:15:33.980 align:start position:0% it's tricky because like on the one hand 00:15:33.980 --> 00:15:35.140 align:start position:0% it's tricky because like on the one hand we<00:15:34.070> want<00:15:34.220> to<00:15:34.250> benefit<00:15:34.520> from<00:15:34.580> other<00:15:34.820> folks<00:15:34.970> we 00:15:35.140 --> 00:15:35.150 align:start position:0% we want to benefit from other folks we 00:15:35.150 --> 00:15:36.370 align:start position:0% we want to benefit from other folks we already<00:15:35.570> have<00:15:35.720> and<00:15:35.900> we're<00:15:35.990> gonna<00:15:36.110> make<00:15:36.290> any 00:15:36.370 --> 00:15:36.380 align:start position:0% already have and we're gonna make any 00:15:36.380 --> 00:15:39.280 align:start position:0% already have and we're gonna make any new<00:15:36.560> ones<00:15:36.740> on<00:15:37.010> the<00:15:37.580> other<00:15:37.730> hand<00:15:38.020> when<00:15:39.020> we<00:15:39.110> have 00:15:39.280 --> 00:15:39.290 align:start position:0% new ones on the other hand when we have 00:15:39.290 --> 00:15:41.050 align:start position:0% new ones on the other hand when we have when<00:15:39.650> we<00:15:39.740> can<00:15:39.890> generalize<00:15:40.280> stuff<00:15:40.580> sometimes 00:15:41.050 --> 00:15:41.060 align:start position:0% when we can generalize stuff sometimes 00:15:41.060 --> 00:15:42.580 align:start position:0% when we can generalize stuff sometimes we<00:15:41.210> can<00:15:41.330> generalize<00:15:41.600> it<00:15:41.750> a<00:15:41.840> little<00:15:42.020> bit<00:15:42.350> and 00:15:42.580 --> 00:15:42.590 align:start position:0% we can generalize it a little bit and 00:15:42.590 --> 00:15:44.920 align:start position:0% we can generalize it a little bit and not<00:15:42.710> as<00:15:42.950> much<00:15:43.340> as<00:15:43.490> we'd<00:15:43.610> like<00:15:43.820> and<00:15:44.090> so<00:15:44.570> if<00:15:44.840> I 00:15:44.920 --> 00:15:44.930 align:start position:0% not as much as we'd like and so if I 00:15:44.930 --> 00:15:46.270 align:start position:0% not as much as we'd like and so if I come<00:15:45.110> up<00:15:45.140> with<00:15:45.320> a<00:15:45.350> more<00:15:45.530> general<00:15:45.590> family<00:15:46.160> of 00:15:46.270 --> 00:15:46.280 align:start position:0% come up with a more general family of 00:15:46.280 --> 00:15:47.740 align:start position:0% come up with a more general family of protocols<00:15:46.490> for<00:15:46.760> doing<00:15:46.940> validated<00:15:47.360> rotation 00:15:47.740 --> 00:15:47.750 align:start position:0% protocols for doing validated rotation 00:15:47.750 --> 00:15:49.210 align:start position:0% protocols for doing validated rotation for<00:15:48.020> example<00:15:48.320> like<00:15:48.710> I<00:15:48.770> haven't<00:15:49.010> come<00:15:49.100> up<00:15:49.160> with 00:15:49.210 --> 00:15:49.220 align:start position:0% for example like I haven't come up with 00:15:49.220 --> 00:15:50.830 align:start position:0% for example like I haven't come up with one<00:15:49.310> that<00:15:49.550> really<00:15:49.730> does<00:15:49.910> everything<00:15:50.510> I<00:15:50.630> want 00:15:50.830 --> 00:15:50.840 align:start position:0% one that really does everything I want 00:15:50.840 --> 00:15:53.140 align:start position:0% one that really does everything I want and<00:15:51.650> so<00:15:51.770> there's<00:15:52.040> there's<00:15:52.370> there's<00:15:52.640> there's 00:15:53.140 --> 00:15:53.150 align:start position:0% and so there's there's there's there's 00:15:53.150 --> 00:15:55.990 align:start position:0% and so there's there's there's there's definitely<00:15:53.740> it<00:15:54.740> definitely<00:15:55.160> isn't<00:15:55.310> as<00:15:55.550> simple 00:15:55.990 --> 00:15:56.000 align:start position:0% definitely it definitely isn't as simple 00:15:56.000 --> 00:15:58.450 align:start position:0% definitely it definitely isn't as simple as<00:15:56.180> like<00:15:56.210> you<00:15:57.080> know<00:15:57.110> define<00:15:57.650> as<00:15:57.860> you<00:15:57.980> go<00:15:58.190> and 00:15:58.450 --> 00:15:58.460 align:start position:0% as like you know define as you go and 00:15:58.460 --> 00:16:00.730 align:start position:0% as like you know define as you go and everything<00:15:58.820> will<00:15:59.000> be<00:15:59.030> fine<00:15:59.500> there's<00:16:00.500> real 00:16:00.730 --> 00:16:00.740 align:start position:0% everything will be fine there's real 00:16:00.740 --> 00:16:03.730 align:start position:0% everything will be fine there's real choices<00:16:01.160> that<00:16:01.250> we<00:16:01.340> need<00:16:01.460> to<00:16:01.550> make<00:16:01.730> and<00:16:02.690> like<00:16:02.900> in 00:16:03.730 --> 00:16:03.740 align:start position:0% choices that we need to make and like in 00:16:03.740 --> 00:16:06.610 align:start position:0% choices that we need to make and like in the<00:16:04.010> design<00:16:04.280> process<00:16:04.310> so<00:16:05.230> one<00:16:06.230> of<00:16:06.260> the 00:16:06.610 --> 00:16:06.620 align:start position:0% the design process so one of the 00:16:06.620 --> 00:16:09.720 align:start position:0% the design process so one of the decisions<00:16:07.070> we've<00:16:07.220> made<00:16:07.370> for<00:16:07.520> example<00:16:07.640> is<00:16:08.090> that 00:16:09.720 --> 00:16:09.730 align:start position:0% decisions we've made for example is that 00:16:09.730 --> 00:16:12.660 align:start position:0% decisions we've made for example is that validator<00:16:10.730> strategies<00:16:11.270> are<00:16:11.390> not<00:16:11.540> part<00:16:12.020> of<00:16:12.170> the 00:16:12.660 --> 00:16:12.670 align:start position:0% validator strategies are not part of the 00:16:12.670 --> 00:16:16.570 align:start position:0% validator strategies are not part of the specification<00:16:14.020> I<00:16:15.020> would<00:16:15.800> like<00:16:15.920> the<00:16:16.010> core<00:16:16.250> core 00:16:16.570 --> 00:16:16.580 align:start position:0% specification I would like the core core 00:16:16.580 --> 00:16:19.740 align:start position:0% specification I would like the core core like<00:16:16.940> the<00:16:17.260> you<00:16:18.260> know<00:16:18.380> the<00:16:18.560> core<00:16:18.830> partial<00:16:19.400> spec 00:16:19.740 --> 00:16:19.750 align:start position:0% like the you know the core partial spec 00:16:19.750 --> 00:16:23.950 align:start position:0% like the you know the core partial spec is<00:16:21.610> only<00:16:22.610> for<00:16:23.030> clients<00:16:23.450> it's<00:16:23.600> like<00:16:23.750> not<00:16:23.930> the 00:16:23.950 --> 00:16:23.960 align:start position:0% is only for clients it's like not the 00:16:23.960 --> 00:16:26.140 align:start position:0% is only for clients it's like not the spec<00:16:24.800> for<00:16:24.950> miners<00:16:25.280> or<00:16:25.490> for<00:16:25.670> people<00:16:25.940> who<00:16:26.000> make 00:16:26.140 --> 00:16:26.150 align:start position:0% spec for miners or for people who make 00:16:26.150 --> 00:16:27.400 align:start position:0% spec for miners or for people who make messages<00:16:26.600> as<00:16:26.720> people<00:16:26.960> for<00:16:27.140> people<00:16:27.350> who 00:16:27.400 --> 00:16:27.410 align:start position:0% messages as people for people who 00:16:27.410 --> 00:16:30.490 align:start position:0% messages as people for people who receive<00:16:27.710> them<00:16:28.240> and<00:16:29.240> and<00:16:29.630> the<00:16:29.960> reason<00:16:30.260> why<00:16:30.350> we 00:16:30.490 --> 00:16:30.500 align:start position:0% receive them and and the reason why we 00:16:30.500 --> 00:16:34.890 align:start position:0% receive them and and the reason why we did<00:16:30.680> this<00:16:30.770> is<00:16:30.950> because<00:16:30.980> there's<00:16:31.370> like<00:16:31.630> kind<00:16:32.630> of 00:16:34.890 --> 00:16:34.900 align:start position:0% 00:16:34.900 --> 00:16:38.710 align:start position:0% it<00:16:36.040> separates<00:16:37.040> out<00:16:37.220> the<00:16:37.610> parts<00:16:38.510> of<00:16:38.630> the 00:16:38.710 --> 00:16:38.720 align:start position:0% it separates out the parts of the 00:16:38.720 --> 00:16:40.360 align:start position:0% it separates out the parts of the protocol<00:16:39.140> in<00:16:39.320> a<00:16:39.530> way<00:16:39.650> that<00:16:39.830> allows<00:16:40.070> us<00:16:40.100> to 00:16:40.360 --> 00:16:40.370 align:start position:0% protocol in a way that allows us to 00:16:40.370 --> 00:16:42.480 align:start position:0% protocol in a way that allows us to tackle<00:16:40.550> them<00:16:40.790> separately<00:16:41.210> and<00:16:41.390> we<00:16:41.870> can<00:16:41.990> like 00:16:42.480 --> 00:16:42.490 align:start position:0% tackle them separately and we can like 00:16:42.490 --> 00:16:44.920 align:start position:0% tackle them separately and we can like independent<00:16:43.490> of<00:16:43.640> when<00:16:43.940> validators<00:16:44.750> make 00:16:44.920 --> 00:16:44.930 align:start position:0% independent of when validators make 00:16:44.930 --> 00:16:47.710 align:start position:0% independent of when validators make messages<00:16:45.440> or<00:16:45.890> how<00:16:46.430> validators<00:16:47.089> make<00:16:47.270> messages 00:16:47.710 --> 00:16:47.720 align:start position:0% messages or how validators make messages 00:16:47.720 --> 00:16:50.350 align:start position:0% messages or how validators make messages show<00:16:48.500> consensus<00:16:49.100> safety<00:16:49.370> so<00:16:49.970> we<00:16:50.000> have<00:16:50.270> this 00:16:50.350 --> 00:16:50.360 align:start position:0% show consensus safety so we have this 00:16:50.360 --> 00:16:53.020 align:start position:0% show consensus safety so we have this big<00:16:50.660> part<00:16:50.930> of<00:16:51.050> this<00:16:51.200> the<00:16:51.980> protocol<00:16:52.400> of<00:16:52.580> like 00:16:53.020 --> 00:16:53.030 align:start position:0% big part of this the protocol of like 00:16:53.030 --> 00:16:54.400 align:start position:0% big part of this the protocol of like when<00:16:53.270> do<00:16:53.480> you<00:16:53.540> know<00:16:53.690> it's<00:16:53.720> make<00:16:53.990> messages 00:16:54.400 --> 00:16:54.410 align:start position:0% when do you know it's make messages 00:16:54.410 --> 00:16:56.740 align:start position:0% when do you know it's make messages which<00:16:55.040> is<00:16:55.190> not<00:16:55.700> defined<00:16:56.120> in<00:16:56.270> the<00:16:56.300> course<00:16:56.540> back 00:16:56.740 --> 00:16:56.750 align:start position:0% which is not defined in the course back 00:16:56.750 --> 00:16:58.810 align:start position:0% which is not defined in the course back which<00:16:57.440> both<00:16:57.680> seems<00:16:58.070> weird<00:16:58.400> because<00:16:58.610> you'd 00:16:58.810 --> 00:16:58.820 align:start position:0% which both seems weird because you'd 00:16:58.820 --> 00:16:59.980 align:start position:0% which both seems weird because you'd expect<00:16:59.180> that<00:16:59.210> to<00:16:59.360> be<00:16:59.390> part<00:16:59.540> of<00:16:59.630> the<00:16:59.720> consensus 00:16:59.980 --> 00:16:59.990 align:start position:0% expect that to be part of the consensus 00:16:59.990 --> 00:17:01.540 align:start position:0% expect that to be part of the consensus protocol<00:17:00.260> but<00:17:00.770> it<00:17:00.830> also<00:17:00.920> is<00:17:01.130> really<00:17:01.160> nice 00:17:01.540 --> 00:17:01.550 align:start position:0% protocol but it also is really nice 00:17:01.550 --> 00:17:04.780 align:start position:0% protocol but it also is really nice because<00:17:01.900> there's<00:17:02.900> nothing<00:17:03.260> that<00:17:03.610> there's<00:17:04.610> no 00:17:04.780 --> 00:17:04.790 align:start position:0% because there's nothing that there's no 00:17:04.790 --> 00:17:06.220 align:start position:0% because there's nothing that there's no way<00:17:04.970> that<00:17:05.000> that<00:17:05.209> term<00:17:05.390> could<00:17:05.569> be<00:17:05.630> defined<00:17:06.020> in<00:17:06.170> a 00:17:06.220 --> 00:17:06.230 align:start position:0% way that that term could be defined in a 00:17:06.230 --> 00:17:10.660 align:start position:0% way that that term could be defined in a way<00:17:06.350> that<00:17:06.500> disrupts<00:17:07.069> the<00:17:07.640> proofs<00:17:08.030> in<00:17:08.329> the<00:17:09.670> for 00:17:10.660 --> 00:17:10.670 align:start position:0% way that disrupts the proofs in the for 00:17:10.670 --> 00:17:15.120 align:start position:0% way that disrupts the proofs in the for the<00:17:10.790> like<00:17:11.000> client<00:17:11.270> protocol<00:17:11.890> and<00:17:13.120> so 00:17:15.120 --> 00:17:15.130 align:start position:0% the like client protocol and so 00:17:15.130 --> 00:17:17.230 align:start position:0% the like client protocol and so validated<00:17:16.130> strategies<00:17:16.490> are<00:17:16.640> not<00:17:16.790> in<00:17:17.000> the<00:17:17.089> core 00:17:17.230 --> 00:17:17.240 align:start position:0% validated strategies are not in the core 00:17:17.240 --> 00:17:20.079 align:start position:0% validated strategies are not in the core the<00:17:17.660> core<00:17:17.810> partial<00:17:18.260> protocol<00:17:18.589> spec<00:17:18.770> and<00:17:19.040> I<00:17:19.760> and 00:17:20.079 --> 00:17:20.089 align:start position:0% the core partial protocol spec and I and 00:17:20.089 --> 00:17:21.400 align:start position:0% the core partial protocol spec and I and that<00:17:20.270> was<00:17:20.329> like<00:17:20.569> one<00:17:20.720> of<00:17:20.750> the<00:17:20.900> decisions<00:17:21.199> we 00:17:21.400 --> 00:17:21.410 align:start position:0% that was like one of the decisions we 00:17:21.410 --> 00:17:24.040 align:start position:0% that was like one of the decisions we made<00:17:21.680> and<00:17:22.030> deaf<00:17:23.030> I<00:17:23.300> definitely<00:17:23.750> don't<00:17:23.839> regret 00:17:24.040 --> 00:17:24.050 align:start position:0% made and deaf I definitely don't regret 00:17:24.050 --> 00:17:27.670 align:start position:0% made and deaf I definitely don't regret it<00:17:24.170> at<00:17:24.350> all<00:17:25.689> we<00:17:26.689> have<00:17:26.870> a<00:17:26.900> bunch<00:17:27.350> of<00:17:27.410> design 00:17:27.670 --> 00:17:27.680 align:start position:0% it at all we have a bunch of design 00:17:27.680 --> 00:17:29.320 align:start position:0% it at all we have a bunch of design decisions<00:17:28.100> that<00:17:28.160> are<00:17:28.339> motivated<00:17:28.820> by<00:17:28.850> economic 00:17:29.320 --> 00:17:29.330 align:start position:0% decisions that are motivated by economic 00:17:29.330 --> 00:17:31.870 align:start position:0% decisions that are motivated by economic thinking<00:17:29.680> but<00:17:30.680> also<00:17:30.710> at<00:17:31.280> the<00:17:31.370> same<00:17:31.490> time<00:17:31.700> we 00:17:31.870 --> 00:17:31.880 align:start position:0% thinking but also at the same time we 00:17:31.880 --> 00:17:34.570 align:start position:0% thinking but also at the same time we leave<00:17:32.090> incentives<00:17:32.630> undefined<00:17:33.110> until<00:17:33.590> very 00:17:34.570 --> 00:17:34.580 align:start position:0% leave incentives undefined until very 00:17:34.580 --> 00:17:36.160 align:start position:0% leave incentives undefined until very late<00:17:34.640> in<00:17:34.880> the<00:17:34.940> game<00:17:35.000> because<00:17:35.420> the<00:17:35.750> incentives 00:17:36.160 --> 00:17:36.170 align:start position:0% late in the game because the incentives 00:17:36.170 --> 00:17:38.080 align:start position:0% late in the game because the incentives have<00:17:36.290> to<00:17:36.470> respond<00:17:37.100> to<00:17:37.250> the<00:17:37.340> actual<00:17:37.670> states<00:17:38.000> of 00:17:38.080 --> 00:17:38.090 align:start position:0% have to respond to the actual states of 00:17:38.090 --> 00:17:41.060 align:start position:0% have to respond to the actual states of the<00:17:38.150> protocol<00:17:38.770> and<00:17:39.770> the<00:17:39.830> actual<00:17:40.250> and 00:17:41.060 --> 00:17:41.070 align:start position:0% the protocol and the actual and 00:17:41.070 --> 00:17:43.490 align:start position:0% the protocol and the actual and you<00:17:41.310> know<00:17:41.400> the<00:17:41.900> consensus<00:17:42.900> protocol<00:17:43.170> itself 00:17:43.490 --> 00:17:43.500 align:start position:0% you know the consensus protocol itself 00:17:43.500 --> 00:17:45.530 align:start position:0% you know the consensus protocol itself and<00:17:43.830> so<00:17:43.920> you<00:17:43.980> can't<00:17:44.340> actually<00:17:44.550> define<00:17:45.360> the 00:17:45.530 --> 00:17:45.540 align:start position:0% and so you can't actually define the 00:17:45.540 --> 00:17:46.940 align:start position:0% and so you can't actually define the incentives<00:17:45.960> until<00:17:46.200> the<00:17:46.320> consensus<00:17:46.650> protocol 00:17:46.940 --> 00:17:46.950 align:start position:0% incentives until the consensus protocol 00:17:46.950 --> 00:17:49.070 align:start position:0% incentives until the consensus protocol is<00:17:47.040> defined<00:17:47.370> and<00:17:47.550> so<00:17:48.090> although<00:17:48.300> we<00:17:48.510> do<00:17:48.660> a<00:17:48.690> lot 00:17:49.070 --> 00:17:49.080 align:start position:0% is defined and so although we do a lot 00:17:49.080 --> 00:17:50.600 align:start position:0% is defined and so although we do a lot of<00:17:49.110> thinking<00:17:49.410> economic<00:17:50.010> thing<00:17:50.130> in<00:17:50.310> front<00:17:50.490> and 00:17:50.600 --> 00:17:50.610 align:start position:0% of thinking economic thing in front and 00:17:50.610 --> 00:17:51.560 align:start position:0% of thinking economic thing in front and we<00:17:50.670> come<00:17:50.820> up<00:17:50.850> with<00:17:51.000> a<00:17:51.060> lot<00:17:51.210> of<00:17:51.240> disturb<00:17:51.480> you 00:17:51.560 --> 00:17:51.570 align:start position:0% we come up with a lot of disturb you 00:17:51.570 --> 00:17:53.120 align:start position:0% we come up with a lot of disturb you systems<00:17:51.840> properties<00:17:52.230> that<00:17:52.320> we<00:17:52.410> want<00:17:52.440> based<00:17:53.010> on 00:17:53.120 --> 00:17:53.130 align:start position:0% systems properties that we want based on 00:17:53.130 --> 00:17:59.900 align:start position:0% systems properties that we want based on the<00:17:53.190> economic<00:17:53.580> thinking<00:17:54.470> the<00:17:58.340> and<00:17:59.340> the<00:17:59.700> the 00:17:59.900 --> 00:17:59.910 align:start position:0% the economic thinking the and the the 00:17:59.910 --> 00:18:02.960 align:start position:0% the economic thinking the and the the the<00:18:00.090> the<00:18:00.840> definition<00:18:01.410> is<00:18:01.710> of<00:18:02.100> the<00:18:02.490> incentives 00:18:02.960 --> 00:18:02.970 align:start position:0% the the definition is of the incentives 00:18:02.970 --> 00:18:06.790 align:start position:0% the the definition is of the incentives is<00:18:03.090> left<00:18:03.300> for<00:18:03.450> later<00:18:03.920> so<00:18:04.920> you<00:18:05.220> know<00:18:05.340> we<00:18:06.180> have 00:18:06.790 --> 00:18:06.800 align:start position:0% is left for later so you know we have 00:18:06.800 --> 00:18:09.440 align:start position:0% is left for later so you know we have the<00:18:07.800> the<00:18:08.130> fault<00:18:08.340> tolerance<00:18:08.520> threshold<00:18:08.910> is<00:18:09.270> not 00:18:09.440 --> 00:18:09.450 align:start position:0% the the fault tolerance threshold is not 00:18:09.450 --> 00:18:11.180 align:start position:0% the the fault tolerance threshold is not specified<00:18:09.960> in<00:18:10.110> the<00:18:10.170> protocol<00:18:10.530> there's<00:18:11.010> like<00:18:11.160> a 00:18:11.180 --> 00:18:11.190 align:start position:0% specified in the protocol there's like a 00:18:11.190 --> 00:18:14.720 align:start position:0% specified in the protocol there's like a decision<00:18:11.610> we<00:18:11.730> made<00:18:11.910> and<00:18:12.120> like<00:18:12.380> very<00:18:13.380> like<00:18:14.070> you 00:18:14.720 --> 00:18:14.730 align:start position:0% decision we made and like very like you 00:18:14.730 --> 00:18:15.980 align:start position:0% decision we made and like very like you know<00:18:14.760> like<00:18:15.060> it<00:18:15.150> was<00:18:15.240> not<00:18:15.390> an<00:18:15.540> arbitrary 00:18:15.980 --> 00:18:15.990 align:start position:0% know like it was not an arbitrary 00:18:15.990 --> 00:18:18.200 align:start position:0% know like it was not an arbitrary decision<00:18:16.410> and<00:18:16.620> was<00:18:16.890> like<00:18:17.430> was<00:18:17.640> motivated<00:18:18.180> by 00:18:18.200 --> 00:18:18.210 align:start position:0% decision and was like was motivated by 00:18:18.210 --> 00:18:19.400 align:start position:0% decision and was like was motivated by like<00:18:18.420> the<00:18:18.510> design<00:18:18.780> requirements<00:18:19.230> that<00:18:19.320> we 00:18:19.400 --> 00:18:19.410 align:start position:0% like the design requirements that we 00:18:19.410 --> 00:18:25.670 align:start position:0% like the design requirements that we have<00:18:21.470> and<00:18:22.700> we<00:18:23.700> have<00:18:24.020> and<00:18:25.020> this<00:18:25.170> is<00:18:25.320> and<00:18:25.470> and 00:18:25.670 --> 00:18:25.680 align:start position:0% have and we have and this is and and 00:18:25.680 --> 00:18:29.510 align:start position:0% have and we have and this is and and this<00:18:25.800> is<00:18:25.920> like<00:18:26.070> an<00:18:26.190> area<00:18:26.460> where<00:18:27.980> it's<00:18:28.980> not<00:18:29.250> in 00:18:29.510 --> 00:18:29.520 align:start position:0% this is like an area where it's not in 00:18:29.520 --> 00:18:31.760 align:start position:0% this is like an area where it's not in the<00:18:29.850> core<00:18:30.120> reference<00:18:30.660> spec<00:18:30.990> but<00:18:31.440> we<00:18:31.560> have<00:18:31.740> a 00:18:31.760 --> 00:18:31.770 align:start position:0% the core reference spec but we have a 00:18:31.770 --> 00:18:34.220 align:start position:0% the core reference spec but we have a proof<00:18:32.070> for<00:18:32.280> how<00:18:32.400> noes<00:18:32.760> use<00:18:33.270> would<00:18:33.630> use<00:18:33.810> it<00:18:33.990> with 00:18:34.220 --> 00:18:34.230 align:start position:0% proof for how noes use would use it with 00:18:34.230 --> 00:18:35.540 align:start position:0% proof for how noes use would use it with different<00:18:34.470> fault<00:18:34.710> tolerance<00:18:34.800> thresholds<00:18:35.370> and 00:18:35.540 --> 00:18:35.550 align:start position:0% different fault tolerance thresholds and 00:18:35.550 --> 00:18:38.390 align:start position:0% different fault tolerance thresholds and so<00:18:36.240> we<00:18:36.390> can<00:18:36.540> without<00:18:36.900> changing<00:18:37.740> the<00:18:37.890> core<00:18:38.100> spec 00:18:38.390 --> 00:18:38.400 align:start position:0% so we can without changing the core spec 00:18:38.400 --> 00:18:41.540 align:start position:0% so we can without changing the core spec very<00:18:38.610> much<00:18:38.990> give<00:18:39.990> proofs<00:18:40.410> for<00:18:40.740> a<00:18:40.770> new<00:18:41.190> kind<00:18:41.460> of 00:18:41.540 --> 00:18:41.550 align:start position:0% very much give proofs for a new kind of 00:18:41.550 --> 00:18:45.650 align:start position:0% very much give proofs for a new kind of use<00:18:41.700> of<00:18:41.730> the<00:18:41.880> protocol<00:18:42.890> so<00:18:43.890> you<00:18:44.430> know<00:18:44.660> more 00:18:45.650 --> 00:18:45.660 align:start position:0% use of the protocol so you know more 00:18:45.660 --> 00:18:49.460 align:start position:0% use of the protocol so you know more kind<00:18:46.080> of<00:18:46.460> weird<00:18:47.460> proof<00:18:47.730> tactics<00:18:48.210> around<00:18:48.870> you 00:18:49.460 --> 00:18:49.470 align:start position:0% kind of weird proof tactics around you 00:18:49.470 --> 00:18:51.770 align:start position:0% kind of weird proof tactics around you know<00:18:49.760> using<00:18:50.760> multiple<00:18:51.090> instances<00:18:51.480> of<00:18:51.660> this 00:18:51.770 --> 00:18:51.780 align:start position:0% know using multiple instances of this 00:18:51.780 --> 00:18:53.960 align:start position:0% know using multiple instances of this like<00:18:52.020> correct<00:18:52.560> by<00:18:52.680> construction<00:18:53.070> core 00:18:53.960 --> 00:18:53.970 align:start position:0% like correct by construction core 00:18:53.970 --> 00:18:57.760 align:start position:0% like correct by construction core protocols<00:18:54.450> partial<00:18:54.960> spec<00:18:55.970> you<00:18:56.970> know<00:18:57.030> we<00:18:57.150> have 00:18:57.760 --> 00:18:57.770 align:start position:0% protocols partial spec you know we have 00:18:57.770 --> 00:19:00.080 align:start position:0% protocols partial spec you know we have preventing<00:18:58.770> das<00:18:58.980> will<00:18:59.310> require<00:18:59.700> like<00:19:00.000> you 00:19:00.080 --> 00:19:00.090 align:start position:0% preventing das will require like you 00:19:00.090 --> 00:19:01.580 align:start position:0% preventing das will require like you know<00:19:00.210> that<00:19:00.330> we<00:19:00.390> bound<00:19:00.600> the<00:19:00.990> amount<00:19:01.380> of<00:19:01.440> work 00:19:01.580 --> 00:19:01.590 align:start position:0% know that we bound the amount of work 00:19:01.590 --> 00:19:03.740 align:start position:0% know that we bound the amount of work required<00:19:01.620> to<00:19:02.130> process<00:19:02.640> a<00:19:02.820> message<00:19:03.450> and<00:19:03.660> that 00:19:03.740 --> 00:19:03.750 align:start position:0% required to process a message and that 00:19:03.750 --> 00:19:06.500 align:start position:0% required to process a message and that people<00:19:03.900> have<00:19:04.050> throttling<00:19:04.770> for<00:19:05.250> the<00:19:05.490> amount<00:19:06.420> of 00:19:06.500 --> 00:19:06.510 align:start position:0% people have throttling for the amount of 00:19:06.510 --> 00:19:09.890 align:start position:0% people have throttling for the amount of messages<00:19:06.630> that<00:19:06.930> they<00:19:07.550> can<00:19:08.550> receive<00:19:08.790> and<00:19:09.210> so 00:19:09.890 --> 00:19:09.900 align:start position:0% messages that they can receive and so 00:19:09.900 --> 00:19:11.870 align:start position:0% messages that they can receive and so that<00:19:10.050> is<00:19:10.260> that's<00:19:10.740> good<00:19:10.890> that<00:19:11.040> requires<00:19:11.370> a<00:19:11.610> new 00:19:11.870 --> 00:19:11.880 align:start position:0% that is that's good that requires a new 00:19:11.880 --> 00:19:13.730 align:start position:0% that is that's good that requires a new constraint<00:19:12.600> on<00:19:12.780> consensus<00:19:13.140> messages<00:19:13.530> it 00:19:13.730 --> 00:19:13.740 align:start position:0% constraint on consensus messages it 00:19:13.740 --> 00:19:15.200 align:start position:0% constraint on consensus messages it requires<00:19:14.070> new<00:19:14.430> strategies<00:19:14.910> for<00:19:14.940> the 00:19:15.200 --> 00:19:15.210 align:start position:0% requires new strategies for the 00:19:15.210 --> 00:19:17.090 align:start position:0% requires new strategies for the validators<00:19:15.660> none<00:19:16.110> of<00:19:16.230> this<00:19:16.350> stuff<00:19:16.590> is<00:19:16.740> part<00:19:16.950> of 00:19:17.090 --> 00:19:17.100 align:start position:0% validators none of this stuff is part of 00:19:17.100 --> 00:19:19.970 align:start position:0% validators none of this stuff is part of the<00:19:17.160> core<00:19:17.370> protocol<00:19:17.940> spec<00:19:18.620> none<00:19:19.620> of<00:19:19.740> it<00:19:19.860> is 00:19:19.970 --> 00:19:19.980 align:start position:0% the core protocol spec none of it is 00:19:19.980 --> 00:19:23.540 align:start position:0% the core protocol spec none of it is part<00:19:20.250> of<00:19:20.370> the<00:19:20.580> minimal<00:19:21.210> you<00:19:22.170> know<00:19:22.290> core<00:19:22.860> piece 00:19:23.540 --> 00:19:23.550 align:start position:0% part of the minimal you know core piece 00:19:23.550 --> 00:19:25.940 align:start position:0% part of the minimal you know core piece of<00:19:23.790> the<00:19:23.940> like<00:19:24.210> you<00:19:24.300> know<00:19:24.390> those<00:19:24.830> like<00:19:25.830> the 00:19:25.940 --> 00:19:25.950 align:start position:0% of the like you know those like the 00:19:25.950 --> 00:19:27.200 align:start position:0% of the like you know those like the start<00:19:26.190> of<00:19:26.310> the<00:19:26.400> correct<00:19:26.670> by<00:19:26.760> construction 00:19:27.200 --> 00:19:27.210 align:start position:0% start of the correct by construction 00:19:27.210 --> 00:19:29.780 align:start position:0% start of the correct by construction process<00:19:27.540> and<00:19:27.750> all<00:19:28.650> of<00:19:28.740> that<00:19:28.770> is<00:19:28.980> kind<00:19:29.250> of<00:19:29.310> very 00:19:29.780 --> 00:19:29.790 align:start position:0% process and all of that is kind of very 00:19:29.790 --> 00:19:32.930 align:start position:0% process and all of that is kind of very deliberate<00:19:30.680> because<00:19:31.680> the<00:19:32.400> idea<00:19:32.640> is<00:19:32.670> that<00:19:32.730> we 00:19:32.930 --> 00:19:32.940 align:start position:0% deliberate because the idea is that we 00:19:32.940 --> 00:19:35.390 align:start position:0% deliberate because the idea is that we can<00:19:33.120> define<00:19:33.360> this<00:19:33.960> stuff<00:19:34.350> later 00:19:35.390 --> 00:19:35.400 align:start position:0% can define this stuff later 00:19:35.400 --> 00:19:38.690 align:start position:0% can define this stuff later and<00:19:35.580> it's<00:19:36.210> more<00:19:36.720> than<00:19:36.900> fine<00:19:37.520> because<00:19:38.520> we 00:19:38.690 --> 00:19:38.700 align:start position:0% and it's more than fine because we 00:19:38.700 --> 00:19:40.070 align:start position:0% and it's more than fine because we didn't<00:19:38.970> screw<00:19:39.180> it<00:19:39.300> up<00:19:39.360> by<00:19:39.570> defining<00:19:39.840> it 00:19:40.070 --> 00:19:40.080 align:start position:0% didn't screw it up by defining it 00:19:40.080 --> 00:19:44.600 align:start position:0% didn't screw it up by defining it earlier<00:19:40.400> so<00:19:41.400> so<00:19:42.240> the<00:19:43.080> the<00:19:43.440> the<00:19:43.470> the<00:19:43.860> other<00:19:44.340> kind 00:19:44.600 --> 00:19:44.610 align:start position:0% earlier so so the the the the other kind 00:19:44.610 --> 00:19:48.320 align:start position:0% earlier so so the the the the other kind of<00:19:45.890> you<00:19:46.890> know<00:19:46.980> really<00:19:47.340> cool<00:19:47.580> thing<00:19:47.820> about<00:19:47.940> the 00:19:48.320 --> 00:19:48.330 align:start position:0% of you know really cool thing about the 00:19:48.330 --> 00:19:49.790 align:start position:0% of you know really cool thing about the crack<00:19:48.660> by<00:19:48.780> construction<00:19:49.110> approaches<00:19:49.620> the 00:19:49.790 --> 00:19:49.800 align:start position:0% crack by construction approaches the 00:19:49.800 --> 00:19:52.940 align:start position:0% crack by construction approaches the fact<00:19:50.580> that<00:19:50.670> you<00:19:50.850> can<00:19:51.200> iterate<00:19:52.200> actually<00:19:52.770> quite 00:19:52.940 --> 00:19:52.950 align:start position:0% fact that you can iterate actually quite 00:19:52.950 --> 00:19:54.390 align:start position:0% fact that you can iterate actually quite quickly 00:19:54.390 --> 00:19:54.400 align:start position:0% quickly 00:19:54.400 --> 00:19:55.770 align:start position:0% quickly without<00:19:54.850> having<00:19:55.150> because<00:19:55.419> you<00:19:55.480> don't<00:19:55.600> have<00:19:55.660> to 00:19:55.770 --> 00:19:55.780 align:start position:0% without having because you don't have to 00:19:55.780 --> 00:19:57.030 align:start position:0% without having because you don't have to reason<00:19:55.960> about<00:19:56.140> much<00:19:56.320> of<00:19:56.440> the<00:19:56.500> protocol<00:19:56.890> when 00:19:57.030 --> 00:19:57.040 align:start position:0% reason about much of the protocol when 00:19:57.040 --> 00:19:58.730 align:start position:0% reason about much of the protocol when you<00:19:57.130> make<00:19:57.280> changes<00:19:57.309> you<00:19:57.880> because<00:19:58.210> you 00:19:58.730 --> 00:19:58.740 align:start position:0% you make changes you because you 00:19:58.740 --> 00:20:02.039 align:start position:0% you make changes you because you literally<00:19:59.740> could<00:20:00.400> not<00:20:00.580> define<00:20:01.210> it<00:20:01.270> it<00:20:01.660> in<00:20:01.929> a 00:20:02.039 --> 00:20:02.049 align:start position:0% literally could not define it it in a 00:20:02.049 --> 00:20:05.250 align:start position:0% literally could not define it it in a way<00:20:02.140> that<00:20:02.169> screws<00:20:02.830> it<00:20:02.980> up<00:20:03.070> and<00:20:03.340> so<00:20:04.090> we<00:20:04.660> show<00:20:05.200> you 00:20:05.250 --> 00:20:05.260 align:start position:0% way that screws it up and so we show you 00:20:05.260 --> 00:20:06.630 align:start position:0% way that screws it up and so we show you some<00:20:05.530> of<00:20:05.620> the<00:20:05.799> progress<00:20:06.070> we've<00:20:06.250> made<00:20:06.280> in<00:20:06.429> the 00:20:06.630 --> 00:20:06.640 align:start position:0% some of the progress we've made in the 00:20:06.640 --> 00:20:09.090 align:start position:0% some of the progress we've made in the last<00:20:06.669> little<00:20:07.120> little<00:20:07.809> few<00:20:08.110> months<00:20:08.380> on<00:20:08.559> some<00:20:09.010> of 00:20:09.090 --> 00:20:09.100 align:start position:0% last little little few months on some of 00:20:09.100 --> 00:20:12.240 align:start position:0% last little little few months on some of the<00:20:09.160> charting<00:20:09.460> stuff<00:20:10.000> so<00:20:10.750> this<00:20:10.900> is<00:20:11.100> what<00:20:12.100> came 00:20:12.240 --> 00:20:12.250 align:start position:0% the charting stuff so this is what came 00:20:12.250 --> 00:20:15.299 align:start position:0% the charting stuff so this is what came out<00:20:12.370> of<00:20:12.549> the<00:20:12.880> East<00:20:13.030> Berlin<00:20:13.330> hackathon<00:20:13.950> we<00:20:14.950> came 00:20:15.299 --> 00:20:15.309 align:start position:0% out of the East Berlin hackathon we came 00:20:15.309 --> 00:20:18.870 align:start position:0% out of the East Berlin hackathon we came up<00:20:15.400> with<00:20:15.549> like<00:20:15.700> a<00:20:16.230> pair<00:20:17.230> of<00:20:17.260> shards<00:20:17.980> one<00:20:18.700> of 00:20:18.870 --> 00:20:18.880 align:start position:0% up with like a pair of shards one of 00:20:18.880 --> 00:20:20.400 align:start position:0% up with like a pair of shards one of which<00:20:19.030> kind<00:20:19.540> of<00:20:19.630> follows<00:20:20.020> the<00:20:20.140> other<00:20:20.260> one 00:20:20.400 --> 00:20:20.410 align:start position:0% which kind of follows the other one 00:20:20.410 --> 00:20:22.409 align:start position:0% which kind of follows the other one there's<00:20:20.650> very<00:20:21.460> it's<00:20:21.610> very<00:20:21.760> similar<00:20:21.970> to<00:20:22.150> the 00:20:22.409 --> 00:20:22.419 align:start position:0% there's very it's very similar to the 00:20:22.419 --> 00:20:25.260 align:start position:0% there's very it's very similar to the traditional<00:20:23.130> CBC<00:20:24.130> cast<00:20:24.309> burkas<00:20:24.669> protocol<00:20:25.059> in 00:20:25.260 --> 00:20:25.270 align:start position:0% traditional CBC cast burkas protocol in 00:20:25.270 --> 00:20:27.510 align:start position:0% traditional CBC cast burkas protocol in the<00:20:25.360> sense<00:20:25.540> that<00:20:25.600> like<00:20:25.720> it's<00:20:26.260> you<00:20:26.860> know<00:20:26.950> it's 00:20:27.510 --> 00:20:27.520 align:start position:0% the sense that like it's you know it's 00:20:27.520 --> 00:20:29.460 align:start position:0% the sense that like it's you know it's really<00:20:27.669> implemented 00:20:29.460 --> 00:20:29.470 align:start position:0% really implemented 00:20:29.470 --> 00:20:31.980 align:start position:0% really implemented completely<00:20:30.010> as<00:20:30.429> just<00:20:31.150> a<00:20:31.270> definition<00:20:31.510> and<00:20:31.929> a 00:20:31.980 --> 00:20:31.990 align:start position:0% completely as just a definition and a 00:20:31.990 --> 00:20:33.480 align:start position:0% completely as just a definition and a further<00:20:32.500> definition<00:20:32.919> that<00:20:32.980> protocol<00:20:33.340> by 00:20:33.480 --> 00:20:33.490 align:start position:0% further definition that protocol by 00:20:33.490 --> 00:20:35.280 align:start position:0% further definition that protocol by giving<00:20:33.850> the<00:20:34.179> consensus<00:20:34.600> values<00:20:34.929> and<00:20:35.230> the 00:20:35.280 --> 00:20:35.290 align:start position:0% giving the consensus values and the 00:20:35.290 --> 00:20:37.020 align:start position:0% giving the consensus values and the estimators<00:20:35.770> and<00:20:35.799> the<00:20:36.100> validators<00:20:36.700> and<00:20:36.910> their 00:20:37.020 --> 00:20:37.030 align:start position:0% estimators and the validators and their 00:20:37.030 --> 00:20:40.430 align:start position:0% estimators and the validators and their weights<00:20:37.240> and<00:20:37.540> the<00:20:37.600> fault<00:20:37.780> on<00:20:37.929> a<00:20:37.960> threshold<00:20:39.240> so 00:20:40.430 --> 00:20:40.440 align:start position:0% weights and the fault on a threshold so 00:20:40.440 --> 00:20:43.409 align:start position:0% weights and the fault on a threshold so so<00:20:41.440> so<00:20:41.740> we<00:20:42.040> did<00:20:42.160> this<00:20:42.280> binary<00:20:42.520> so<00:20:43.059> we<00:20:43.179> said<00:20:43.330> we 00:20:43.409 --> 00:20:43.419 align:start position:0% so so we did this binary so we said we 00:20:43.419 --> 00:20:48.210 align:start position:0% so so we did this binary so we said we did<00:20:43.570> this<00:20:43.630> to<00:20:43.840> two<00:20:44.140> shard<00:20:44.380> system<00:20:45.720> and<00:20:47.220> one 00:20:48.210 --> 00:20:48.220 align:start position:0% did this to two shard system and one 00:20:48.220 --> 00:20:49.650 align:start position:0% did this to two shard system and one thing<00:20:48.400> that<00:20:48.549> we<00:20:48.640> kind<00:20:48.790> of<00:20:48.880> have<00:20:49.030> been<00:20:49.120> wanting 00:20:49.650 --> 00:20:49.660 align:start position:0% thing that we kind of have been wanting 00:20:49.660 --> 00:20:52.950 align:start position:0% thing that we kind of have been wanting to<00:20:49.750> do<00:20:49.840> for<00:20:49.870> a<00:20:50.049> while<00:20:50.260> that<00:20:51.660> finally<00:20:52.660> kind<00:20:52.870> of 00:20:52.950 --> 00:20:52.960 align:start position:0% to do for a while that finally kind of 00:20:52.960 --> 00:20:56.220 align:start position:0% to do for a while that finally kind of got<00:20:53.140> to<00:20:53.260> implementing<00:20:53.590> is<00:20:54.960> you<00:20:55.960> know<00:20:56.080> I<00:20:56.110> mean 00:20:56.220 --> 00:20:56.230 align:start position:0% got to implementing is you know I mean 00:20:56.230 --> 00:20:59.430 align:start position:0% got to implementing is you know I mean just<00:20:57.100> like<00:20:57.250> a<00:20:57.280> few<00:20:57.910> months<00:20:58.169> like<00:20:59.169> there's<00:20:59.380> a 00:20:59.430 --> 00:20:59.440 align:start position:0% just like a few months like there's a 00:20:59.440 --> 00:21:03.690 align:start position:0% just like a few months like there's a really<00:20:59.770> short<00:21:00.100> order<00:21:00.340> is<00:21:01.950> shard<00:21:02.950> rotation<00:21:03.429> so 00:21:03.690 --> 00:21:03.700 align:start position:0% really short order is shard rotation so 00:21:03.700 --> 00:21:05.789 align:start position:0% really short order is shard rotation so like<00:21:03.910> here<00:21:04.240> what<00:21:04.360> we<00:21:04.480> see<00:21:04.510> is<00:21:04.809> two<00:21:05.169> shards<00:21:05.590> that 00:21:05.789 --> 00:21:05.799 align:start position:0% like here what we see is two shards that 00:21:05.799 --> 00:21:08.370 align:start position:0% like here what we see is two shards that are<00:21:05.890> changing<00:21:06.280> position<00:21:06.900> one<00:21:07.900> of<00:21:07.929> them<00:21:08.140> is<00:21:08.260> the 00:21:08.370 --> 00:21:08.380 align:start position:0% are changing position one of them is the 00:21:08.380 --> 00:21:10.169 align:start position:0% are changing position one of them is the route<00:21:08.530> at<00:21:08.740> first<00:21:08.980> and<00:21:09.280> then<00:21:09.400> it<00:21:09.580> changes<00:21:09.970> and 00:21:10.169 --> 00:21:10.179 align:start position:0% route at first and then it changes and 00:21:10.179 --> 00:21:12.330 align:start position:0% route at first and then it changes and then<00:21:10.630> the<00:21:10.720> other<00:21:10.870> one<00:21:11.049> is<00:21:11.169> the<00:21:11.290> route<00:21:11.470> and<00:21:11.710> then 00:21:12.330 --> 00:21:12.340 align:start position:0% then the other one is the route and then 00:21:12.340 --> 00:21:13.710 align:start position:0% then the other one is the route and then it<00:21:12.549> changes<00:21:12.910> again<00:21:13.000> and<00:21:13.270> the<00:21:13.330> other<00:21:13.450> one<00:21:13.600> is 00:21:13.710 --> 00:21:13.720 align:start position:0% it changes again and the other one is 00:21:13.720 --> 00:21:15.960 align:start position:0% it changes again and the other one is the<00:21:13.840> route<00:21:13.990> so<00:21:14.710> the<00:21:15.010> purple<00:21:15.340> blocks<00:21:15.549> there<00:21:15.790> are 00:21:15.960 --> 00:21:15.970 align:start position:0% the route so the purple blocks there are 00:21:15.970 --> 00:21:19.590 align:start position:0% the route so the purple blocks there are route<00:21:16.150> blocks<00:21:16.450> the<00:21:17.020> yellow<00:21:17.830> blocks<00:21:18.160> are<00:21:18.600> child 00:21:19.590 --> 00:21:19.600 align:start position:0% route blocks the yellow blocks are child 00:21:19.600 --> 00:21:22.799 align:start position:0% route blocks the yellow blocks are child locks<00:21:19.870> and<00:21:20.169> the<00:21:20.950> roles<00:21:21.400> of<00:21:21.850> these<00:21:21.970> shards<00:21:22.540> and 00:21:22.799 --> 00:21:22.809 align:start position:0% locks and the roles of these shards and 00:21:22.809 --> 00:21:24.270 align:start position:0% locks and the roles of these shards and the<00:21:22.870> hierarchical<00:21:23.290> census<00:21:23.679> are<00:21:23.799> changing<00:21:24.100> and 00:21:24.270 --> 00:21:24.280 align:start position:0% the hierarchical census are changing and 00:21:24.280 --> 00:21:26.340 align:start position:0% the hierarchical census are changing and this<00:21:24.910> does<00:21:25.210> not<00:21:25.240> require<00:21:25.720> that<00:21:25.929> we<00:21:26.049> reason 00:21:26.340 --> 00:21:26.350 align:start position:0% this does not require that we reason 00:21:26.350 --> 00:21:28.080 align:start position:0% this does not require that we reason about<00:21:26.410> consensus<00:21:27.040> safety<00:21:27.309> at<00:21:27.400> all<00:21:27.549> because 00:21:28.080 --> 00:21:28.090 align:start position:0% about consensus safety at all because 00:21:28.090 --> 00:21:31.049 align:start position:0% about consensus safety at all because the<00:21:28.799> the<00:21:29.799> correct<00:21:30.309> by<00:21:30.370> construction<00:21:30.640> process 00:21:31.049 --> 00:21:31.059 align:start position:0% the the correct by construction process 00:21:31.059 --> 00:21:33.210 align:start position:0% the the correct by construction process kind<00:21:31.630> of<00:21:31.690> guarantees<00:21:32.320> that<00:21:32.350> I<00:21:32.679> with<00:21:33.040> no 00:21:33.210 --> 00:21:33.220 align:start position:0% kind of guarantees that I with no 00:21:33.220 --> 00:21:35.549 align:start position:0% kind of guarantees that I with no thought<00:21:33.490> because<00:21:33.970> it's<00:21:34.900> kind<00:21:35.049> of<00:21:35.080> upstream 00:21:35.549 --> 00:21:35.559 align:start position:0% thought because it's kind of upstream 00:21:35.559 --> 00:21:37.789 align:start position:0% thought because it's kind of upstream from<00:21:35.919> our<00:21:35.980> definition<00:21:36.130> process<00:21:36.730> and<00:21:37.000> so 00:21:37.789 --> 00:21:37.799 align:start position:0% from our definition process and so 00:21:37.799 --> 00:21:39.690 align:start position:0% from our definition process and so relatively<00:21:38.799> little<00:21:39.070> work<00:21:39.100> compared<00:21:39.640> to 00:21:39.690 --> 00:21:39.700 align:start position:0% relatively little work compared to 00:21:39.700 --> 00:21:41.760 align:start position:0% relatively little work compared to normally<00:21:40.150> working<00:21:40.360> Contessa's<00:21:40.990> protocols<00:21:41.380> we 00:21:41.760 --> 00:21:41.770 align:start position:0% normally working Contessa's protocols we 00:21:41.770 --> 00:21:43.500 align:start position:0% normally working Contessa's protocols we define<00:21:42.100> this<00:21:42.280> like<00:21:42.460> actually<00:21:42.940> relatively 00:21:43.500 --> 00:21:43.510 align:start position:0% define this like actually relatively 00:21:43.510 --> 00:21:45.419 align:start position:0% define this like actually relatively complex<00:21:44.080> because<00:21:44.320> it's<00:21:44.440> protocol<00:21:44.770> there<00:21:45.280> like 00:21:45.419 --> 00:21:45.429 align:start position:0% complex because it's protocol there like 00:21:45.429 --> 00:21:48.090 align:start position:0% complex because it's protocol there like this<00:21:45.910> comes<00:21:46.210> to<00:21:46.450> consensus<00:21:46.870> on<00:21:47.020> you<00:21:47.590> know<00:21:47.679> the 00:21:48.090 --> 00:21:48.100 align:start position:0% this comes to consensus on you know the 00:21:48.100 --> 00:21:51.240 align:start position:0% this comes to consensus on you know the state<00:21:48.309> of<00:21:48.340> two<00:21:49.240> shards<00:21:49.960> with<00:21:50.320> locks<00:21:50.740> that<00:21:51.070> have 00:21:51.240 --> 00:21:51.250 align:start position:0% state of two shards with locks that have 00:21:51.250 --> 00:21:52.890 align:start position:0% state of two shards with locks that have like<00:21:51.520> two<00:21:51.730> different<00:21:52.030> positions<00:21:52.150> and<00:21:52.690> have 00:21:52.890 --> 00:21:52.900 align:start position:0% like two different positions and have 00:21:52.900 --> 00:21:54.510 align:start position:0% like two different positions and have like<00:21:53.080> a<00:21:53.110> relatively<00:21:53.860> complicated<00:21:54.190> fork 00:21:54.510 --> 00:21:54.520 align:start position:0% like a relatively complicated fork 00:21:54.520 --> 00:21:57.720 align:start position:0% like a relatively complicated fork choice<00:21:54.700> role<00:21:55.650> and<00:21:56.650> here's<00:21:56.919> like<00:21:57.070> an<00:21:57.250> the<00:21:57.490> kind 00:21:57.720 --> 00:21:57.730 align:start position:0% choice role and here's like an the kind 00:21:57.730 --> 00:22:00.120 align:start position:0% choice role and here's like an the kind of<00:21:57.790> next<00:21:58.750> kind<00:21:59.260> of<00:21:59.320> conclusion<00:21:59.710> of<00:21:59.799> that<00:21:59.950> is 00:22:00.120 --> 00:22:00.130 align:start position:0% of next kind of conclusion of that is 00:22:00.130 --> 00:22:02.220 align:start position:0% of next kind of conclusion of that is like<00:22:00.280> oh<00:22:00.370> look<00:22:00.580> when<00:22:00.790> we<00:22:00.850> have<00:22:00.970> two<00:22:01.230> shards 00:22:02.220 --> 00:22:02.230 align:start position:0% like oh look when we have two shards 00:22:02.230 --> 00:22:04.159 align:start position:0% like oh look when we have two shards that<00:22:02.440> can<00:22:02.590> send<00:22:02.919> messages<00:22:03.010> we<00:22:03.340> can<00:22:03.460> do<00:22:03.520> routing 00:22:04.159 --> 00:22:04.169 align:start position:0% that can send messages we can do routing 00:22:04.169 --> 00:22:07.020 align:start position:0% that can send messages we can do routing we<00:22:05.169> can<00:22:05.320> move<00:22:05.740> shards<00:22:06.100> around<00:22:06.370> in<00:22:06.700> two 00:22:07.020 --> 00:22:07.030 align:start position:0% we can move shards around in two 00:22:07.030 --> 00:22:08.070 align:start position:0% we can move shards around in two positions<00:22:07.210> we<00:22:07.540> can<00:22:07.659> move<00:22:07.750> short 00:22:08.070 --> 00:22:08.080 align:start position:0% positions we can move short 00:22:08.080 --> 00:22:10.889 align:start position:0% positions we can move short rounded<00:22:08.440> more<00:22:08.649> and<00:22:09.070> then<00:22:09.970> we<00:22:10.029> have<00:22:10.179> this<00:22:10.299> you 00:22:10.889 --> 00:22:10.899 align:start position:0% rounded more and then we have this you 00:22:10.899 --> 00:22:13.289 align:start position:0% rounded more and then we have this you know<00:22:11.039> pretty<00:22:12.039> cool<00:22:12.340> sharding<00:22:12.730> solution<00:22:13.120> where 00:22:13.289 --> 00:22:13.299 align:start position:0% know pretty cool sharding solution where 00:22:13.299 --> 00:22:15.680 align:start position:0% know pretty cool sharding solution where we<00:22:13.419> have<00:22:13.539> messages<00:22:13.990> being<00:22:14.169> routed<00:22:14.350> around 00:22:15.680 --> 00:22:15.690 align:start position:0% we have messages being routed around 00:22:15.690 --> 00:22:18.240 align:start position:0% we have messages being routed around cross<00:22:16.690> yards<00:22:17.110> and<00:22:17.289> with<00:22:17.500> like<00:22:17.830> the<00:22:17.980> atomicity 00:22:18.240 --> 00:22:18.250 align:start position:0% cross yards and with like the atomicity 00:22:18.250 --> 00:22:21.750 align:start position:0% cross yards and with like the atomicity property<00:22:18.760> that<00:22:18.850> if<00:22:18.970> your<00:22:20.250> route<00:22:21.250> isn't<00:22:21.610> fully 00:22:21.750 --> 00:22:21.760 align:start position:0% property that if your route isn't fully 00:22:21.760 --> 00:22:23.880 align:start position:0% property that if your route isn't fully completed<00:22:22.269> then<00:22:22.450> the<00:22:22.480> block<00:22:22.990> that<00:22:23.200> started 00:22:23.880 --> 00:22:23.890 align:start position:0% completed then the block that started 00:22:23.890 --> 00:22:26.519 align:start position:0% completed then the block that started that<00:22:23.980> route<00:22:24.130> will<00:22:24.279> be<00:22:24.309> orphaned<00:22:25.260> so<00:22:26.260> we<00:22:26.409> have 00:22:26.519 --> 00:22:26.529 align:start position:0% that route will be orphaned so we have 00:22:26.529 --> 00:22:29.610 align:start position:0% that route will be orphaned so we have like<00:22:26.740> you<00:22:27.210> know<00:22:28.210> a<00:22:28.330> really<00:22:28.840> kind<00:22:29.200> of<00:22:29.320> strong 00:22:29.610 --> 00:22:29.620 align:start position:0% like you know a really kind of strong 00:22:29.620 --> 00:22:32.909 align:start position:0% like you know a really kind of strong ability<00:22:30.100> to<00:22:30.399> iterate<00:22:31.179> very<00:22:31.210> quickly<00:22:31.919> because 00:22:32.909 --> 00:22:32.919 align:start position:0% ability to iterate very quickly because 00:22:32.919 --> 00:22:34.500 align:start position:0% ability to iterate very quickly because of<00:22:33.039> the<00:22:33.130> correct<00:22:33.340> by<00:22:33.429> construction<00:22:33.850> approach 00:22:34.500 --> 00:22:34.510 align:start position:0% of the correct by construction approach 00:22:34.510 --> 00:22:36.870 align:start position:0% of the correct by construction approach because<00:22:35.080> we<00:22:35.110> don't<00:22:35.409> need<00:22:35.649> to<00:22:35.710> look<00:22:36.100> back<00:22:36.309> at 00:22:36.870 --> 00:22:36.880 align:start position:0% because we don't need to look back at 00:22:36.880 --> 00:22:38.820 align:start position:0% because we don't need to look back at the<00:22:37.360> previous<00:22:37.600> guarantees<00:22:38.169> we're<00:22:38.590> not<00:22:38.710> at 00:22:38.820 --> 00:22:38.830 align:start position:0% the previous guarantees we're not at 00:22:38.830 --> 00:22:41.700 align:start position:0% the previous guarantees we're not at risk<00:22:38.980> of<00:22:39.220> disrupting<00:22:39.549> them<00:22:40.200> and<00:22:41.200> so<00:22:41.380> the<00:22:41.590> you 00:22:41.700 --> 00:22:41.710 align:start position:0% risk of disrupting them and so the you 00:22:41.710 --> 00:22:44.310 align:start position:0% risk of disrupting them and so the you know<00:22:41.830> I'm<00:22:42.450> never<00:22:43.450> walking<00:22:44.049> through<00:22:44.230> this 00:22:44.310 --> 00:22:44.320 align:start position:0% know I'm never walking through this 00:22:44.320 --> 00:22:46.950 align:start position:0% know I'm never walking through this again<00:22:44.649> so<00:22:45.010> this<00:22:45.399> so<00:22:45.700> so<00:22:46.120> what's<00:22:46.600> gonna<00:22:46.690> happen 00:22:46.950 --> 00:22:46.960 align:start position:0% again so this so so what's gonna happen 00:22:46.960 --> 00:22:49.139 align:start position:0% again so this so so what's gonna happen here<00:22:47.080> is<00:22:47.230> first<00:22:47.470> the<00:22:47.710> the<00:22:48.190> route<00:22:48.460> chart<00:22:48.789> was 00:22:49.139 --> 00:22:49.149 align:start position:0% here is first the the route chart was 00:22:49.149 --> 00:22:50.430 align:start position:0% here is first the the route chart was initially<00:22:49.419> 0<00:22:49.600> now<00:22:49.779> is<00:22:49.899> switching<00:22:50.169> to<00:22:50.260> one 00:22:50.430 --> 00:22:50.440 align:start position:0% initially 0 now is switching to one 00:22:50.440 --> 00:22:52.379 align:start position:0% initially 0 now is switching to one these<00:22:51.130> messages<00:22:51.490> are<00:22:51.610> being<00:22:51.639> routed<00:22:51.970> from 00:22:52.379 --> 00:22:52.389 align:start position:0% these messages are being routed from 00:22:52.389 --> 00:22:56.820 align:start position:0% these messages are being routed from chars<00:22:53.350> 6<00:22:53.740> to<00:22:53.889> 3<00:22:54.070> and<00:22:54.340> back<00:22:54.990> charged<00:22:55.990> shard<00:22:56.440> 0 00:22:56.820 --> 00:22:56.830 align:start position:0% chars 6 to 3 and back charged shard 0 00:22:56.830 --> 00:23:00.990 align:start position:0% chars 6 to 3 and back charged shard 0 and<00:22:57.010> one<00:22:57.220> switched<00:22:57.750> from<00:22:58.750> 0<00:22:59.139> 1<00:22:59.320> to<00:22:59.679> like<00:22:59.830> 1<00:23:00.700> 0 00:23:00.990 --> 00:23:01.000 align:start position:0% and one switched from 0 1 to like 1 0 00:23:01.000 --> 00:23:03.450 align:start position:0% and one switched from 0 1 to like 1 0 and<00:23:01.179> then<00:23:01.240> and<00:23:01.539> then<00:23:01.630> back<00:23:01.840> and<00:23:02.139> then<00:23:02.590> shard<00:23:02.980> 3 00:23:03.450 --> 00:23:03.460 align:start position:0% and then and then back and then shard 3 00:23:03.460 --> 00:23:05.700 align:start position:0% and then and then back and then shard 3 became<00:23:04.330> a<00:23:04.389> child<00:23:04.690> to<00:23:04.809> start<00:23:05.019> for<00:23:05.320> even<00:23:05.620> though 00:23:05.700 --> 00:23:05.710 align:start position:0% became a child to start for even though 00:23:05.710 --> 00:23:07.409 align:start position:0% became a child to start for even though it<00:23:05.769> was<00:23:05.860> previously<00:23:06.340> a<00:23:06.399> sibling<00:23:06.760> and<00:23:06.880> then 00:23:07.409 --> 00:23:07.419 align:start position:0% it was previously a sibling and then 00:23:07.419 --> 00:23:09.240 align:start position:0% it was previously a sibling and then messages<00:23:08.139> start<00:23:08.470> to<00:23:08.740> get<00:23:08.860> routed<00:23:09.010> through 00:23:09.240 --> 00:23:09.250 align:start position:0% messages start to get routed through 00:23:09.250 --> 00:23:13.500 align:start position:0% messages start to get routed through shard<00:23:09.549> for<00:23:10.919> after<00:23:11.919> that<00:23:12.100> swap<00:23:12.490> so<00:23:13.269> it's<00:23:13.389> really 00:23:13.500 --> 00:23:13.510 align:start position:0% shard for after that swap so it's really 00:23:13.510 --> 00:23:15.000 align:start position:0% shard for after that swap so it's really kind<00:23:13.659> of<00:23:13.750> quite<00:23:14.110> complicated<00:23:14.470> we<00:23:14.769> have<00:23:14.799> like 00:23:15.000 --> 00:23:15.010 align:start position:0% kind of quite complicated we have like 00:23:15.010 --> 00:23:16.649 align:start position:0% kind of quite complicated we have like routing<00:23:15.279> tables<00:23:15.789> and<00:23:15.940> they're<00:23:16.029> updating<00:23:16.510> and 00:23:16.649 --> 00:23:16.659 align:start position:0% routing tables and they're updating and 00:23:16.659 --> 00:23:18.029 align:start position:0% routing tables and they're updating and but<00:23:17.110> we<00:23:17.200> really<00:23:17.470> didn't<00:23:17.710> need<00:23:17.769> to<00:23:17.860> think<00:23:17.980> about 00:23:18.029 --> 00:23:18.039 align:start position:0% but we really didn't need to think about 00:23:18.039 --> 00:23:19.200 align:start position:0% but we really didn't need to think about consensus<00:23:18.429> protocol<00:23:18.730> is<00:23:18.820> almost<00:23:18.970> at<00:23:19.090> all 00:23:19.200 --> 00:23:19.210 align:start position:0% consensus protocol is almost at all 00:23:19.210 --> 00:23:23.310 align:start position:0% consensus protocol is almost at all whilst<00:23:19.809> us<00:23:20.019> find<00:23:20.260> this<00:23:20.350> thing<00:23:21.720> so<00:23:22.720> you<00:23:22.779> know<00:23:23.169> we 00:23:23.310 --> 00:23:23.320 align:start position:0% whilst us find this thing so you know we 00:23:23.320 --> 00:23:29.710 align:start position:0% whilst us find this thing so you know we have<00:23:23.850> thank<00:23:24.850> you 00:23:29.710 --> 00:23:29.720 align:start position:0% 00:23:29.720 --> 00:23:32.870 align:start position:0% so<00:23:30.720> we<00:23:30.810> have<00:23:31.020> like<00:23:31.310> methodology<00:23:32.310> that<00:23:32.340> lets<00:23:32.700> us 00:23:32.870 --> 00:23:32.880 align:start position:0% so we have like methodology that lets us 00:23:32.880 --> 00:23:34.610 align:start position:0% so we have like methodology that lets us define<00:23:33.270> consensus<00:23:33.780> protocols<00:23:34.170> we've<00:23:34.320> defined 00:23:34.610 --> 00:23:34.620 align:start position:0% define consensus protocols we've defined 00:23:34.620 --> 00:23:36.470 align:start position:0% define consensus protocols we've defined a<00:23:34.770> large<00:23:34.980> number<00:23:35.250> of<00:23:35.370> consensus<00:23:35.850> protocols<00:23:36.240> or 00:23:36.470 --> 00:23:36.480 align:start position:0% a large number of consensus protocols or 00:23:36.480 --> 00:23:38.360 align:start position:0% a large number of consensus protocols or partially<00:23:37.380> defined<00:23:37.650> a<00:23:37.860> large<00:23:38.100> number<00:23:38.280> of 00:23:38.360 --> 00:23:38.370 align:start position:0% partially defined a large number of 00:23:38.370 --> 00:23:41.600 align:start position:0% partially defined a large number of consensus<00:23:38.670> protocols<00:23:39.030> and<00:23:40.070> you<00:23:41.070> know<00:23:41.190> and<00:23:41.400> we 00:23:41.600 --> 00:23:41.610 align:start position:0% consensus protocols and you know and we 00:23:41.610 --> 00:23:42.920 align:start position:0% consensus protocols and you know and we iterate<00:23:41.820> while<00:23:42.090> creating<00:23:42.360> minimal<00:23:42.750> proof 00:23:42.920 --> 00:23:42.930 align:start position:0% iterate while creating minimal proof 00:23:42.930 --> 00:23:44.810 align:start position:0% iterate while creating minimal proof obligations<00:23:43.470> and<00:23:43.620> we<00:23:43.680> are<00:23:43.980> able<00:23:44.100> to<00:23:44.280> mix<00:23:44.700> and 00:23:44.810 --> 00:23:44.820 align:start position:0% obligations and we are able to mix and 00:23:44.820 --> 00:23:47.630 align:start position:0% obligations and we are able to mix and match<00:23:45.290> kind<00:23:46.290> of<00:23:46.350> a<00:23:46.410> lot<00:23:46.560> and<00:23:46.830> you<00:23:47.340> know<00:23:47.430> so<00:23:47.610> I 00:23:47.630 --> 00:23:47.640 align:start position:0% match kind of a lot and you know so I 00:23:47.640 --> 00:23:50.750 align:start position:0% match kind of a lot and you know so I recommend<00:23:48.150> that<00:23:48.240> you<00:23:48.300> try<00:23:48.600> out<00:23:49.670> you<00:23:50.670> know 00:23:50.750 --> 00:23:50.760 align:start position:0% recommend that you try out you know 00:23:50.760 --> 00:23:53.990 align:start position:0% recommend that you try out you know correct<00:23:51.030> by<00:23:51.120> construction<00:23:51.480> and<00:23:52.320> we<00:23:52.880> sorry<00:23:53.880> I'm 00:23:53.990 --> 00:23:54.000 align:start position:0% correct by construction and we sorry I'm 00:23:54.000 --> 00:23:55.670 align:start position:0% correct by construction and we sorry I'm looking<00:23:54.300> at<00:23:54.390> the<00:23:54.450> wrong<00:23:54.600> slide<00:23:54.870> here<00:23:55.140> got 00:23:55.670 --> 00:23:55.680 align:start position:0% looking at the wrong slide here got 00:23:55.680 --> 00:23:58.750 align:start position:0% looking at the wrong slide here got ahead<00:23:55.800> of<00:23:55.860> myself<00:23:56.420> that<00:23:57.420> was<00:23:57.510> the<00:23:57.630> next<00:23:57.750> slide 00:23:58.750 --> 00:23:58.760 align:start position:0% ahead of myself that was the next slide 00:23:58.760 --> 00:24:01.430 align:start position:0% ahead of myself that was the next slide so<00:23:59.760> we<00:24:00.270> basically<00:24:00.420> really<00:24:01.020> rely<00:24:01.230> on<00:24:01.290> these 00:24:01.430 --> 00:24:01.440 align:start position:0% so we basically really rely on these 00:24:01.440 --> 00:24:03.920 align:start position:0% so we basically really rely on these partial<00:24:01.800> specifications<00:24:02.430> and<00:24:02.700> you<00:24:03.630> know<00:24:03.750> the 00:24:03.920 --> 00:24:03.930 align:start position:0% partial specifications and you know the 00:24:03.930 --> 00:24:05.390 align:start position:0% partial specifications and you know the fact<00:24:04.170> that<00:24:04.260> it's<00:24:04.470> not<00:24:04.590> defined<00:24:05.010> yet<00:24:05.130> is 00:24:05.390 --> 00:24:05.400 align:start position:0% fact that it's not defined yet is 00:24:05.400 --> 00:24:07.580 align:start position:0% fact that it's not defined yet is actually<00:24:05.760> a<00:24:05.820> huge<00:24:06.030> asset<00:24:06.210> for<00:24:06.390> us<00:24:06.570> the<00:24:07.440> fact 00:24:07.580 --> 00:24:07.590 align:start position:0% actually a huge asset for us the fact 00:24:07.590 --> 00:24:10.100 align:start position:0% actually a huge asset for us the fact that<00:24:07.710> we<00:24:07.800> leave<00:24:08.130> things<00:24:08.400> undefined<00:24:09.000> until<00:24:09.450> you 00:24:10.100 --> 00:24:10.110 align:start position:0% that we leave things undefined until you 00:24:10.110 --> 00:24:12.980 align:start position:0% that we leave things undefined until you know<00:24:10.230> the<00:24:10.800> latest<00:24:11.040> possible<00:24:11.610> moment<00:24:11.990> means 00:24:12.980 --> 00:24:12.990 align:start position:0% know the latest possible moment means 00:24:12.990 --> 00:24:16.370 align:start position:0% know the latest possible moment means that<00:24:13.320> we<00:24:13.560> have<00:24:13.940> as<00:24:14.940> much<00:24:15.630> flexibility<00:24:16.320> as 00:24:16.370 --> 00:24:16.380 align:start position:0% that we have as much flexibility as 00:24:16.380 --> 00:24:18.230 align:start position:0% that we have as much flexibility as possible<00:24:16.500> to<00:24:17.070> iterate<00:24:17.580> without<00:24:17.850> disrupting 00:24:18.230 --> 00:24:18.240 align:start position:0% possible to iterate without disrupting 00:24:18.240 --> 00:24:22.190 align:start position:0% possible to iterate without disrupting our<00:24:18.420> previous<00:24:18.750> proofs<00:24:19.760> so<00:24:20.990> all<00:24:21.990> right<00:24:22.110> you 00:24:22.190 --> 00:24:22.200 align:start position:0% our previous proofs so all right you 00:24:22.200 --> 00:24:25.120 align:start position:0% our previous proofs so all right you said<00:24:22.380> all<00:24:22.500> this<00:24:22.680> yes<00:24:23.310> it's<00:24:24.030> it's<00:24:24.420> great<00:24:24.690> try<00:24:25.050> it 00:24:25.120 --> 00:24:25.130 align:start position:0% said all this yes it's it's great try it 00:24:25.130 --> 00:24:27.290 align:start position:0% said all this yes it's it's great try it correct<00:24:26.130> by<00:24:26.250> construction<00:24:26.580> protocol<00:24:27.000> design 00:24:27.290 --> 00:24:27.300 align:start position:0% correct by construction protocol design 00:24:27.300 --> 00:24:32.450 align:start position:0% correct by construction protocol design it's<00:24:28.050> awesome<00:24:29.270> so<00:24:30.270> now<00:24:31.140> let's<00:24:31.620> moving<00:24:32.250> to<00:24:32.370> the 00:24:32.450 --> 00:24:32.460 align:start position:0% it's awesome so now let's moving to the 00:24:32.460 --> 00:24:34.760 align:start position:0% it's awesome so now let's moving to the like<00:24:32.780> kind<00:24:33.780> of<00:24:33.840> announcement<00:24:34.350> section<00:24:34.500> of<00:24:34.710> the 00:24:34.760 --> 00:24:34.770 align:start position:0% like kind of announcement section of the 00:24:34.770 --> 00:24:37.130 align:start position:0% like kind of announcement section of the talk<00:24:35.150> so<00:24:36.150> that<00:24:36.180> was<00:24:36.420> that<00:24:36.600> was<00:24:36.720> like<00:24:36.840> oh<00:24:36.930> that 00:24:37.130 --> 00:24:37.140 align:start position:0% talk so that was that was like oh that 00:24:37.140 --> 00:24:38.870 align:start position:0% talk so that was that was like oh that was<00:24:37.230> pretty<00:24:37.320> much<00:24:37.500> all<00:24:37.650> of<00:24:37.680> the<00:24:37.950> all<00:24:38.160> of<00:24:38.700> the 00:24:38.870 --> 00:24:38.880 align:start position:0% was pretty much all of the all of the 00:24:38.880 --> 00:24:42.710 align:start position:0% was pretty much all of the all of the content<00:24:39.390> so<00:24:39.630> we<00:24:40.380> have<00:24:40.970> some<00:24:41.970> a<00:24:42.210> bunch<00:24:42.570> of<00:24:42.660> a 00:24:42.710 --> 00:24:42.720 align:start position:0% content so we have some a bunch of a 00:24:42.720 --> 00:24:43.910 align:start position:0% content so we have some a bunch of a bunch<00:24:42.840> of<00:24:43.050> announcements<00:24:43.500> of<00:24:43.530> people<00:24:43.770> like 00:24:43.910 --> 00:24:43.920 align:start position:0% bunch of announcements of people like 00:24:43.920 --> 00:24:46.100 align:start position:0% bunch of announcements of people like you<00:24:44.010> know<00:24:44.100> contributing<00:24:44.580> to<00:24:44.820> a<00:24:45.270> CBC<00:24:45.840> Kasper 00:24:46.100 --> 00:24:46.110 align:start position:0% you know contributing to a CBC Kasper 00:24:46.110 --> 00:24:49.310 align:start position:0% you know contributing to a CBC Kasper research<00:24:46.380> this<00:24:46.710> is<00:24:46.920> a<00:24:47.420> brog<00:24:48.420> ham<00:24:48.960> rock<00:24:49.140> from 00:24:49.310 --> 00:24:49.320 align:start position:0% research this is a brog ham rock from 00:24:49.320 --> 00:24:51.200 align:start position:0% research this is a brog ham rock from true<00:24:49.620> level<00:24:49.770> built<00:24:50.070> a<00:24:50.250> generative<00:24:50.760> testing 00:24:51.200 --> 00:24:51.210 align:start position:0% true level built a generative testing 00:24:51.210 --> 00:24:54.920 align:start position:0% true level built a generative testing for<00:24:51.540> CBC<00:24:52.050> caster<00:24:52.290> protocols<00:24:53.270> I'm<00:24:54.270> gonna<00:24:54.390> let 00:24:54.920 --> 00:24:54.930 align:start position:0% for CBC caster protocols I'm gonna let 00:24:54.930 --> 00:24:59.180 align:start position:0% for CBC caster protocols I'm gonna let see<00:24:55.050> if<00:24:55.110> I<00:24:55.140> can<00:24:55.610> and<00:24:56.610> then<00:24:57.300> with<00:24:57.720> this<00:24:58.190> spoiler 00:24:59.180 --> 00:24:59.190 align:start position:0% see if I can and then with this spoiler 00:24:59.190 --> 00:25:02.180 align:start position:0% see if I can and then with this spoiler alert<00:25:00.050> so<00:25:01.050> with<00:25:01.170> this<00:25:01.290> what<00:25:01.680> this<00:25:01.800> kind<00:25:02.070> of 00:25:02.180 --> 00:25:02.190 align:start position:0% alert so with this what this kind of 00:25:02.190 --> 00:25:07.700 align:start position:0% alert so with this what this kind of shows<00:25:02.910> here<00:25:03.240> is<00:25:03.360> a<00:25:03.390> the<00:25:04.140> the<00:25:04.470> red<00:25:04.680> the<00:25:05.640> red<00:25:06.710> dots 00:25:07.700 --> 00:25:07.710 align:start position:0% shows here is a the the red the red dots 00:25:07.710 --> 00:25:10.220 align:start position:0% shows here is a the the red the red dots are<00:25:07.890> members<00:25:08.700> of<00:25:08.730> a<00:25:08.880> clique<00:25:09.150> which<00:25:10.050> are 00:25:10.220 --> 00:25:10.230 align:start position:0% are members of a clique which are 00:25:10.230 --> 00:25:11.960 align:start position:0% are members of a clique which are validators<00:25:10.800> who<00:25:10.890> see<00:25:11.130> each<00:25:11.220> other<00:25:11.490> agree<00:25:11.790> in<00:25:11.910> a 00:25:11.960 --> 00:25:11.970 align:start position:0% validators who see each other agree in a 00:25:11.970 --> 00:25:15.170 align:start position:0% validators who see each other agree in a way<00:25:12.090> that<00:25:12.240> they<00:25:12.360> are<00:25:13.280> actually<00:25:14.280> finalizing 00:25:15.170 --> 00:25:15.180 align:start position:0% way that they are actually finalizing 00:25:15.180 --> 00:25:18.050 align:start position:0% way that they are actually finalizing that<00:25:15.210> block<00:25:15.660> the<00:25:16.080> blue<00:25:16.290> one<00:25:16.470> down<00:25:16.620> there<00:25:17.060> and 00:25:18.050 --> 00:25:18.060 align:start position:0% that block the blue one down there and 00:25:18.060 --> 00:25:19.490 align:start position:0% that block the blue one down there and this<00:25:18.270> is<00:25:18.330> something<00:25:18.450> you<00:25:19.020> know<00:25:19.110> related<00:25:19.440> to 00:25:19.490 --> 00:25:19.500 align:start position:0% this is something you know related to 00:25:19.500 --> 00:25:21.920 align:start position:0% this is something you know related to the<00:25:19.590> way<00:25:19.680> that<00:25:19.860> finality<00:25:20.130> works<00:25:20.430> in<00:25:20.580> in<00:25:20.930> in 00:25:21.920 --> 00:25:21.930 align:start position:0% the way that finality works in in in 00:25:21.930 --> 00:25:25.790 align:start position:0% the way that finality works in in in Casper<00:25:22.670> and<00:25:24.020> and<00:25:25.020> and<00:25:25.200> here<00:25:25.380> we<00:25:25.500> see<00:25:25.650> like 00:25:25.790 --> 00:25:25.800 align:start position:0% Casper and and and here we see like 00:25:25.800 --> 00:25:29.390 align:start position:0% Casper and and and here we see like multiple<00:25:26.340> views<00:25:26.760> of<00:25:26.790> the<00:25:27.630> protocol<00:25:28.080> from<00:25:29.070> the 00:25:29.390 --> 00:25:29.400 align:start position:0% multiple views of the protocol from the 00:25:29.400 --> 00:25:30.620 align:start position:0% multiple views of the protocol from the point<00:25:29.550> view<00:25:29.610> for<00:25:29.880> different<00:25:30.120> validators 00:25:30.620 --> 00:25:30.630 align:start position:0% point view for different validators 00:25:30.630 --> 00:25:33.470 align:start position:0% point view for different validators until<00:25:31.290> one<00:25:31.530> of<00:25:31.560> them<00:25:31.770> finds<00:25:32.130> a<00:25:32.670> decision<00:25:33.300> on 00:25:33.470 --> 00:25:33.480 align:start position:0% until one of them finds a decision on 00:25:33.480 --> 00:25:36.170 align:start position:0% until one of them finds a decision on this<00:25:33.990> block<00:25:34.230> namely<00:25:35.070> finalizing<00:25:35.760> you<00:25:36.090> know 00:25:36.170 --> 00:25:36.180 align:start position:0% this block namely finalizing you know 00:25:36.180 --> 00:25:39.230 align:start position:0% this block namely finalizing you know this<00:25:36.330> this<00:25:36.990> blue<00:25:37.200> block<00:25:37.350> and<00:25:37.740> the<00:25:38.430> the<00:25:38.940> green 00:25:39.230 --> 00:25:39.240 align:start position:0% this this blue block and the the green 00:25:39.240 --> 00:25:41.570 align:start position:0% this this blue block and the the green dots<00:25:39.630> are<00:25:39.840> the<00:25:40.080> messages<00:25:40.920> from<00:25:41.040> the<00:25:41.160> validator 00:25:41.570 --> 00:25:41.580 align:start position:0% dots are the messages from the validator 00:25:41.580 --> 00:25:42.259 align:start position:0% dots are the messages from the validator whose<00:25:41.730> view 00:25:42.259 --> 00:25:42.269 align:start position:0% whose view 00:25:42.269 --> 00:25:45.799 align:start position:0% whose view and<00:25:42.539> the<00:25:42.959> red<00:25:43.169> dots<00:25:43.409> are<00:25:43.559> the<00:25:44.119> click<00:25:45.119> which<00:25:45.719> I 00:25:45.799 --> 00:25:45.809 align:start position:0% and the red dots are the click which I 00:25:45.809 --> 00:25:48.680 align:start position:0% and the red dots are the click which I was<00:25:45.929> like<00:25:46.049> a<00:25:46.399> group<00:25:47.399> of<00:25:47.549> validators<00:25:48.209> who<00:25:48.389> sees 00:25:48.680 --> 00:25:48.690 align:start position:0% was like a group of validators who sees 00:25:48.690 --> 00:25:50.209 align:start position:0% was like a group of validators who sees each<00:25:48.839> other<00:25:48.989> agree<00:25:49.440> in<00:25:49.619> a<00:25:49.679> certain<00:25:49.979> way<00:25:50.190> that 00:25:50.209 --> 00:25:50.219 align:start position:0% each other agree in a certain way that 00:25:50.219 --> 00:25:51.499 align:start position:0% each other agree in a certain way that corresponds<00:25:50.969> to<00:25:51.029> a<00:25:51.089> because<00:25:51.299> that's<00:25:51.450> a 00:25:51.499 --> 00:25:51.509 align:start position:0% corresponds to a because that's a 00:25:51.509 --> 00:25:54.589 align:start position:0% corresponds to a because that's a signature<00:25:51.809> that<00:25:52.440> you<00:25:53.309> know<00:25:53.399> is<00:25:54.330> like<00:25:54.539> a 00:25:54.589 --> 00:25:54.599 align:start position:0% signature that you know is like a 00:25:54.599 --> 00:25:57.709 align:start position:0% signature that you know is like a decision<00:25:55.080> so<00:25:56.070> so<00:25:56.940> that's<00:25:57.089> pretty<00:25:57.299> cool<00:25:57.450> stuff 00:25:57.709 --> 00:25:57.719 align:start position:0% decision so so that's pretty cool stuff 00:25:57.719 --> 00:25:59.359 align:start position:0% decision so so that's pretty cool stuff you<00:25:57.959> know<00:25:58.049> that<00:25:58.559> I<00:25:58.589> mentioned<00:25:59.039> the<00:25:59.099> charting 00:25:59.359 --> 00:25:59.369 align:start position:0% you know that I mentioned the charting 00:25:59.369 --> 00:26:00.440 align:start position:0% you know that I mentioned the charting proof<00:25:59.519> of<00:25:59.580> concept<00:25:59.879> we've<00:25:59.999> been<00:26:00.089> working<00:26:00.359> on 00:26:00.440 --> 00:26:00.450 align:start position:0% proof of concept we've been working on 00:26:00.450 --> 00:26:03.219 align:start position:0% proof of concept we've been working on this<00:26:00.599> but<00:26:00.839> like<00:26:00.929> I<00:26:01.019> look<00:26:01.379> significant<00:26:02.219> like 00:26:03.219 --> 00:26:03.229 align:start position:0% this but like I look significant like 00:26:03.229 --> 00:26:05.619 align:start position:0% this but like I look significant like rotating<00:26:04.229> group<00:26:04.469> of<00:26:04.709> people<00:26:05.039> since<00:26:05.279> the 00:26:05.619 --> 00:26:05.629 align:start position:0% rotating group of people since the 00:26:05.629 --> 00:26:07.579 align:start position:0% rotating group of people since the Berlin<00:26:06.629> hackathon<00:26:07.080> and<00:26:07.200> actually<00:26:07.409> before 00:26:07.579 --> 00:26:07.589 align:start position:0% Berlin hackathon and actually before 00:26:07.589 --> 00:26:09.440 align:start position:0% Berlin hackathon and actually before that<00:26:07.799> at<00:26:08.099> the<00:26:08.190> etherium<00:26:08.639> ic3<00:26:09.029> workshop<00:26:09.330> we 00:26:09.440 --> 00:26:09.450 align:start position:0% that at the etherium ic3 workshop we 00:26:09.450 --> 00:26:11.989 align:start position:0% that at the etherium ic3 workshop we worked<00:26:09.629> on<00:26:09.719> the<00:26:09.839> specification<00:26:10.999> especially 00:26:11.989 --> 00:26:11.999 align:start position:0% worked on the specification especially 00:26:11.999 --> 00:26:13.549 align:start position:0% worked on the specification especially want<00:26:12.119> to<00:26:12.179> give<00:26:12.269> a<00:26:12.299> shout<00:26:12.509> out<00:26:12.539> to<00:26:12.690> Alex<00:26:13.229> Keaton 00:26:13.549 --> 00:26:13.559 align:start position:0% want to give a shout out to Alex Keaton 00:26:13.559 --> 00:26:16.579 align:start position:0% want to give a shout out to Alex Keaton off<00:26:13.769> who<00:26:13.979> in<00:26:14.249> the<00:26:14.639> last<00:26:14.849> like<00:26:15.209> you<00:26:16.049> know<00:26:16.169> week 00:26:16.579 --> 00:26:16.589 align:start position:0% off who in the last like you know week 00:26:16.589 --> 00:26:18.440 align:start position:0% off who in the last like you know week and<00:26:16.859> also<00:26:17.129> during<00:26:17.309> the<00:26:17.519> East<00:26:17.669> San<00:26:18.059> Francisco 00:26:18.440 --> 00:26:18.450 align:start position:0% and also during the East San Francisco 00:26:18.450 --> 00:26:20.810 align:start position:0% and also during the East San Francisco hackathon<00:26:19.139> put<00:26:19.320> in<00:26:19.469> like<00:26:19.619> heroic<00:26:20.309> efforts<00:26:20.669> to 00:26:20.810 --> 00:26:20.820 align:start position:0% hackathon put in like heroic efforts to 00:26:20.820 --> 00:26:23.619 align:start position:0% hackathon put in like heroic efforts to get<00:26:21.089> the<00:26:22.079> grouting<00:26:22.349> working<00:26:22.829> and<00:26:22.979> the<00:26:23.129> shard 00:26:23.619 --> 00:26:23.629 align:start position:0% get the grouting working and the shard 00:26:23.629 --> 00:26:26.029 align:start position:0% get the grouting working and the shard swapping<00:26:24.629> I<00:26:24.809> mean<00:26:25.229> he's<00:26:25.379> the<00:26:25.409> first<00:26:25.739> guy<00:26:25.889> he's 00:26:26.029 --> 00:26:26.039 align:start position:0% swapping I mean he's the first guy he's 00:26:26.039 --> 00:26:28.339 align:start position:0% swapping I mean he's the first guy he's the<00:26:26.190> first<00:26:26.339> person<00:26:26.429> to<00:26:26.609> prototype<00:26:27.269> the<00:26:27.450> cross 00:26:28.339 --> 00:26:28.349 align:start position:0% the first person to prototype the cross 00:26:28.349 --> 00:26:32.719 align:start position:0% the first person to prototype the cross shard<00:26:28.619> message<00:26:28.979> routing<00:26:29.309> bit<00:26:30.059> jealous<00:26:31.729> but 00:26:32.719 --> 00:26:32.729 align:start position:0% shard message routing bit jealous but 00:26:32.729 --> 00:26:34.579 align:start position:0% shard message routing bit jealous but you<00:26:33.239> know<00:26:33.329> you<00:26:34.019> should<00:26:34.169> check<00:26:34.349> out<00:26:34.440> this 00:26:34.579 --> 00:26:34.589 align:start position:0% you know you should check out this 00:26:34.589 --> 00:26:37.669 align:start position:0% you know you should check out this github<00:26:34.859> repo<00:26:35.279> and<00:26:35.629> see<00:26:36.629> if<00:26:36.779> you<00:26:37.019> like<00:26:37.320> it<00:26:37.529> and 00:26:37.669 --> 00:26:37.679 align:start position:0% github repo and see if you like it and 00:26:37.679 --> 00:26:40.789 align:start position:0% github repo and see if you like it and it's<00:26:38.099> not<00:26:38.249> there's<00:26:38.609> still<00:26:38.759> loads<00:26:38.969> of<00:26:39.179> bugs<00:26:39.799> but 00:26:40.789 --> 00:26:40.799 align:start position:0% it's not there's still loads of bugs but 00:26:40.799 --> 00:26:42.440 align:start position:0% it's not there's still loads of bugs but there's<00:26:41.339> you<00:26:41.579> know<00:26:41.609> it's<00:26:42.029> definitely 00:26:42.440 --> 00:26:42.450 align:start position:0% there's you know it's definitely 00:26:42.450 --> 00:26:44.060 align:start position:0% there's you know it's definitely interesting 00:26:44.060 --> 00:26:44.070 align:start position:0% interesting 00:26:44.070 --> 00:26:47.029 align:start position:0% interesting Aditya<00:26:45.059> who<00:26:45.509> is<00:26:45.899> probably<00:26:46.769> somewhere<00:26:46.979> here 00:26:47.029 --> 00:26:47.039 align:start position:0% Aditya who is probably somewhere here 00:26:47.039 --> 00:26:49.249 align:start position:0% Aditya who is probably somewhere here has<00:26:47.489> announced<00:26:47.820> that<00:26:48.059> he's<00:26:48.269> implementing<00:26:49.200> a 00:26:49.249 --> 00:26:49.259 align:start position:0% has announced that he's implementing a 00:26:49.259 --> 00:26:51.379 align:start position:0% has announced that he's implementing a shortened<00:26:49.559> client<00:26:49.969> with<00:26:50.969> like<00:26:51.179> you<00:26:51.269> know 00:26:51.379 --> 00:26:51.389 align:start position:0% shortened client with like you know 00:26:51.389 --> 00:26:53.869 align:start position:0% shortened client with like you know they're<00:26:51.719> in<00:26:51.839> blocks<00:26:52.169> and<00:26:52.469> like<00:26:53.309> you<00:26:53.759> know<00:26:53.849> very 00:26:53.869 --> 00:26:53.879 align:start position:0% they're in blocks and like you know very 00:26:53.879 --> 00:26:56.449 align:start position:0% they're in blocks and like you know very like<00:26:54.269> aetherium<00:26:54.629> starting<00:26:55.379> client<00:26:55.679> and<00:26:56.339> he 00:26:56.449 --> 00:26:56.459 align:start position:0% like aetherium starting client and he 00:26:56.459 --> 00:26:58.099 align:start position:0% like aetherium starting client and he has<00:26:56.609> a<00:26:56.639> github<00:26:57.089> repo<00:26:57.479> and<00:26:57.719> that<00:26:57.869> Twitter 00:26:58.099 --> 00:26:58.109 align:start position:0% has a github repo and that Twitter 00:26:58.109 --> 00:27:02.319 align:start position:0% has a github repo and that Twitter handle<00:26:59.099> he<00:26:59.219> should<00:26:59.369> follow<00:26:59.519> him<00:26:59.789> for<00:27:00.299> his<00:27:00.509> work 00:27:02.319 --> 00:27:02.329 align:start position:0% handle he should follow him for his work 00:27:02.329 --> 00:27:05.359 align:start position:0% handle he should follow him for his work we<00:27:03.329> this<00:27:03.719> is<00:27:03.899> a<00:27:03.929> exciting<00:27:04.529> one<00:27:04.859> we<00:27:05.039> kind<00:27:05.219> of 00:27:05.359 --> 00:27:05.369 align:start position:0% we this is a exciting one we kind of 00:27:05.369 --> 00:27:07.969 align:start position:0% we this is a exciting one we kind of released<00:27:06.029> a<00:27:06.299> draft<00:27:06.509> or<00:27:06.809> are<00:27:07.139> going<00:27:07.619> to<00:27:07.739> release 00:27:07.969 --> 00:27:07.979 align:start position:0% released a draft or are going to release 00:27:07.979 --> 00:27:09.259 align:start position:0% released a draft or are going to release a<00:27:08.009> draft<00:27:08.339> I<00:27:08.459> wrote<00:27:08.639> these<00:27:08.789> slides<00:27:09.029> I<00:27:09.149> thought 00:27:09.259 --> 00:27:09.269 align:start position:0% a draft I wrote these slides I thought 00:27:09.269 --> 00:27:11.089 align:start position:0% a draft I wrote these slides I thought we'd<00:27:09.419> have<00:27:09.450> it<00:27:09.719> released<00:27:09.839> by<00:27:10.229> now<00:27:10.409> but<00:27:10.649> we're 00:27:11.089 --> 00:27:11.099 align:start position:0% we'd have it released by now but we're 00:27:11.099 --> 00:27:13.729 align:start position:0% we'd have it released by now but we're gonna<00:27:11.219> release<00:27:11.429> a<00:27:11.579> draft<00:27:11.879> today<00:27:12.059> of<00:27:12.469> oh<00:27:13.469> wait 00:27:13.729 --> 00:27:13.739 align:start position:0% gonna release a draft today of oh wait 00:27:13.739 --> 00:27:16.669 align:start position:0% gonna release a draft today of oh wait it<00:27:13.859> is<00:27:13.979> released<00:27:14.309> my<00:27:14.669> bad<00:27:14.909> github<00:27:15.629> calm<00:27:16.200> slash 00:27:16.669 --> 00:27:16.679 align:start position:0% it is released my bad github calm slash 00:27:16.679 --> 00:27:20.839 align:start position:0% it is released my bad github calm slash CBC<00:27:17.249> Kasper<00:27:18.349> and<00:27:19.349> you<00:27:20.039> can<00:27:20.190> download<00:27:20.309> a<00:27:20.579> new 00:27:20.839 --> 00:27:20.849 align:start position:0% CBC Kasper and you can download a new 00:27:20.849 --> 00:27:23.299 align:start position:0% CBC Kasper and you can download a new specification<00:27:21.509> of<00:27:22.109> the<00:27:22.379> minimal<00:27:22.709> CBC<00:27:23.009> Kasper 00:27:23.299 --> 00:27:23.309 align:start position:0% specification of the minimal CBC Kasper 00:27:23.309 --> 00:27:26.839 align:start position:0% specification of the minimal CBC Kasper of<00:27:23.399> protocol<00:27:23.759> states<00:27:24.749> that<00:27:25.049> is<00:27:25.729> you<00:27:26.729> know 00:27:26.839 --> 00:27:26.849 align:start position:0% of protocol states that is you know 00:27:26.849 --> 00:27:30.190 align:start position:0% of protocol states that is you know extremely<00:27:27.629> rigorous<00:27:28.019> and<00:27:28.379> pedantic<00:27:28.879> with 00:27:30.190 --> 00:27:30.200 align:start position:0% extremely rigorous and pedantic with 00:27:30.200 --> 00:27:32.479 align:start position:0% extremely rigorous and pedantic with extremely<00:27:31.200> rigorous<00:27:31.440> and<00:27:31.829> pedantic<00:27:31.979> proof<00:27:32.339> of 00:27:32.479 --> 00:27:32.489 align:start position:0% extremely rigorous and pedantic proof of 00:27:32.489 --> 00:27:34.999 align:start position:0% extremely rigorous and pedantic proof of the<00:27:32.609> consensus<00:27:32.999> safety<00:27:33.269> result<00:27:33.629> and<00:27:34.009> example 00:27:34.999 --> 00:27:35.009 align:start position:0% the consensus safety result and example 00:27:35.009 --> 00:27:37.789 align:start position:0% the consensus safety result and example protocols<00:27:35.459> including<00:27:36.059> the<00:27:37.019> Friendly<00:27:37.320> Ghost<00:27:37.349> a 00:27:37.789 --> 00:27:37.799 align:start position:0% protocols including the Friendly Ghost a 00:27:37.799 --> 00:27:41.419 align:start position:0% protocols including the Friendly Ghost a finality<00:27:38.099> gadget<00:27:38.759> a<00:27:39.859> sharding<00:27:40.859> with<00:27:41.009> fixed 00:27:41.419 --> 00:27:41.429 align:start position:0% finality gadget a sharding with fixed 00:27:41.429 --> 00:27:44.539 align:start position:0% finality gadget a sharding with fixed hierarchy<00:27:42.679> and<00:27:43.679> I'd<00:27:43.829> like<00:27:44.009> to<00:27:44.099> thank<00:27:44.190> the<00:27:44.339> code 00:27:44.539 --> 00:27:44.549 align:start position:0% hierarchy and I'd like to thank the code 00:27:44.549 --> 00:27:48.249 align:start position:0% hierarchy and I'd like to thank the code my<00:27:44.820> co-author<00:27:45.149> is<00:27:45.359> Nate<00:27:46.139> rush<00:27:46.379> Aditya<00:27:47.249> and 00:27:48.249 --> 00:27:48.259 align:start position:0% my co-author is Nate rush Aditya and 00:27:48.259 --> 00:27:52.849 align:start position:0% my co-author is Nate rush Aditya and Georgio's<00:27:49.399> and<00:27:50.399> they're<00:27:50.519> all<00:27:50.639> here<00:27:51.619> you<00:27:52.619> you 00:27:52.849 --> 00:27:52.859 align:start position:0% Georgio's and they're all here you you 00:27:52.859 --> 00:27:54.440 align:start position:0% Georgio's and they're all here you you should<00:27:53.039> you<00:27:53.460> can<00:27:53.609> probably<00:27:53.849> recognize<00:27:54.059> them 00:27:54.440 --> 00:27:54.450 align:start position:0% should you can probably recognize them 00:27:54.450 --> 00:27:55.769 align:start position:0% should you can probably recognize them from<00:27:54.539> their<00:27:54.749> faces 00:27:55.769 --> 00:27:55.779 align:start position:0% from their faces 00:27:55.779 --> 00:27:58.049 align:start position:0% from their faces I<00:27:55.869> put<00:27:56.679> a<00:27:56.710> GES<00:27:57.219> face<00:27:57.399> was<00:27:57.609> on<00:27:57.669> the<00:27:57.759> previous 00:27:58.049 --> 00:27:58.059 align:start position:0% I put a GES face was on the previous 00:27:58.059 --> 00:28:01.139 align:start position:0% I put a GES face was on the previous slide<00:27:59.340> finally<00:28:00.340> you<00:28:00.580> know<00:28:00.669> don't<00:28:00.909> forget 00:28:01.139 --> 00:28:01.149 align:start position:0% slide finally you know don't forget 00:28:01.149 --> 00:28:03.930 align:start position:0% slide finally you know don't forget about<00:28:01.179> the<00:28:01.779> prototype<00:28:02.590> in<00:28:02.769> the<00:28:02.859> wiki<00:28:03.129> at<00:28:03.309> dairy 00:28:03.930 --> 00:28:03.940 align:start position:0% about the prototype in the wiki at dairy 00:28:03.940 --> 00:28:07.619 align:start position:0% about the prototype in the wiki at dairy m<00:28:04.090> /<00:28:04.299> TVC<00:28:04.690> -<00:28:04.809> Casper<00:28:05.729> these<00:28:06.729> are<00:28:06.849> like<00:28:07.059> good 00:28:07.619 --> 00:28:07.629 align:start position:0% m / TVC - Casper these are like good 00:28:07.629 --> 00:28:09.989 align:start position:0% m / TVC - Casper these are like good resources<00:28:08.289> if<00:28:08.440> you<00:28:08.529> want<00:28:08.710> to<00:28:08.950> like<00:28:09.249> dip<00:28:09.849> your 00:28:09.989 --> 00:28:09.999 align:start position:0% resources if you want to like dip your 00:28:09.999 --> 00:28:12.450 align:start position:0% resources if you want to like dip your toes<00:28:10.179> and<00:28:10.419> check<00:28:10.869> it<00:28:11.019> out 00:28:12.450 --> 00:28:12.460 align:start position:0% toes and check it out 00:28:12.460 --> 00:28:14.009 align:start position:0% toes and check it out you<00:28:12.700> know<00:28:12.789> we're<00:28:12.940> totally<00:28:13.179> looking<00:28:13.659> for<00:28:13.869> help 00:28:14.009 --> 00:28:14.019 align:start position:0% you know we're totally looking for help 00:28:14.019 --> 00:28:16.080 align:start position:0% you know we're totally looking for help of<00:28:14.259> all<00:28:14.499> kinds<00:28:15.009> and<00:28:15.190> we're<00:28:15.759> getting<00:28:15.820> better 00:28:16.080 --> 00:28:16.090 align:start position:0% of all kinds and we're getting better 00:28:16.090 --> 00:28:18.359 align:start position:0% of all kinds and we're getting better and<00:28:16.210> better<00:28:16.359> at<00:28:16.659> helping<00:28:17.379> you<00:28:17.769> help<00:28:17.979> us<00:28:18.129> as 00:28:18.359 --> 00:28:18.369 align:start position:0% and better at helping you help us as 00:28:18.369 --> 00:28:20.459 align:start position:0% and better at helping you help us as they're<00:28:19.149> like<00:28:19.299> documentation<00:28:20.169> and 00:28:20.459 --> 00:28:20.469 align:start position:0% they're like documentation and 00:28:20.469 --> 00:28:22.349 align:start position:0% they're like documentation and definitions<00:28:21.039> and<00:28:21.279> stuff<00:28:21.519> have<00:28:21.700> laid 00:28:22.349 --> 00:28:22.359 align:start position:0% definitions and stuff have laid 00:28:22.359 --> 00:28:23.489 align:start position:0% definitions and stuff have laid themselves<00:28:22.809> out<00:28:22.929> in<00:28:22.960> a<00:28:23.109> way<00:28:23.229> where<00:28:23.379> you<00:28:23.469> can 00:28:23.489 --> 00:28:23.499 align:start position:0% themselves out in a way where you can 00:28:23.499 --> 00:28:25.830 align:start position:0% themselves out in a way where you can you<00:28:24.070> know<00:28:24.190> come<00:28:24.399> in<00:28:24.580> and<00:28:24.729> contribute<00:28:25.059> in<00:28:25.450> a<00:28:25.809> way 00:28:25.830 --> 00:28:25.840 align:start position:0% you know come in and contribute in a way 00:28:25.840 --> 00:28:27.029 align:start position:0% you know come in and contribute in a way where<00:28:26.320> it's<00:28:26.440> really<00:28:26.559> clear<00:28:26.830> how<00:28:26.950> it 00:28:27.029 --> 00:28:27.039 align:start position:0% where it's really clear how it 00:28:27.039 --> 00:28:28.409 align:start position:0% where it's really clear how it interfaces<00:28:27.249> with<00:28:27.489> everyone<00:28:27.789> else's<00:28:28.029> work<00:28:28.059> and 00:28:28.409 --> 00:28:28.419 align:start position:0% interfaces with everyone else's work and 00:28:28.419 --> 00:28:30.659 align:start position:0% interfaces with everyone else's work and where<00:28:29.259> you<00:28:29.589> know<00:28:29.679> you<00:28:29.799> won't<00:28:30.039> be<00:28:30.190> wasting<00:28:30.549> your 00:28:30.659 --> 00:28:30.669 align:start position:0% where you know you won't be wasting your 00:28:30.669 --> 00:28:33.389 align:start position:0% where you know you won't be wasting your time<00:28:30.820> and<00:28:30.879> you<00:28:31.210> will<00:28:31.330> be<00:28:31.389> helping<00:28:32.339> so<00:28:33.339> you 00:28:33.389 --> 00:28:33.399 align:start position:0% time and you will be helping so you 00:28:33.399 --> 00:28:37.229 align:start position:0% time and you will be helping so you don't<00:28:34.289> reach<00:28:35.289> out<00:28:35.499> and<00:28:35.999> thanks<00:28:36.999> so<00:28:37.029> much<00:28:37.149> for 00:28:37.229 --> 00:28:37.239 align:start position:0% don't reach out and thanks so much for 00:28:37.239 --> 00:28:44.910 align:start position:0% don't reach out and thanks so much for listening 00:28:44.910 --> 00:28:44.920 align:start position:0% 00:28:44.920 --> 00:28:57.120 align:start position:0% I<00:28:48.000> have<00:28:49.000> time<00:28:49.120> for<00:28:49.180> one<00:28:49.330> question<00:28:55.620> it's<00:28:56.620> okay 00:28:57.120 --> 00:28:57.130 align:start position:0% I have time for one question it's okay 00:28:57.130 --> 00:28:59.340 align:start position:0% I have time for one question it's okay you<00:28:58.090> don't<00:28:58.270> need<00:28:58.390> to<00:28:58.480> ask<00:28:58.570> a<00:28:58.690> question<00:28:59.080> I<00:28:59.170> can 00:28:59.340 --> 00:28:59.350 align:start position:0% you don't need to ask a question I can 00:28:59.350 --> 00:29:03.060 align:start position:0% you don't need to ask a question I can just<00:28:59.620> go<00:29:00.660> by<00:29:01.660> everyone<00:29:02.020> oh<00:29:02.200> wait<00:29:02.830> there's<00:29:02.980> a 00:29:03.060 --> 00:29:03.070 align:start position:0% just go by everyone oh wait there's a 00:29:03.070 --> 00:29:04.680 align:start position:0% just go by everyone oh wait there's a question<00:29:03.370> sorry<00:29:03.670> sorry<00:29:04.360> sorry 00:29:04.680 --> 00:29:04.690 align:start position:0% question sorry sorry sorry 00:29:04.690 --> 00:29:06.150 align:start position:0% question sorry sorry sorry do<00:29:04.990> you<00:29:05.050> have<00:29:05.170> a<00:29:05.200> microphone<00:29:05.500> so<00:29:05.800> what's<00:29:05.980> the 00:29:06.150 --> 00:29:06.160 align:start position:0% do you have a microphone so what's the 00:29:06.160 --> 00:29:08.310 align:start position:0% do you have a microphone so what's the deal<00:29:06.310> there<00:29:06.630> the<00:29:07.630> microphones<00:29:08.080> are<00:29:08.170> at<00:29:08.200> the 00:29:08.310 --> 00:29:08.320 align:start position:0% deal there the microphones are at the 00:29:08.320 --> 00:29:09.810 align:start position:0% deal there the microphones are at the front<00:29:08.560> you<00:29:08.740> have<00:29:08.860> to<00:29:08.950> come<00:29:09.100> come<00:29:09.550> over<00:29:09.670> to<00:29:09.730> the 00:29:09.810 --> 00:29:09.820 align:start position:0% front you have to come come over to the 00:29:09.820 --> 00:29:10.140 align:start position:0% front you have to come come over to the front 00:29:10.140 --> 00:29:10.150 align:start position:0% front 00:29:10.150 --> 00:29:12.000 align:start position:0% front we<00:29:10.630> got<00:29:10.780> like<00:29:10.990> 30<00:29:11.230> seconds<00:29:11.590> you<00:29:11.740> got<00:29:11.830> to<00:29:11.950> be 00:29:12.000 --> 00:29:12.010 align:start position:0% we got like 30 seconds you got to be 00:29:12.010 --> 00:29:14.040 align:start position:0% we got like 30 seconds you got to be quick<00:29:12.190> 10<00:29:12.820> second<00:29:13.180> question<00:29:13.510> 20<00:29:13.750> second 00:29:14.040 --> 00:29:14.050 align:start position:0% quick 10 second question 20 second 00:29:14.050 --> 00:29:23.610 align:start position:0% quick 10 second question 20 second answer<00:29:20.760> yeah<00:29:21.760> can<00:29:21.940> you<00:29:21.970> hear<00:29:22.060> me<00:29:22.180> good<00:29:22.630> what's 00:29:23.610 --> 00:29:23.620 align:start position:0% answer yeah can you hear me good what's 00:29:23.620 --> 00:29:25.800 align:start position:0% answer yeah can you hear me good what's a<00:29:23.710> good<00:29:23.860> way<00:29:23.950> of<00:29:23.980> really<00:29:24.700> understanding<00:29:24.820> CBC 00:29:25.800 --> 00:29:25.810 align:start position:0% a good way of really understanding CBC 00:29:25.810 --> 00:29:28.470 align:start position:0% a good way of really understanding CBC if<00:29:26.710> you<00:29:26.830> come<00:29:26.980> from<00:29:27.100> a<00:29:27.190> math<00:29:27.370> background<00:29:27.640> yes 00:29:28.470 --> 00:29:28.480 align:start position:0% if you come from a math background yes 00:29:28.480 --> 00:29:31.290 align:start position:0% if you come from a math background yes read<00:29:28.780> this<00:29:28.960> paper<00:29:29.370> and<00:29:30.370> anything<00:29:30.730> anything 00:29:31.290 --> 00:29:31.300 align:start position:0% read this paper and anything anything 00:29:31.300 --> 00:29:33.630 align:start position:0% read this paper and anything anything more<00:29:31.480> sort<00:29:31.720> of<00:29:31.780> high-level<00:29:32.050> just<00:29:32.710> know<00:29:33.550> the 00:29:33.630 --> 00:29:33.640 align:start position:0% more sort of high-level just know the 00:29:33.640 --> 00:29:35.040 align:start position:0% more sort of high-level just know the paper<00:29:33.820> is<00:29:33.970> really<00:29:34.180> good<00:29:34.330> it's<00:29:34.480> just<00:29:34.600> that<00:29:34.780> it's 00:29:35.040 --> 00:29:35.050 align:start position:0% paper is really good it's just that it's 00:29:35.050 --> 00:29:37.590 align:start position:0% paper is really good it's just that it's set<00:29:35.200> theory<00:29:35.410> okay<00:29:36.310> it's<00:29:36.490> very<00:29:36.760> accessible<00:29:37.090> I 00:29:37.590 --> 00:29:37.600 align:start position:0% set theory okay it's very accessible I 00:29:37.600 --> 00:29:41.350 align:start position:0% set theory okay it's very accessible I think<00:29:37.630> okay 00:29:41.350 --> 00:29:41.360 align:start position:0% 00:29:41.360 --> 00:29:42.130 align:start position:0% you 00:29:42.130 --> 00:29:42.140 align:start position:0% you 00:29:42.140 --> 00:29:55.840 align:start position:0% you [Applause] 00:29:55.840 --> 00:29:55.850 align:start position:0% 00:29:55.850 --> 00:29:57.910 align:start position:0% you