WEBVTT Kind: captions Language: en 00:00:01.070 --> 00:00:12.610 align:start position:0% [Applause] 00:00:12.610 --> 00:00:12.620 align:start position:0% 00:00:12.620 --> 00:00:16.039 align:start position:0% it's<00:00:13.620> part<00:00:13.830> contracts<00:00:14.250> and<00:00:14.630> how<00:00:15.630> inductive 00:00:16.039 --> 00:00:16.049 align:start position:0% it's part contracts and how inductive 00:00:16.049 --> 00:00:21.350 align:start position:0% it's part contracts and how inductive covariance<00:00:16.550> help<00:00:18.560> help<00:00:19.560> prove<00:00:20.360> assertions 00:00:21.350 --> 00:00:21.360 align:start position:0% covariance help help prove assertions 00:00:21.360 --> 00:00:23.420 align:start position:0% covariance help help prove assertions that<00:00:21.480> should<00:00:21.960> be<00:00:22.110> true<00:00:22.410> on<00:00:22.920> the<00:00:23.070> contract 00:00:23.420 --> 00:00:23.430 align:start position:0% that should be true on the contract 00:00:23.430 --> 00:00:26.240 align:start position:0% that should be true on the contract level<00:00:23.990> concerning<00:00:24.990> an<00:00:25.140> unbounded<00:00:25.740> number<00:00:25.800> of 00:00:26.240 --> 00:00:26.250 align:start position:0% level concerning an unbounded number of 00:00:26.250 --> 00:00:28.429 align:start position:0% level concerning an unbounded number of concessions<00:00:26.790> this<00:00:27.750> is<00:00:27.900> all<00:00:28.079> implemented 00:00:28.429 --> 00:00:28.439 align:start position:0% concessions this is all implemented 00:00:28.439 --> 00:00:30.470 align:start position:0% concessions this is all implemented inside<00:00:29.070> the<00:00:29.279> compiler<00:00:29.669> into<00:00:30.000> multiple 00:00:30.470 --> 00:00:30.480 align:start position:0% inside the compiler into multiple 00:00:30.480 --> 00:00:33.530 align:start position:0% inside the compiler into multiple destiny<00:00:30.990> checker<00:00:31.230> which<00:00:32.189> runs<00:00:32.550> to<00:00:33.300> use<00:00:33.510> a 00:00:33.530 --> 00:00:33.540 align:start position:0% destiny checker which runs to use a 00:00:33.540 --> 00:00:36.410 align:start position:0% destiny checker which runs to use a program<00:00:33.840> experimental<00:00:34.530> sent<00:00:34.710> to<00:00:34.800> checker<00:00:35.420> the 00:00:36.410 --> 00:00:36.420 align:start position:0% program experimental sent to checker the 00:00:36.420 --> 00:00:38.420 align:start position:0% program experimental sent to checker the Rhondda<00:00:36.960> compilers<00:00:37.380> in<00:00:37.500> aesthetic<00:00:37.950> analysis 00:00:38.420 --> 00:00:38.430 align:start position:0% Rhondda compilers in aesthetic analysis 00:00:38.430 --> 00:00:40.580 align:start position:0% Rhondda compilers in aesthetic analysis trying<00:00:38.670> to<00:00:38.850> prove<00:00:39.090> that<00:00:39.450> the<00:00:40.110> assertions<00:00:40.530> have 00:00:40.580 --> 00:00:40.590 align:start position:0% trying to prove that the assertions have 00:00:40.590 --> 00:00:43.160 align:start position:0% trying to prove that the assertions have in<00:00:40.890> your<00:00:41.010> contract<00:00:41.400> are<00:00:41.610> never<00:00:41.910> violated<00:00:42.450> no 00:00:43.160 --> 00:00:43.170 align:start position:0% in your contract are never violated no 00:00:43.170 --> 00:00:48.230 align:start position:0% in your contract are never violated no matter<00:00:43.410> the<00:00:43.740> number<00:00:43.920> of<00:00:45.080> transactions<00:00:47.240> so 00:00:48.230 --> 00:00:48.240 align:start position:0% matter the number of transactions so 00:00:48.240 --> 00:00:51.140 align:start position:0% matter the number of transactions so first<00:00:48.870> I'm<00:00:49.170> gonna<00:00:49.320> start<00:00:49.440> at<00:00:49.710> the<00:00:49.860> demo<00:00:50.220> as 00:00:51.140 --> 00:00:51.150 align:start position:0% first I'm gonna start at the demo as 00:00:51.150 --> 00:00:54.470 align:start position:0% first I'm gonna start at the demo as priest<00:00:51.540> as<00:00:51.750> small<00:00:52.230> as<00:00:52.530> you're<00:00:52.710> getting<00:00:52.890> this<00:00:53.820> I 00:00:54.470 --> 00:00:54.480 align:start position:0% priest as small as you're getting this I 00:00:54.480 --> 00:00:56.120 align:start position:0% priest as small as you're getting this I have<00:00:54.690> a<00:00:54.780> really<00:00:54.930> tiny<00:00:55.200> contract<00:00:55.680> that<00:00:55.830> Sigma 00:00:56.120 --> 00:00:56.130 align:start position:0% have a really tiny contract that Sigma 00:00:56.130 --> 00:00:59.360 align:start position:0% have a really tiny contract that Sigma that<00:00:56.310> firma<00:00:57.090> pega<00:00:57.300> lace<00:00:57.600> overlay<00:00:58.010> toy<00:00:59.010> state 00:00:59.360 --> 00:00:59.370 align:start position:0% that firma pega lace overlay toy state 00:00:59.370 --> 00:01:00.980 align:start position:0% that firma pega lace overlay toy state machines<00:00:59.730> that<00:00:59.970> have<00:01:00.090> a<00:01:00.120> state<00:01:00.360> permit<00:01:00.570> enact 00:01:00.980 --> 00:01:00.990 align:start position:0% machines that have a state permit enact 00:01:00.990 --> 00:01:04.579 align:start position:0% machines that have a state permit enact a<00:01:01.320> function<00:01:02.130> and<00:01:02.370> that<00:01:02.720> changes<00:01:03.720> ax<00:01:03.990> from<00:01:04.140> 0<00:01:04.439> to 00:01:04.579 --> 00:01:04.589 align:start position:0% a function and that changes ax from 0 to 00:01:04.589 --> 00:01:06.380 align:start position:0% a function and that changes ax from 0 to 1<00:01:04.830> so<00:01:05.159> X<00:01:05.369> star<00:01:05.519> to<00:01:05.729> the<00:01:05.790> Syrian<00:01:06.240> in<00:01:06.330> the 00:01:06.380 --> 00:01:06.390 align:start position:0% 1 so X star to the Syrian in the 00:01:06.390 --> 00:01:11.090 align:start position:0% 1 so X star to the Syrian in the constructor<00:01:08.869> G<00:01:09.869> changes<00:01:10.259> one<00:01:10.650> back<00:01:10.920> to 00:01:11.090 --> 00:01:11.100 align:start position:0% constructor G changes one back to 00:01:11.100 --> 00:01:12.649 align:start position:0% constructor G changes one back to serious<00:01:11.430> they<00:01:11.549> have<00:01:11.759> the<00:01:11.909> state<00:01:12.119> machine<00:01:12.420> that 00:01:12.649 --> 00:01:12.659 align:start position:0% serious they have the state machine that 00:01:12.659 --> 00:01:14.600 align:start position:0% serious they have the state machine that starts<00:01:12.960> with<00:01:13.020> 0<00:01:13.350> and<00:01:13.470> then<00:01:13.650> you<00:01:13.770> can<00:01:14.040> go<00:01:14.190> to<00:01:14.220> one 00:01:14.600 --> 00:01:14.610 align:start position:0% starts with 0 and then you can go to one 00:01:14.610 --> 00:01:16.970 align:start position:0% starts with 0 and then you can go to one and<00:01:14.909> go<00:01:15.659> back<00:01:15.900> to<00:01:16.020> Sierra<00:01:16.290> and<00:01:16.380> just<00:01:16.590> keep 00:01:16.970 --> 00:01:16.980 align:start position:0% and go back to Sierra and just keep 00:01:16.980 --> 00:01:19.250 align:start position:0% and go back to Sierra and just keep doing<00:01:17.190> this<00:01:17.280> forever<00:01:17.520> and<00:01:17.940> then<00:01:18.690> I<00:01:18.720> have<00:01:18.930> this 00:01:19.250 --> 00:01:19.260 align:start position:0% doing this forever and then I have this 00:01:19.260 --> 00:01:21.350 align:start position:0% doing this forever and then I have this third<00:01:19.650> function<00:01:19.920> called<00:01:20.280> in<00:01:20.370> grant<00:01:20.580> asserts 00:01:21.350 --> 00:01:21.360 align:start position:0% third function called in grant asserts 00:01:21.360 --> 00:01:24.980 align:start position:0% third function called in grant asserts that<00:01:21.690> X<00:01:22.260> less<00:01:22.830> or<00:01:23.010> equal<00:01:23.100> one<00:01:23.400> and<00:01:23.930> this<00:01:24.930> is 00:01:24.980 --> 00:01:24.990 align:start position:0% that X less or equal one and this is 00:01:24.990 --> 00:01:27.500 align:start position:0% that X less or equal one and this is this<00:01:25.440> function<00:01:26.100> very<00:01:26.310> public<00:01:26.790> so<00:01:27.300> whenever 00:01:27.500 --> 00:01:27.510 align:start position:0% this function very public so whenever 00:01:27.510 --> 00:01:29.330 align:start position:0% this function very public so whenever you<00:01:27.690> call<00:01:27.960> it<00:01:28.110> it<00:01:28.320> should<00:01:28.500> be<00:01:28.650> true<00:01:28.920> inner<00:01:29.190> wise 00:01:29.330 --> 00:01:29.340 align:start position:0% you call it it should be true inner wise 00:01:29.340 --> 00:01:33.440 align:start position:0% you call it it should be true inner wise what<00:01:29.970> the<00:01:30.060> restaurant<00:01:30.270> report<00:01:30.540> right<00:01:32.450> so 00:01:33.440 --> 00:01:33.450 align:start position:0% what the restaurant report right so 00:01:33.450 --> 00:01:40.790 align:start position:0% what the restaurant report right so these<00:01:33.690> things<00:01:33.930> and<00:01:34.110> assertions<00:01:34.350> true 00:01:40.790 --> 00:01:40.800 align:start position:0% 00:01:40.800 --> 00:01:43.220 align:start position:0% I'm<00:01:41.800> in<00:01:41.920> disguise 00:01:43.220 --> 00:01:43.230 align:start position:0% I'm in disguise 00:01:43.230 --> 00:01:45.540 align:start position:0% I'm in disguise so<00:01:44.230> because<00:01:44.620> of<00:01:44.650> Ulysses<00:01:45.160> constructure 00:01:45.540 --> 00:01:45.550 align:start position:0% so because of Ulysses constructure 00:01:45.550 --> 00:01:49.620 align:start position:0% so because of Ulysses constructure accident<00:01:46.240> is<00:01:46.330> interrelation<00:01:46.930> zero<00:01:47.200> right<00:01:48.630> so 00:01:49.620 --> 00:01:49.630 align:start position:0% accident is interrelation zero right so 00:01:49.630 --> 00:01:51.210 align:start position:0% accident is interrelation zero right so you'll<00:01:49.840> start<00:01:50.080> at<00:01:50.170> zero<00:01:50.380> you<00:01:50.680> might<00:01:51.010> go<00:01:51.190> to 00:01:51.210 --> 00:01:51.220 align:start position:0% you'll start at zero you might go to 00:01:51.220 --> 00:01:53.460 align:start position:0% you'll start at zero you might go to point<00:01:51.670> if<00:01:51.790> you<00:01:51.880> go<00:01:52.000> laughs<00:01:52.240> you<00:01:52.930> might<00:01:53.080> go<00:01:53.260> back 00:01:53.460 --> 00:01:53.470 align:start position:0% point if you go laughs you might go back 00:01:53.470 --> 00:01:55.200 align:start position:0% point if you go laughs you might go back to<00:01:53.500> zero<00:01:54.250> if<00:01:54.550> you're<00:01:54.700> gonna<00:01:54.820> cheat<00:01:55.030> after 00:01:55.200 --> 00:01:55.210 align:start position:0% to zero if you're gonna cheat after 00:01:55.210 --> 00:01:57.600 align:start position:0% to zero if you're gonna cheat after building<00:01:55.570> up<00:01:55.780> so<00:01:56.380> it<00:01:56.680> is<00:01:56.770> true<00:01:57.010> right<00:01:57.490> in 00:01:57.600 --> 00:01:57.610 align:start position:0% building up so it is true right in 00:01:57.610 --> 00:01:58.950 align:start position:0% building up so it is true right in future<00:01:58.120> yeah 00:01:58.950 --> 00:01:58.960 align:start position:0% future yeah 00:01:58.960 --> 00:02:02.100 align:start position:0% future yeah and<00:01:59.340> this<00:02:00.340> is<00:02:00.490> what<00:02:00.729> destiny<00:02:01.270> checkers<00:02:01.840> and 00:02:02.100 --> 00:02:02.110 align:start position:0% and this is what destiny checkers and 00:02:02.110 --> 00:02:04.230 align:start position:0% and this is what destiny checkers and then<00:02:02.200> try<00:02:02.470> to<00:02:02.500> improve<00:02:03.010> that<00:02:03.760> that<00:02:04.000> assertion 00:02:04.230 --> 00:02:04.240 align:start position:0% then try to improve that that assertion 00:02:04.240 --> 00:02:07.200 align:start position:0% then try to improve that that assertion is<00:02:04.420> always<00:02:04.690> true<00:02:04.840> so<00:02:05.610> if<00:02:06.610> we<00:02:06.729> look<00:02:06.970> at<00:02:07.120> this 00:02:07.200 --> 00:02:07.210 align:start position:0% is always true so if we look at this 00:02:07.210 --> 00:02:09.090 align:start position:0% is always true so if we look at this program<00:02:07.479> as<00:02:07.810> the<00:02:08.020> actual<00:02:08.320> state<00:02:08.560> machine<00:02:08.890> as 00:02:09.090 --> 00:02:09.100 align:start position:0% program as the actual state machine as 00:02:09.100 --> 00:02:10.740 align:start position:0% program as the actual state machine as asking<00:02:09.340> for<00:02:09.399> flow<00:02:09.640> graph<00:02:09.880> we<00:02:10.509> have<00:02:10.660> the 00:02:10.740 --> 00:02:10.750 align:start position:0% asking for flow graph we have the 00:02:10.750 --> 00:02:12.960 align:start position:0% asking for flow graph we have the constructor<00:02:11.260> initializes<00:02:11.860> X<00:02:12.340> of<00:02:12.459> zero<00:02:12.700> and 00:02:12.960 --> 00:02:12.970 align:start position:0% constructor initializes X of zero and 00:02:12.970 --> 00:02:15.300 align:start position:0% constructor initializes X of zero and then<00:02:13.270> it<00:02:13.300> goes<00:02:13.540> to<00:02:13.810> this<00:02:13.990> liability<00:02:14.440> disperse 00:02:15.300 --> 00:02:15.310 align:start position:0% then it goes to this liability disperse 00:02:15.310 --> 00:02:17.430 align:start position:0% then it goes to this liability disperse official<00:02:15.790> know<00:02:16.480> that<00:02:16.720> I<00:02:16.780> call<00:02:16.930> the<00:02:17.050> interface 00:02:17.430 --> 00:02:17.440 align:start position:0% official know that I call the interface 00:02:17.440 --> 00:02:20.310 align:start position:0% official know that I call the interface which<00:02:18.100> is<00:02:18.130> the<00:02:18.850> Iowa<00:02:19.120> State<00:02:19.390> of<00:02:19.570> the<00:02:19.780> awesomer 00:02:20.310 --> 00:02:20.320 align:start position:0% which is the Iowa State of the awesomer 00:02:20.320 --> 00:02:22.920 align:start position:0% which is the Iowa State of the awesomer contract<00:02:20.709> right<00:02:20.890> doesn't<00:02:21.280> have<00:02:21.550> an<00:02:21.730> active<00:02:22.150> an 00:02:22.920 --> 00:02:22.930 align:start position:0% contract right doesn't have an active an 00:02:22.930 --> 00:02:24.660 align:start position:0% contract right doesn't have an active an execution<00:02:23.530> you<00:02:23.709> have<00:02:23.860> to<00:02:24.010> call<00:02:24.220> it<00:02:24.370> so<00:02:24.550> it's 00:02:24.660 --> 00:02:24.670 align:start position:0% execution you have to call it so it's 00:02:24.670 --> 00:02:27.120 align:start position:0% execution you have to call it so it's late<00:02:24.880> for<00:02:25.060> this<00:02:25.120> interface<00:02:25.690> until<00:02:26.500> you<00:02:26.860> call<00:02:27.100> a 00:02:27.120 --> 00:02:27.130 align:start position:0% late for this interface until you call a 00:02:27.130 --> 00:02:28.949 align:start position:0% late for this interface until you call a function<00:02:27.430> from<00:02:28.120> the<00:02:28.240> contract<00:02:28.630> which<00:02:28.750> give<00:02:28.930> me 00:02:28.949 --> 00:02:28.959 align:start position:0% function from the contract which give me 00:02:28.959 --> 00:02:32.640 align:start position:0% function from the contract which give me a<00:02:29.080> tagine<00:02:29.620> or<00:02:29.860> a<00:02:30.430> variant<00:02:30.850> to<00:02:31.330> ask<00:02:31.650> changes 00:02:32.640 --> 00:02:32.650 align:start position:0% a tagine or a variant to ask changes 00:02:32.650 --> 00:02:35.160 align:start position:0% a tagine or a variant to ask changes might<00:02:32.890> change<00:02:33.070> X<00:02:33.340> goes<00:02:34.090> back<00:02:34.270> interface<00:02:34.780> Ji 00:02:35.160 --> 00:02:35.170 align:start position:0% might change X goes back interface Ji 00:02:35.170 --> 00:02:37.260 align:start position:0% might change X goes back interface Ji sang<00:02:35.560> an<00:02:35.830> invariant<00:02:36.459> you<00:02:36.520> can<00:02:36.670> go<00:02:36.790> to<00:02:36.850> sync 00:02:37.260 --> 00:02:37.270 align:start position:0% sang an invariant you can go to sync 00:02:37.270 --> 00:02:39.960 align:start position:0% sang an invariant you can go to sync error<00:02:37.480> state<00:02:37.840> if<00:02:38.290> the<00:02:38.500> assertion<00:02:38.830> is<00:02:38.860> false<00:02:39.190> so 00:02:39.960 --> 00:02:39.970 align:start position:0% error state if the assertion is false so 00:02:39.970 --> 00:02:41.160 align:start position:0% error state if the assertion is false so what<00:02:40.060> has<00:02:40.180> the<00:02:40.300> destined<00:02:40.630> to<00:02:40.720> checkers<00:02:40.959> gonna 00:02:41.160 --> 00:02:41.170 align:start position:0% what has the destined to checkers gonna 00:02:41.170 --> 00:02:44.790 align:start position:0% what has the destined to checkers gonna try<00:02:41.380> to<00:02:41.440> do<00:02:41.650> is<00:02:42.300> statically<00:02:43.300> see<00:02:44.230> we<00:02:44.470> can<00:02:44.620> have 00:02:44.790 --> 00:02:44.800 align:start position:0% try to do is statically see we can have 00:02:44.800 --> 00:02:47.370 align:start position:0% try to do is statically see we can have a<00:02:44.830> path<00:02:45.130> from<00:02:45.820> the<00:02:46.000> constructor<00:02:46.540> all<00:02:46.900> the<00:02:47.260> way 00:02:47.370 --> 00:02:47.380 align:start position:0% a path from the constructor all the way 00:02:47.380 --> 00:02:50.460 align:start position:0% a path from the constructor all the way to<00:02:47.440> the<00:02:47.650> mirror<00:02:47.860> state<00:02:48.220> and<00:02:48.989> for<00:02:49.989> that<00:02:50.170> you 00:02:50.460 --> 00:02:50.470 align:start position:0% to the mirror state and for that you 00:02:50.470 --> 00:02:53.460 align:start position:0% to the mirror state and for that you might<00:02:50.680> actually<00:02:51.550> go<00:02:52.030> through<00:02:52.750> this<00:02:52.900> loop<00:02:53.140> a 00:02:53.460 --> 00:02:53.470 align:start position:0% might actually go through this loop a 00:02:53.470 --> 00:02:54.540 align:start position:0% might actually go through this loop a bunch<00:02:54.100> of<00:02:54.160> times 00:02:54.540 --> 00:02:54.550 align:start position:0% bunch of times 00:02:54.550 --> 00:02:56.970 align:start position:0% bunch of times it's<00:02:55.299> gonna<00:02:55.450> try<00:02:55.720> to<00:02:55.780> see<00:02:56.620> if<00:02:56.650> you<00:02:56.709> can<00:02:56.860> go 00:02:56.970 --> 00:02:56.980 align:start position:0% it's gonna try to see if you can go 00:02:56.980 --> 00:02:58.020 align:start position:0% it's gonna try to see if you can go through<00:02:57.010> the<00:02:57.220> constructor<00:02:57.580> to<00:02:57.760> the<00:02:57.850> arrow 00:02:58.020 --> 00:02:58.030 align:start position:0% through the constructor to the arrow 00:02:58.030 --> 00:02:59.670 align:start position:0% through the constructor to the arrow state<00:02:58.390> no<00:02:58.900> matter<00:02:59.110> the<00:02:59.260> number<00:02:59.530> of 00:02:59.670 --> 00:02:59.680 align:start position:0% state no matter the number of 00:02:59.680 --> 00:03:01.170 align:start position:0% state no matter the number of transactions<00:03:00.340> you<00:03:00.459> might<00:03:00.760> have<00:03:00.940> to<00:03:01.060> go 00:03:01.170 --> 00:03:01.180 align:start position:0% transactions you might have to go 00:03:01.180 --> 00:03:07.310 align:start position:0% transactions you might have to go through<00:03:01.980> so<00:03:02.980> I'm<00:03:03.489> gonna<00:03:03.760> try<00:03:04.720> it<00:03:05.250> so<00:03:06.250> this<00:03:06.280> is 00:03:07.310 --> 00:03:07.320 align:start position:0% through so I'm gonna try it so this is 00:03:07.320 --> 00:03:11.740 align:start position:0% through so I'm gonna try it so this is yeah<00:03:08.320> this<00:03:08.350> is<00:03:08.590> a<00:03:08.620> KO 00:03:11.740 --> 00:03:11.750 align:start position:0% 00:03:11.750 --> 00:03:14.970 align:start position:0% and<00:03:12.140> I'm<00:03:12.860> just<00:03:13.070> gonna<00:03:13.190> run<00:03:13.490> compiler<00:03:13.970> on<00:03:14.240> it 00:03:14.970 --> 00:03:14.980 align:start position:0% and I'm just gonna run compiler on it 00:03:14.980 --> 00:03:17.470 align:start position:0% and I'm just gonna run compiler on it and<00:03:15.980> it<00:03:16.250> does<00:03:16.400> not<00:03:16.580> say<00:03:16.910> that<00:03:17.090> it's<00:03:17.210> wrong 00:03:17.470 --> 00:03:17.480 align:start position:0% and it does not say that it's wrong 00:03:17.480 --> 00:03:19.750 align:start position:0% and it does not say that it's wrong therefore<00:03:18.320> it's<00:03:18.410> for<00:03:18.650> its<00:03:18.920> sorry 00:03:19.750 --> 00:03:19.760 align:start position:0% therefore it's for its sorry 00:03:19.760 --> 00:03:21.370 align:start position:0% therefore it's for its sorry it<00:03:19.880> does<00:03:20.270> not<00:03:20.420> say<00:03:20.630> it<00:03:20.690> wrong<00:03:20.840> therefore<00:03:21.110> it's 00:03:21.370 --> 00:03:21.380 align:start position:0% it does not say it wrong therefore it's 00:03:21.380 --> 00:03:24.160 align:start position:0% it does not say it wrong therefore it's safe<00:03:21.590> but<00:03:22.550> compiler<00:03:23.030> also<00:03:23.210> puts<00:03:23.660> a<00:03:23.750> bunch<00:03:23.960> of 00:03:24.160 --> 00:03:24.170 align:start position:0% safe but compiler also puts a bunch of 00:03:24.170 --> 00:03:26.560 align:start position:0% safe but compiler also puts a bunch of weird<00:03:24.560> stuff<00:03:24.830> that's<00:03:25.270> instantly<00:03:26.270> but<00:03:26.420> it's 00:03:26.560 --> 00:03:26.570 align:start position:0% weird stuff that's instantly but it's 00:03:26.570 --> 00:03:28.840 align:start position:0% weird stuff that's instantly but it's going<00:03:26.690> to<00:03:26.750> look<00:03:26.870> nice<00:03:27.170> eventually<00:03:27.680> but<00:03:28.490> it's 00:03:28.840 --> 00:03:28.850 align:start position:0% going to look nice eventually but it's 00:03:28.850 --> 00:03:34.180 align:start position:0% going to look nice eventually but it's part<00:03:29.150> of<00:03:29.240> it<00:03:30.460> what<00:03:31.460> it<00:03:31.580> tells<00:03:31.760> us<00:03:31.940> is<00:03:33.190> this 00:03:34.180 --> 00:03:34.190 align:start position:0% part of it what it tells us is this 00:03:34.190 --> 00:03:36.130 align:start position:0% part of it what it tells us is this thing<00:03:34.700> here<00:03:34.970> so<00:03:35.210> what<00:03:35.510> this<00:03:35.630> is<00:03:35.750> telling<00:03:35.780> us 00:03:36.130 --> 00:03:36.140 align:start position:0% thing here so what this is telling us 00:03:36.140 --> 00:03:39.130 align:start position:0% thing here so what this is telling us this<00:03:36.500> is<00:03:36.560> a<00:03:37.180> contract<00:03:38.180> invariant 00:03:39.130 --> 00:03:39.140 align:start position:0% this is a contract invariant 00:03:39.140 --> 00:03:43.720 align:start position:0% this is a contract invariant because<00:03:39.890> it's<00:03:40.340> an<00:03:40.520> invariant<00:03:41.000> on<00:03:41.890> on<00:03:42.890> the 00:03:43.720 --> 00:03:43.730 align:start position:0% because it's an invariant on on the 00:03:43.730 --> 00:03:46.750 align:start position:0% because it's an invariant on on the interface<00:03:44.540> node<00:03:44.960> so<00:03:45.950> this<00:03:46.370> is<00:03:46.460> telling<00:03:46.610> us 00:03:46.750 --> 00:03:46.760 align:start position:0% interface node so this is telling us 00:03:46.760 --> 00:03:49.000 align:start position:0% interface node so this is telling us that<00:03:46.820> on<00:03:47.270> the<00:03:47.390> interface<00:03:47.780> node<00:03:48.110> it's<00:03:48.440> always 00:03:49.000 --> 00:03:49.010 align:start position:0% that on the interface node it's always 00:03:49.010 --> 00:03:52.270 align:start position:0% that on the interface node it's always true<00:03:49.310> for<00:03:49.790> all<00:03:50.030> values<00:03:50.060> that<00:03:50.690> X<00:03:50.930> can<00:03:51.280> happen 00:03:52.270 --> 00:03:52.280 align:start position:0% true for all values that X can happen 00:03:52.280 --> 00:03:56.860 align:start position:0% true for all values that X can happen that<00:03:52.700> X<00:03:53.330> is<00:03:54.080> less<00:03:54.680> than<00:03:54.710> 2<00:03:55.070> right<00:03:56.000> and<00:03:56.360> because 00:03:56.860 --> 00:03:56.870 align:start position:0% that X is less than 2 right and because 00:03:56.870 --> 00:03:58.750 align:start position:0% that X is less than 2 right and because we've<00:03:57.140> talked<00:03:57.290> about<00:03:57.380> integers<00:03:57.770> this<00:03:58.430> means 00:03:58.750 --> 00:03:58.760 align:start position:0% we've talked about integers this means 00:03:58.760 --> 00:04:01.380 align:start position:0% we've talked about integers this means it<00:03:59.150> is<00:03:59.540> the<00:03:59.600> same<00:03:59.720> as<00:04:00.050> X<00:04:00.590> less<00:04:00.830> or<00:04:00.980> equal<00:04:01.040> 1 00:04:01.380 --> 00:04:01.390 align:start position:0% it is the same as X less or equal 1 00:04:01.390 --> 00:04:06.010 align:start position:0% it is the same as X less or equal 1 right<00:04:02.390> which<00:04:02.570> in<00:04:02.750> this<00:04:02.900> case<00:04:03.170> is<00:04:04.870> which<00:04:05.870> in 00:04:06.010 --> 00:04:06.020 align:start position:0% right which in this case is which in 00:04:06.020 --> 00:04:11.340 align:start position:0% right which in this case is which in this<00:04:06.140> case<00:04:06.350> is<00:04:06.650> the<00:04:06.770> same<00:04:08.110> as<00:04:09.110> our<00:04:09.380> second<00:04:09.950> year 00:04:11.340 --> 00:04:11.350 align:start position:0% this case is the same as our second year 00:04:11.350 --> 00:04:14.800 align:start position:0% this case is the same as our second year but<00:04:12.350> if<00:04:12.470> we<00:04:12.590> change<00:04:12.800> the<00:04:13.040> code<00:04:13.280> slightly<00:04:14.270> here 00:04:14.800 --> 00:04:14.810 align:start position:0% but if we change the code slightly here 00:04:14.810 --> 00:04:20.410 align:start position:0% but if we change the code slightly here so<00:04:15.440> I<00:04:15.500> added<00:04:15.710> this<00:04:15.920> function<00:04:16.370> age<00:04:19.150> but<00:04:20.150> now 00:04:20.410 --> 00:04:20.420 align:start position:0% so I added this function age but now 00:04:20.420 --> 00:04:22.660 align:start position:0% so I added this function age but now it's<00:04:20.810> a<00:04:20.900> new<00:04:21.080> it's<00:04:21.320> a<00:04:21.470> new<00:04:21.500> rule<00:04:21.980> in<00:04:22.280> nursing 00:04:22.660 --> 00:04:22.670 align:start position:0% it's a new it's a new rule in nursing 00:04:22.670 --> 00:04:25.690 align:start position:0% it's a new it's a new rule in nursing machine<00:04:23.000> that<00:04:23.210> says<00:04:23.450> now<00:04:24.080> if<00:04:24.140> x<00:04:24.470> equals<00:04:24.860> 7<00:04:25.280> make 00:04:25.690 --> 00:04:25.700 align:start position:0% machine that says now if x equals 7 make 00:04:25.700 --> 00:04:28.150 align:start position:0% machine that says now if x equals 7 make it<00:04:25.850> 100<00:04:26.270> and<00:04:26.510> then<00:04:27.170> I<00:04:27.200> changed<00:04:27.590> the<00:04:27.710> assertion 00:04:28.150 --> 00:04:28.160 align:start position:0% it 100 and then I changed the assertion 00:04:28.160 --> 00:04:32.620 align:start position:0% it 100 and then I changed the assertion to<00:04:28.400> ax<00:04:29.030> less<00:04:29.300> or<00:04:29.480> equal<00:04:29.570> 7<00:04:31.270> is<00:04:32.270> the<00:04:32.450> assertion 00:04:32.620 --> 00:04:32.630 align:start position:0% to ax less or equal 7 is the assertion 00:04:32.630 --> 00:04:38.530 align:start position:0% to ax less or equal 7 is the assertion correct 00:04:38.530 --> 00:04:38.540 align:start position:0% 00:04:38.540 --> 00:04:41.240 align:start position:0% everything<00:04:39.540> exactly<00:04:40.110> right<00:04:40.410> so<00:04:40.710> this<00:04:40.830> is<00:04:41.040> a 00:04:41.240 --> 00:04:41.250 align:start position:0% everything exactly right so this is a 00:04:41.250 --> 00:04:44.060 align:start position:0% everything exactly right so this is a weird<00:04:41.730> local<00:04:42.180> state<00:04:42.420> which<00:04:43.380> considering<00:04:43.950> the 00:04:44.060 --> 00:04:44.070 align:start position:0% weird local state which considering the 00:04:44.070 --> 00:04:46.730 align:start position:0% weird local state which considering the global<00:04:44.460> contract<00:04:45.030> state<00:04:45.300> it's<00:04:46.110> useless 00:04:46.730 --> 00:04:46.740 align:start position:0% global contract state it's useless 00:04:46.740 --> 00:04:49.790 align:start position:0% global contract state it's useless right<00:04:47.360> but<00:04:48.360> still<00:04:48.600> we<00:04:48.750> try<00:04:48.780> professors<00:04:49.500> in<00:04:49.620> any 00:04:49.790 --> 00:04:49.800 align:start position:0% right but still we try professors in any 00:04:49.800 --> 00:04:58.100 align:start position:0% right but still we try professors in any way<00:04:49.980> and<00:04:51.920> when<00:04:52.920> we<00:04:53.010> do<00:04:53.190> that<00:04:56.840> the<00:04:57.840> compiler 00:04:58.100 --> 00:04:58.110 align:start position:0% way and when we do that the compiler 00:04:58.110 --> 00:05:00.320 align:start position:0% way and when we do that the compiler also<00:04:58.560> says<00:04:58.740> to<00:04:58.890> save<00:04:59.130> and<00:04:59.430> also<00:04:59.910> gives<00:05:00.090> us<00:05:00.270> a 00:05:00.320 --> 00:05:00.330 align:start position:0% also says to save and also gives us a 00:05:00.330 --> 00:05:02.300 align:start position:0% also says to save and also gives us a bunch<00:05:00.630> of<00:05:00.690> information<00:05:00.810> again<00:05:01.350> about<00:05:01.890> things 00:05:02.300 --> 00:05:02.310 align:start position:0% bunch of information again about things 00:05:02.310 --> 00:05:04.160 align:start position:0% bunch of information again about things that<00:05:02.400> are<00:05:02.580> true<00:05:02.850> at<00:05:03.180> certain<00:05:03.600> points<00:05:03.990> in<00:05:04.110> the 00:05:04.160 --> 00:05:04.170 align:start position:0% that are true at certain points in the 00:05:04.170 --> 00:05:08.540 align:start position:0% that are true at certain points in the cleaner<00:05:04.410> flow<00:05:04.620> graph<00:05:04.890> and<00:05:06.860> similarly<00:05:07.860> we<00:05:08.310> can 00:05:08.540 --> 00:05:08.550 align:start position:0% cleaner flow graph and similarly we can 00:05:08.550 --> 00:05:10.340 align:start position:0% cleaner flow graph and similarly we can check<00:05:09.150> what's<00:05:09.390> going<00:05:09.570> on<00:05:09.750> with<00:05:09.900> the<00:05:09.990> interface 00:05:10.340 --> 00:05:10.350 align:start position:0% check what's going on with the interface 00:05:10.350 --> 00:05:13.160 align:start position:0% check what's going on with the interface now<00:05:10.620> and<00:05:11.190> it<00:05:11.490> gives<00:05:11.610> us<00:05:11.820> the<00:05:11.940> same<00:05:11.970> be<00:05:12.930> very 00:05:13.160 --> 00:05:13.170 align:start position:0% now and it gives us the same be very 00:05:13.170 --> 00:05:13.820 align:start position:0% now and it gives us the same be very again 00:05:13.820 --> 00:05:13.830 align:start position:0% again 00:05:13.830 --> 00:05:17.630 align:start position:0% again so<00:05:14.430> before<00:05:15.150> I<00:05:15.180> try<00:05:15.510> to<00:05:15.570> prove<00:05:15.840> X<00:05:16.430> less<00:05:17.430> or<00:05:17.550> equal 00:05:17.630 --> 00:05:17.640 align:start position:0% so before I try to prove X less or equal 00:05:17.640 --> 00:05:20.300 align:start position:0% so before I try to prove X less or equal 1<00:05:17.970> and<00:05:18.210> they<00:05:18.510> gave<00:05:18.690> me<00:05:18.720> accessory<00:05:19.470> for<00:05:19.620> one<00:05:19.800> to 00:05:20.300 --> 00:05:20.310 align:start position:0% 1 and they gave me accessory for one to 00:05:20.310 --> 00:05:23.000 align:start position:0% 1 and they gave me accessory for one to learn<00:05:20.580> that<00:05:20.910> but<00:05:21.660> now<00:05:21.810> I'm<00:05:22.050> trying<00:05:22.260> to<00:05:22.350> prove<00:05:22.560> X 00:05:23.000 --> 00:05:23.010 align:start position:0% learn that but now I'm trying to prove X 00:05:23.010 --> 00:05:24.950 align:start position:0% learn that but now I'm trying to prove X lesser<00:05:23.340> equals<00:05:23.610> seven<00:05:23.940> and<00:05:24.420> it<00:05:24.510> still<00:05:24.750> gives 00:05:24.950 --> 00:05:24.960 align:start position:0% lesser equals seven and it still gives 00:05:24.960 --> 00:05:27.830 align:start position:0% lesser equals seven and it still gives me<00:05:25.230> X<00:05:25.800> less<00:05:26.040> or<00:05:26.190> equal<00:05:26.280> one<00:05:26.550> even<00:05:27.540> though<00:05:27.690> I'm 00:05:27.830 --> 00:05:27.840 align:start position:0% me X less or equal one even though I'm 00:05:27.840 --> 00:05:29.290 align:start position:0% me X less or equal one even though I'm trying<00:05:27.990> to<00:05:28.140> prove<00:05:28.260> something<00:05:28.500> else 00:05:29.290 --> 00:05:29.300 align:start position:0% trying to prove something else 00:05:29.300 --> 00:05:32.600 align:start position:0% trying to prove something else so<00:05:30.300> both<00:05:31.140> these<00:05:31.530> two<00:05:31.860> properties<00:05:32.310> are 00:05:32.600 --> 00:05:32.610 align:start position:0% so both these two properties are 00:05:32.610 --> 00:05:34.370 align:start position:0% so both these two properties are invariance<00:05:33.120> of<00:05:33.240> the<00:05:33.330> contract<00:05:33.720> right<00:05:33.900> so<00:05:34.200> you 00:05:34.370 --> 00:05:34.380 align:start position:0% invariance of the contract right so you 00:05:34.380 --> 00:05:36.590 align:start position:0% invariance of the contract right so you can<00:05:34.500> probably<00:05:34.620> prove<00:05:34.980> that<00:05:35.070> they're<00:05:35.250> true<00:05:35.600> but 00:05:36.590 --> 00:05:36.600 align:start position:0% can probably prove that they're true but 00:05:36.600 --> 00:05:38.750 align:start position:0% can probably prove that they're true but they<00:05:37.260> have<00:05:37.470> to<00:05:37.590> be<00:05:37.680> different<00:05:38.070> somehow<00:05:38.280> so 00:05:38.750 --> 00:05:38.760 align:start position:0% they have to be different somehow so 00:05:38.760 --> 00:05:41.240 align:start position:0% they have to be different somehow so what<00:05:39.570> is<00:05:39.660> the<00:05:39.750> difference<00:05:40.110> between<00:05:40.200> X<00:05:40.800> less<00:05:41.100> or 00:05:41.240 --> 00:05:41.250 align:start position:0% what is the difference between X less or 00:05:41.250 --> 00:05:45.940 align:start position:0% what is the difference between X less or equal<00:05:41.310> to<00:05:41.640> and<00:05:41.910> ax<00:05:42.780> less<00:05:43.020> or<00:05:43.170> equal<00:05:43.260> seven<00:05:43.710> I 00:05:45.940 --> 00:05:45.950 align:start position:0% equal to and ax less or equal seven I 00:05:45.950 --> 00:05:50.680 align:start position:0% equal to and ax less or equal seven I know<00:05:46.950> the<00:05:47.070> answer<00:05:47.280> already<00:05:47.400> doesn't<00:05:48.120> come 00:05:50.680 --> 00:05:50.690 align:start position:0% 00:05:50.690 --> 00:05:55.810 align:start position:0% that's<00:05:51.690> true 00:05:55.810 --> 00:05:55.820 align:start position:0% 00:05:55.820 --> 00:05:58.730 align:start position:0% so<00:05:56.820> the<00:05:56.940> check<00:05:57.150> the<00:05:57.270> difference<00:05:57.740> to 00:05:58.730 --> 00:05:58.740 align:start position:0% so the check the difference to 00:05:58.740 --> 00:06:00.530 align:start position:0% so the check the difference to understand<00:05:59.160> what's<00:05:59.910> fundamental<00:06:00.480> is 00:06:00.530 --> 00:06:00.540 align:start position:0% understand what's fundamental is 00:06:00.540 --> 00:06:02.990 align:start position:0% understand what's fundamental is different<00:06:00.960> in<00:06:01.140> this<00:06:01.350> case<00:06:01.410> between<00:06:02.010> accessory 00:06:02.990 --> 00:06:03.000 align:start position:0% different in this case between accessory 00:06:03.000 --> 00:06:06.020 align:start position:0% different in this case between accessory co2<00:06:03.360> and<00:06:03.540> exit<00:06:03.810> the<00:06:04.050> circle<00:06:04.350> 7<00:06:04.680> we<00:06:05.580> need<00:06:05.910> to 00:06:06.020 --> 00:06:06.030 align:start position:0% co2 and exit the circle 7 we need to 00:06:06.030 --> 00:06:08.450 align:start position:0% co2 and exit the circle 7 we need to analyze<00:06:06.180> each<00:06:06.900> of<00:06:06.930> those<00:06:07.290> variants<00:06:07.800> with 00:06:08.450 --> 00:06:08.460 align:start position:0% analyze each of those variants with 00:06:08.460 --> 00:06:10.160 align:start position:0% analyze each of those variants with respect<00:06:08.970> to<00:06:09.090> each<00:06:09.240> function<00:06:09.870> separately 00:06:10.160 --> 00:06:10.170 align:start position:0% respect to each function separately 00:06:10.170 --> 00:06:13.070 align:start position:0% respect to each function separately without<00:06:11.100> considering<00:06:12.000> the<00:06:12.240> rest<00:06:12.720> of<00:06:12.990> the 00:06:13.070 --> 00:06:13.080 align:start position:0% without considering the rest of the 00:06:13.080 --> 00:06:14.750 align:start position:0% without considering the rest of the state<00:06:13.260> of<00:06:13.380> the<00:06:13.410> complement<00:06:13.860> so<00:06:14.040> randomized 00:06:14.750 --> 00:06:14.760 align:start position:0% state of the complement so randomized 00:06:14.760 --> 00:06:16.970 align:start position:0% state of the complement so randomized each<00:06:14.940> invariant<00:06:15.530> only<00:06:16.530> looking<00:06:16.830> at<00:06:16.890> the 00:06:16.970 --> 00:06:16.980 align:start position:0% each invariant only looking at the 00:06:16.980 --> 00:06:18.980 align:start position:0% each invariant only looking at the function<00:06:17.430> each<00:06:17.820> function<00:06:18.300> without<00:06:18.540> carrying 00:06:18.980 --> 00:06:18.990 align:start position:0% function each function without carrying 00:06:18.990 --> 00:06:20.720 align:start position:0% function each function without carrying as<00:06:19.290> if<00:06:19.440> any<00:06:19.710> other<00:06:19.860> as<00:06:20.160> if<00:06:20.280> that<00:06:20.460> function 00:06:20.720 --> 00:06:20.730 align:start position:0% as if any other as if that function 00:06:20.730 --> 00:06:23.360 align:start position:0% as if any other as if that function thrown<00:06:21.120> will<00:06:21.270> exist<00:06:21.630> the<00:06:21.750> only<00:06:22.130> so<00:06:23.130> you<00:06:23.250> can 00:06:23.360 --> 00:06:23.370 align:start position:0% thrown will exist the only so you can 00:06:23.370 --> 00:06:26.540 align:start position:0% thrown will exist the only so you can point<00:06:23.490> in<00:06:23.760> this<00:06:24.240> degree<00:06:24.450> before<00:06:25.020> by<00:06:25.740> app<00:06:26.160> and 00:06:26.540 --> 00:06:26.550 align:start position:0% point in this degree before by app and 00:06:26.550 --> 00:06:28.910 align:start position:0% point in this degree before by app and then<00:06:26.760> after<00:06:27.570> it<00:06:27.690> as<00:06:27.900> the<00:06:28.080> post<00:06:28.290> condition<00:06:28.710> for 00:06:28.910 --> 00:06:28.920 align:start position:0% then after it as the post condition for 00:06:28.920 --> 00:06:32.800 align:start position:0% then after it as the post condition for app<00:06:29.070> this<00:06:29.910> they<00:06:30.390> very<00:06:30.660> still<00:06:30.930> hold<00:06:31.200> after<00:06:32.190> that 00:06:32.800 --> 00:06:32.810 align:start position:0% app this they very still hold after that 00:06:32.810 --> 00:06:35.990 align:start position:0% app this they very still hold after that it<00:06:33.810> does<00:06:34.080> right<00:06:34.350> because<00:06:35.070> it<00:06:35.220> because<00:06:35.640> even<00:06:35.820> if 00:06:35.990 --> 00:06:36.000 align:start position:0% it does right because it because even if 00:06:36.000 --> 00:06:39.410 align:start position:0% it does right because it because even if it<00:06:36.120> changes<00:06:36.420> souls<00:06:36.900> and<00:06:37.140> sent<00:06:37.800> you<00:06:37.980> but<00:06:38.970> this 00:06:39.410 --> 00:06:39.420 align:start position:0% it changes souls and sent you but this 00:06:39.420 --> 00:06:41.510 align:start position:0% it changes souls and sent you but this also<00:06:39.630> holds<00:06:39.870> its<00:06:40.140> lesser<00:06:40.500> equal<00:06:40.710> 7<00:06:41.040> you<00:06:41.400> can 00:06:41.510 --> 00:06:41.520 align:start position:0% also holds its lesser equal 7 you can 00:06:41.520 --> 00:06:46.040 align:start position:0% also holds its lesser equal 7 you can change<00:06:41.790> it<00:06:41.970> to<00:06:42.120> 1<00:06:42.300> its<00:06:42.480> soul<00:06:42.660> volt<00:06:44.840> what<00:06:45.840> about 00:06:46.040 --> 00:06:46.050 align:start position:0% change it to 1 its soul volt what about 00:06:46.050 --> 00:06:49.520 align:start position:0% change it to 1 its soul volt what about G<00:06:46.290> this<00:06:46.590> is<00:06:47.310> variants<00:06:47.610> to<00:06:47.700> volts<00:06:48.060> right<00:06:48.630> so 00:06:49.520 --> 00:06:49.530 align:start position:0% G this is variants to volts right so 00:06:49.530 --> 00:06:51.590 align:start position:0% G this is variants to volts right so even<00:06:49.710> if<00:06:49.890> it<00:06:49.980> was<00:06:50.250> one<00:06:50.490> which<00:06:50.910> would<00:06:51.150> fit<00:06:51.480> the 00:06:51.590 --> 00:06:51.600 align:start position:0% even if it was one which would fit the 00:06:51.600 --> 00:06:54.950 align:start position:0% even if it was one which would fit the grand<00:06:52.020> for<00:06:52.500> changes<00:06:52.740> to<00:06:52.770> zero<00:06:53.040> volt<00:06:53.490> and<00:06:54.090> it's 00:06:54.950 --> 00:06:54.960 align:start position:0% grand for changes to zero volt and it's 00:06:54.960 --> 00:06:57.350 align:start position:0% grand for changes to zero volt and it's a<00:06:55.080> sin<00:06:55.260> year<00:06:55.440> for<00:06:55.590> so<00:06:55.970> he<00:06:56.970> use<00:06:57.120> it<00:06:57.270> as 00:06:57.350 --> 00:06:57.360 align:start position:0% a sin year for so he use it as 00:06:57.360 --> 00:06:59.300 align:start position:0% a sin year for so he use it as precondition<00:06:58.110> given<00:06:58.800> efficiently<00:06:58.980> to 00:06:59.300 --> 00:06:59.310 align:start position:0% precondition given efficiently to 00:06:59.310 --> 00:07:03.290 align:start position:0% precondition given efficiently to syllables<00:07:00.560> but<00:07:01.560> now<00:07:01.710> he<00:07:01.770> is<00:07:01.920> attached<00:07:02.280> so<00:07:02.700> he 00:07:03.290 --> 00:07:03.300 align:start position:0% syllables but now he is attached so he 00:07:03.300 --> 00:07:05.570 align:start position:0% syllables but now he is attached so he here<00:07:03.750> for<00:07:03.780> X<00:07:04.140> less<00:07:04.350> or<00:07:04.500> equal<00:07:04.560> to<00:07:04.860> for<00:07:05.430> the 00:07:05.570 --> 00:07:05.580 align:start position:0% here for X less or equal to for the 00:07:05.580 --> 00:07:08.560 align:start position:0% here for X less or equal to for the artificial<00:07:05.970> just<00:07:06.960> a<00:07:07.080> something<00:07:07.290> that<00:07:07.500> I<00:07:07.530> added 00:07:08.560 --> 00:07:08.570 align:start position:0% artificial just a something that I added 00:07:08.570 --> 00:07:11.690 align:start position:0% artificial just a something that I added if<00:07:09.570> we<00:07:10.170> have<00:07:10.260> to<00:07:10.410> give<00:07:10.590> this<00:07:10.830> function<00:07:11.310> in<00:07:11.490> this 00:07:11.690 --> 00:07:11.700 align:start position:0% if we have to give this function in this 00:07:11.700 --> 00:07:14.390 align:start position:0% if we have to give this function in this with<00:07:12.540> this<00:07:12.690> event<00:07:13.050> is<00:07:13.320> it<00:07:13.530> is<00:07:13.890> it<00:07:14.040> still<00:07:14.220> true 00:07:14.390 --> 00:07:14.400 align:start position:0% with this event is it is it still true 00:07:14.400 --> 00:07:18.140 align:start position:0% with this event is it is it still true afterwards<00:07:15.350> it<00:07:16.350> is<00:07:16.560> right<00:07:16.800> so<00:07:17.610> here<00:07:17.940> you<00:07:18.000> can 00:07:18.140 --> 00:07:18.150 align:start position:0% afterwards it is right so here you can 00:07:18.150 --> 00:07:20.660 align:start position:0% afterwards it is right so here you can see<00:07:18.360> that<00:07:18.570> ax<00:07:18.780> less<00:07:19.110> or<00:07:19.230> equal<00:07:19.320> to<00:07:19.620> where<00:07:20.550> the 00:07:20.660 --> 00:07:20.670 align:start position:0% see that ax less or equal to where the 00:07:20.670 --> 00:07:22.370 align:start position:0% see that ax less or equal to where the makes<00:07:20.880> this<00:07:21.000> function<00:07:21.210> useless<00:07:21.690> because<00:07:22.050> it's 00:07:22.370 --> 00:07:22.380 align:start position:0% makes this function useless because it's 00:07:22.380 --> 00:07:25.220 align:start position:0% makes this function useless because it's not<00:07:22.500> really<00:07:22.770> going<00:07:22.890> to<00:07:23.040> change<00:07:23.630> but<00:07:24.630> with<00:07:24.990> this 00:07:25.220 --> 00:07:25.230 align:start position:0% not really going to change but with this 00:07:25.230 --> 00:07:26.960 align:start position:0% not really going to change but with this invariant<00:07:25.770> we<00:07:25.980> see<00:07:26.160> that<00:07:26.250> the<00:07:26.370> event<00:07:26.430> is<00:07:26.760> not 00:07:26.960 --> 00:07:26.970 align:start position:0% invariant we see that the event is not 00:07:26.970 --> 00:07:27.670 align:start position:0% invariant we see that the event is not cold 00:07:27.670 --> 00:07:27.680 align:start position:0% cold 00:07:27.680 --> 00:07:30.310 align:start position:0% cold after<00:07:28.680> the<00:07:28.890> function<00:07:29.130> is<00:07:29.310> locally<00:07:29.520> exact<00:07:29.970> it 00:07:30.310 --> 00:07:30.320 align:start position:0% after the function is locally exact it 00:07:30.320 --> 00:07:31.660 align:start position:0% after the function is locally exact it when<00:07:30.440> using<00:07:30.650> Varian<00:07:31.070> itself<00:07:31.460> as<00:07:31.640> a 00:07:31.660 --> 00:07:31.670 align:start position:0% when using Varian itself as a 00:07:31.670 --> 00:07:34.870 align:start position:0% when using Varian itself as a precondition<00:07:32.560> so<00:07:33.560> this<00:07:33.890> what<00:07:34.220> this<00:07:34.340> tells<00:07:34.700> us 00:07:34.870 --> 00:07:34.880 align:start position:0% precondition so this what this tells us 00:07:34.880 --> 00:07:37.930 align:start position:0% precondition so this what this tells us is<00:07:35.210> basically<00:07:35.870> that<00:07:36.520> access<00:07:37.520> for<00:07:37.550> go-to<00:07:37.880> is 00:07:37.930 --> 00:07:37.940 align:start position:0% is basically that access for go-to is 00:07:37.940 --> 00:07:38.710 align:start position:0% is basically that access for go-to is inductive 00:07:38.710 --> 00:07:38.720 align:start position:0% inductive 00:07:38.720 --> 00:07:41.820 align:start position:0% inductive whereas<00:07:39.680> access<00:07:40.340> circle<00:07:40.640> seven<00:07:40.910> is<00:07:41.030> not<00:07:41.210> and 00:07:41.820 --> 00:07:41.830 align:start position:0% whereas access circle seven is not and 00:07:41.830 --> 00:07:44.080 align:start position:0% whereas access circle seven is not and what<00:07:42.830> that<00:07:42.950> means<00:07:43.130> in<00:07:43.340> a<00:07:43.370> higher<00:07:43.550> level<00:07:43.820> is 00:07:44.080 --> 00:07:44.090 align:start position:0% what that means in a higher level is 00:07:44.090 --> 00:07:46.660 align:start position:0% what that means in a higher level is that<00:07:44.270> is<00:07:44.690> attending<00:07:45.140> variant<00:07:45.530> and<00:07:45.800> conjoining 00:07:46.660 --> 00:07:46.670 align:start position:0% that is attending variant and conjoining 00:07:46.670 --> 00:07:48.160 align:start position:0% that is attending variant and conjoining with<00:07:46.850> the<00:07:46.970> local<00:07:47.330> behavior<00:07:47.480> of<00:07:47.900> a<00:07:47.990> function 00:07:48.160 --> 00:07:48.170 align:start position:0% with the local behavior of a function 00:07:48.170 --> 00:07:50.620 align:start position:0% with the local behavior of a function alone<00:07:48.530> without<00:07:48.980> caring<00:07:49.370> about<00:07:49.430> the<00:07:49.610> rest<00:07:49.910> the 00:07:50.620 --> 00:07:50.630 align:start position:0% alone without caring about the rest the 00:07:50.630 --> 00:07:53.680 align:start position:0% alone without caring about the rest the invariant<00:07:51.080> should<00:07:51.260> still<00:07:51.530> hold<00:07:52.030> after<00:07:53.030> that 00:07:53.680 --> 00:07:53.690 align:start position:0% invariant should still hold after that 00:07:53.690 --> 00:07:56.130 align:start position:0% invariant should still hold after that execution<00:07:54.320> this<00:07:55.190> is<00:07:55.370> what<00:07:55.520> differentiates 00:07:56.130 --> 00:07:56.140 align:start position:0% execution this is what differentiates 00:07:56.140 --> 00:07:58.390 align:start position:0% execution this is what differentiates inductively<00:07:57.140> varies<00:07:57.530> from<00:07:58.040> normal 00:07:58.390 --> 00:07:58.400 align:start position:0% inductively varies from normal 00:07:58.400 --> 00:08:00.730 align:start position:0% inductively varies from normal invariance<00:07:58.760> an<00:07:58.850> inductive<00:07:59.360> world<00:08:00.170> has<00:08:00.470> to<00:08:00.710> be 00:08:00.730 --> 00:08:00.740 align:start position:0% invariance an inductive world has to be 00:08:00.740 --> 00:08:03.130 align:start position:0% invariance an inductive world has to be true<00:08:01.100> after<00:08:01.490> the<00:08:01.550> execution<00:08:01.820> as<00:08:02.210> well<00:08:02.420> so<00:08:02.660> it 00:08:03.130 --> 00:08:03.140 align:start position:0% true after the execution as well so it 00:08:03.140 --> 00:08:06.220 align:start position:0% true after the execution as well so it implies<00:08:03.770> itself<00:08:04.760> with<00:08:05.630> limited<00:08:05.960> with<00:08:06.080> the 00:08:06.220 --> 00:08:06.230 align:start position:0% implies itself with limited with the 00:08:06.230 --> 00:08:10.750 align:start position:0% implies itself with limited with the variables<00:08:06.710> being<00:08:07.190> in<00:08:07.370> the<00:08:07.430> next<00:08:07.730> state<00:08:09.160> so<00:08:10.160> dr. 00:08:10.750 --> 00:08:10.760 align:start position:0% variables being in the next state so dr. 00:08:10.760 --> 00:08:16.050 align:start position:0% variables being in the next state so dr. variance<00:08:11.210> is 00:08:16.050 --> 00:08:16.060 align:start position:0% 00:08:16.060 --> 00:08:21.820 align:start position:0% [Music] 00:08:21.820 --> 00:08:21.830 align:start position:0% 00:08:21.830 --> 00:08:25.570 align:start position:0% maybe<00:08:22.129> seven<00:08:22.580> and<00:08:22.759> then<00:08:22.940> oh<00:08:23.530> but<00:08:24.530> the<00:08:25.099> contract 00:08:25.570 --> 00:08:25.580 align:start position:0% maybe seven and then oh but the contract 00:08:25.580 --> 00:08:28.559 align:start position:0% maybe seven and then oh but the contract said<00:08:26.300> out<00:08:26.389> of<00:08:26.419> anger<00:08:26.740> sorry 00:08:28.559 --> 00:08:28.569 align:start position:0% said out of anger sorry 00:08:28.569 --> 00:08:35.469 align:start position:0% said out of anger sorry yeah<00:08:29.569> this<00:08:29.720> is<00:08:29.840> the<00:08:29.930> contract<00:08:32.740> yeah<00:08:34.330> but<00:08:35.330> even 00:08:35.469 --> 00:08:35.479 align:start position:0% yeah this is the contract yeah but even 00:08:35.479 --> 00:08:36.790 align:start position:0% yeah this is the contract yeah but even if<00:08:35.659> it's<00:08:35.810> folded<00:08:36.080> you<00:08:36.169> couldn't<00:08:36.469> change<00:08:36.500> it 00:08:36.790 --> 00:08:36.800 align:start position:0% if it's folded you couldn't change it 00:08:36.800 --> 00:08:39.279 align:start position:0% if it's folded you couldn't change it right<00:08:37.029> if<00:08:38.029> the<00:08:38.209> very<00:08:38.419> particular<00:08:38.599> public<00:08:39.200> you 00:08:39.279 --> 00:08:39.289 align:start position:0% right if the very particular public you 00:08:39.289 --> 00:08:41.350 align:start position:0% right if the very particular public you got<00:08:39.440> it<00:08:39.529> you<00:08:39.649> got<00:08:39.680> a<00:08:39.829> bullet<00:08:40.310> gutter<00:08:40.519> but<00:08:41.240> it 00:08:41.350 --> 00:08:41.360 align:start position:0% got it you got a bullet gutter but it 00:08:41.360 --> 00:08:43.120 align:start position:0% got it you got a bullet gutter but it can't<00:08:41.539> change<00:08:41.779> it<00:08:41.899> by<00:08:42.050> together<00:08:42.409> you<00:08:42.919> wouldn't 00:08:43.120 --> 00:08:43.130 align:start position:0% can't change it by together you wouldn't 00:08:43.130 --> 00:08:45.550 align:start position:0% can't change it by together you wouldn't need<00:08:43.190> it<00:08:43.399> I<00:08:44.269> can<00:08:44.570> you<00:08:44.870> show<00:08:45.050> the<00:08:45.170> throat<00:08:45.380> of<00:08:45.529> the 00:08:45.550 --> 00:08:45.560 align:start position:0% need it I can you show the throat of the 00:08:45.560 --> 00:08:52.930 align:start position:0% need it I can you show the throat of the seven<00:08:50.050> so<00:08:51.050> how<00:08:51.380> so<00:08:52.010> here<00:08:52.279> you're<00:08:52.399> starting<00:08:52.730> in 00:08:52.930 --> 00:08:52.940 align:start position:0% seven so how so here you're starting in 00:08:52.940 --> 00:08:54.579 align:start position:0% seven so how so here you're starting in varying<00:08:53.329> X<00:08:53.480> is<00:08:53.630> less<00:08:53.779> than<00:08:53.810> or<00:08:53.959> equal<00:08:54.019> so<00:08:54.350> but 00:08:54.579 --> 00:08:54.589 align:start position:0% varying X is less than or equal so but 00:08:54.589 --> 00:08:57.579 align:start position:0% varying X is less than or equal so but how<00:08:54.709> does<00:08:54.769> it<00:08:54.950> earn<00:08:55.329> to<00:08:56.329> the<00:08:56.899> actual<00:08:57.170> doctor 00:08:57.579 --> 00:08:57.589 align:start position:0% how does it earn to the actual doctor 00:08:57.589 --> 00:08:59.110 align:start position:0% how does it earn to the actual doctor here<00:08:57.860> because<00:08:58.160> these<00:08:58.430> are<00:08:58.730> the<00:08:58.880> only<00:08:59.000> ones 00:08:59.110 --> 00:08:59.120 align:start position:0% here because these are the only ones 00:08:59.120 --> 00:09:01.509 align:start position:0% here because these are the only ones that<00:08:59.329> that<00:08:59.510> hold<00:08:59.750> but<00:09:00.230> that<00:09:00.649> that<00:09:00.800> it<00:09:01.250> wouldn't 00:09:01.509 --> 00:09:01.519 align:start position:0% that that hold but that that it wouldn't 00:09:01.519 --> 00:09:03.310 align:start position:0% that that hold but that that it wouldn't matter<00:09:01.670> but<00:09:02.029> I<00:09:02.089> just<00:09:02.269> don't<00:09:02.420> see<00:09:02.540> to<00:09:02.870> anywhere 00:09:03.310 --> 00:09:03.320 align:start position:0% matter but I just don't see to anywhere 00:09:03.320 --> 00:09:05.769 align:start position:0% matter but I just don't see to anywhere in<00:09:03.380> the<00:09:03.529> coders<00:09:03.980> or<00:09:04.190> as<00:09:04.310> a<00:09:04.339> combo<00:09:05.300> with<00:09:05.329> the<00:09:05.570> one 00:09:05.769 --> 00:09:05.779 align:start position:0% in the coders or as a combo with the one 00:09:05.779 --> 00:09:07.690 align:start position:0% in the coders or as a combo with the one here<00:09:06.050> it's<00:09:06.649> led<00:09:06.860> them<00:09:07.010> to<00:09:07.100> because<00:09:07.610> of 00:09:07.690 --> 00:09:07.700 align:start position:0% here it's led them to because of 00:09:07.700 --> 00:09:11.620 align:start position:0% here it's led them to because of integers<00:09:09.370> it's<00:09:10.370> less<00:09:10.579> or<00:09:10.730> equal<00:09:10.820> 1<00:09:11.089> or<00:09:11.390> less 00:09:11.620 --> 00:09:11.630 align:start position:0% integers it's less or equal 1 or less 00:09:11.630 --> 00:09:14.500 align:start position:0% integers it's less or equal 1 or less than<00:09:11.660> two<00:09:11.959> okay<00:09:12.380> I<00:09:13.089> guess<00:09:14.089> I'm<00:09:14.209> just<00:09:14.300> kind<00:09:14.420> of 00:09:14.500 --> 00:09:14.510 align:start position:0% than two okay I guess I'm just kind of 00:09:14.510 --> 00:09:16.389 align:start position:0% than two okay I guess I'm just kind of essentially<00:09:14.930> interesting<00:09:15.589> it<00:09:15.769> picks<00:09:16.279> up 00:09:16.389 --> 00:09:16.399 align:start position:0% essentially interesting it picks up 00:09:16.399 --> 00:09:18.069 align:start position:0% essentially interesting it picks up person<00:09:16.700> just<00:09:16.790> picking<00:09:17.089> a<00:09:17.149> model<00:09:17.450> or<00:09:17.690> house<00:09:17.839> it 00:09:18.069 --> 00:09:18.079 align:start position:0% person just picking a model or house it 00:09:18.079 --> 00:09:20.680 align:start position:0% person just picking a model or house it is<00:09:18.890> XIII<00:09:19.550> just<00:09:19.730> picking<00:09:20.000> a<00:09:20.029> model<00:09:20.329> that<00:09:20.360> says 00:09:20.680 --> 00:09:20.690 align:start position:0% is XIII just picking a model that says 00:09:20.690 --> 00:09:22.090 align:start position:0% is XIII just picking a model that says two<00:09:20.899> is<00:09:21.050> the<00:09:21.140> smallest<00:09:21.380> number<00:09:21.589> I<00:09:21.740> can<00:09:21.800> find 00:09:22.090 --> 00:09:22.100 align:start position:0% two is the smallest number I can find 00:09:22.100 --> 00:09:24.040 align:start position:0% two is the smallest number I can find that<00:09:22.279> it's<00:09:22.430> true<00:09:22.640> for<00:09:22.670> doesn't<00:09:23.570> come<00:09:23.660> over<00:09:23.839> to 00:09:24.040 --> 00:09:24.050 align:start position:0% that it's true for doesn't come over to 00:09:24.050 --> 00:09:26.079 align:start position:0% that it's true for doesn't come over to cuz<00:09:24.860> we<00:09:24.980> guess<00:09:25.130> that's<00:09:25.339> that<00:09:25.550> because<00:09:25.790> nothing 00:09:26.079 --> 00:09:26.089 align:start position:0% cuz we guess that's that because nothing 00:09:26.089 --> 00:09:29.470 align:start position:0% cuz we guess that's that because nothing ducting<00:09:26.390> link<00:09:26.680> there's<00:09:27.680> an<00:09:27.829> uninfected<00:09:28.480> but 00:09:29.470 --> 00:09:29.480 align:start position:0% ducting link there's an uninfected but 00:09:29.480 --> 00:09:31.090 align:start position:0% ducting link there's an uninfected but every<00:09:29.690> big<00:09:29.930> grid<00:09:30.140> in<00:09:30.350> tubes<00:09:30.620> looking<00:09:30.950> to<00:09:31.010> be 00:09:31.090 --> 00:09:31.100 align:start position:0% every big grid in tubes looking to be 00:09:31.100 --> 00:09:33.190 align:start position:0% every big grid in tubes looking to be inducted<00:09:31.310> I<00:09:32.120> think<00:09:32.600> he's<00:09:32.779> asking<00:09:32.899> the 00:09:33.190 --> 00:09:33.200 align:start position:0% inducted I think he's asking the 00:09:33.200 --> 00:09:34.240 align:start position:0% inducted I think he's asking the lower-level<00:09:33.560> question<00:09:34.010> which<00:09:34.130> is 00:09:34.240 --> 00:09:34.250 align:start position:0% lower-level question which is 00:09:34.250 --> 00:09:37.110 align:start position:0% lower-level question which is algorithmically<00:09:34.820> how<00:09:35.089> do<00:09:35.149> I<00:09:35.209> write<00:09:35.510> a<00:09:35.570> solver 00:09:37.110 --> 00:09:37.120 align:start position:0% algorithmically how do I write a solver 00:09:37.120 --> 00:09:39.699 align:start position:0% algorithmically how do I write a solver from<00:09:38.120> this<00:09:38.300> does<00:09:39.079> not<00:09:39.230> the<00:09:39.410> reason<00:09:39.680> the 00:09:39.699 --> 00:09:39.709 align:start position:0% from this does not the reason the 00:09:39.709 --> 00:09:41.769 align:start position:0% from this does not the reason the character<00:09:40.190> to<00:09:40.399> yeah<00:09:40.880> yeah<00:09:41.420> but<00:09:41.570> the<00:09:41.660> reason 00:09:41.769 --> 00:09:41.779 align:start position:0% character to yeah yeah but the reason 00:09:41.779 --> 00:09:43.000 align:start position:0% character to yeah yeah but the reason for<00:09:41.930> that<00:09:42.079> is<00:09:42.320> that<00:09:42.470> it<00:09:42.680> looks<00:09:42.860> great 00:09:43.000 --> 00:09:43.010 align:start position:0% for that is that it looks great 00:09:43.010 --> 00:09:44.590 align:start position:0% for that is that it looks great inductive<00:09:43.399> and<00:09:43.550> grants<00:09:43.790> both<00:09:44.180> three<00:09:44.420> would<00:09:44.570> be 00:09:44.590 --> 00:09:44.600 align:start position:0% inductive and grants both three would be 00:09:44.600 --> 00:09:46.510 align:start position:0% inductive and grants both three would be an<00:09:44.750> article<00:09:44.959> to<00:09:45.200> great<00:09:45.470> like<00:09:45.680> if<00:09:45.950> you're<00:09:46.130> say<00:09:46.339> X 00:09:46.510 --> 00:09:46.520 align:start position:0% an article to great like if you're say X 00:09:46.520 --> 00:09:48.160 align:start position:0% an article to great like if you're say X less<00:09:46.700> than<00:09:46.820> B<00:09:47.060> would<00:09:47.300> be<00:09:47.329> inducted<00:09:47.750> yeah<00:09:47.930> yeah 00:09:48.160 --> 00:09:48.170 align:start position:0% less than B would be inducted yeah yeah 00:09:48.170 --> 00:09:52.750 align:start position:0% less than B would be inducted yeah yeah so<00:09:48.440> why<00:09:48.560> isn't<00:09:48.740> it<00:09:51.279> they're<00:09:52.279> only<00:09:52.399> right<00:09:52.610> it's 00:09:52.750 --> 00:09:52.760 align:start position:0% so why isn't it they're only right it's 00:09:52.760 --> 00:09:54.100 align:start position:0% so why isn't it they're only right it's fairly<00:09:52.940> prevalence<00:09:53.390> for<00:09:53.480> the<00:09:53.570> strongest<00:09:53.870> one 00:09:54.100 --> 00:09:54.110 align:start position:0% fairly prevalence for the strongest one 00:09:54.110 --> 00:09:56.260 align:start position:0% fairly prevalence for the strongest one all<00:09:54.380> right<00:09:54.589> yeah<00:09:55.430> because<00:09:55.700> three<00:09:55.970> would<00:09:56.120> be 00:09:56.260 --> 00:09:56.270 align:start position:0% all right yeah because three would be 00:09:56.270 --> 00:09:58.870 align:start position:0% all right yeah because three would be weaker<00:09:56.540> than<00:09:56.570> two<00:09:56.930> yeah<00:09:57.440> in<00:09:58.160> the<00:09:58.250> sense<00:09:58.459> that<00:09:58.550> X 00:09:58.870 --> 00:09:58.880 align:start position:0% weaker than two yeah in the sense that X 00:09:58.880 --> 00:10:00.910 align:start position:0% weaker than two yeah in the sense that X plus<00:09:59.209> rho2<00:09:59.480> would<00:09:59.779> you<00:09:59.839> play<00:10:00.050> but<00:10:00.350> there's<00:10:00.770> no 00:10:00.910 --> 00:10:00.920 align:start position:0% plus rho2 would you play but there's no 00:10:00.920 --> 00:10:02.090 align:start position:0% plus rho2 would you play but there's no longer<00:10:01.130> than<00:10:01.370> you<00:10:01.520> bro 00:10:02.090 --> 00:10:02.100 align:start position:0% longer than you bro 00:10:02.100 --> 00:10:04.310 align:start position:0% longer than you bro oh<00:10:02.130> no<00:10:02.910> I<00:10:02.940> didn't<00:10:03.270> write<00:10:03.390> down<00:10:03.420> that<00:10:04.050> comes 00:10:04.310 --> 00:10:04.320 align:start position:0% oh no I didn't write down that comes 00:10:04.320 --> 00:10:12.170 align:start position:0% oh no I didn't write down that comes from<00:10:04.560> from<00:10:04.980> from<00:10:05.190> semester<00:10:11.030> the<00:10:12.030> other 00:10:12.170 --> 00:10:12.180 align:start position:0% from from from semester the other 00:10:12.180 --> 00:10:15.290 align:start position:0% from from from semester the other questions<00:10:12.540> here<00:10:14.120> okay 00:10:15.290 --> 00:10:15.300 align:start position:0% questions here okay 00:10:15.300 --> 00:10:18.140 align:start position:0% questions here okay so<00:10:15.840> loop<00:10:16.260> invariants<00:10:16.980> that's<00:10:17.910> right 00:10:18.140 --> 00:10:18.150 align:start position:0% so loop invariants that's right 00:10:18.150 --> 00:10:21.440 align:start position:0% so loop invariants that's right inductive<00:10:18.660> invariants<00:10:20.030> they're<00:10:21.030> used<00:10:21.300> to 00:10:21.440 --> 00:10:21.450 align:start position:0% inductive invariants they're used to 00:10:21.450 --> 00:10:23.090 align:start position:0% inductive invariants they're used to summarize<00:10:21.930> the<00:10:22.230> relevant<00:10:22.590> piece<00:10:22.740> of<00:10:22.860> code 00:10:23.090 --> 00:10:23.100 align:start position:0% summarize the relevant piece of code 00:10:23.100 --> 00:10:24.500 align:start position:0% summarize the relevant piece of code without<00:10:23.280> really<00:10:23.550> caring<00:10:23.760> about<00:10:24.000> the<00:10:24.240> rest<00:10:24.420> of 00:10:24.500 --> 00:10:24.510 align:start position:0% without really caring about the rest of 00:10:24.510 --> 00:10:25.100 align:start position:0% without really caring about the rest of the<00:10:24.630> code 00:10:25.100 --> 00:10:25.110 align:start position:0% the code 00:10:25.110 --> 00:10:27.290 align:start position:0% the code sorry<00:10:25.440> you're<00:10:25.740> interested<00:10:26.280> in<00:10:26.790> a<00:10:26.910> single 00:10:27.290 --> 00:10:27.300 align:start position:0% sorry you're interested in a single 00:10:27.300 --> 00:10:29.060 align:start position:0% sorry you're interested in a single piece<00:10:27.600> of<00:10:27.780> code<00:10:27.960> you<00:10:28.140> want<00:10:28.320> some<00:10:28.530> right<00:10:28.710> step 00:10:29.060 --> 00:10:29.070 align:start position:0% piece of code you want some right step 00:10:29.070 --> 00:10:31.550 align:start position:0% piece of code you want some right step and<00:10:29.400> you<00:10:30.120> might<00:10:30.420> even<00:10:30.750> you<00:10:31.050> might<00:10:31.290> have 00:10:31.550 --> 00:10:31.560 align:start position:0% and you might even you might have 00:10:31.560 --> 00:10:33.050 align:start position:0% and you might even you might have information<00:10:32.250> or<00:10:32.430> it<00:10:32.550> might<00:10:32.700> not<00:10:32.730> have 00:10:33.050 --> 00:10:33.060 align:start position:0% information or it might not have 00:10:33.060 --> 00:10:34.280 align:start position:0% information or it might not have information<00:10:33.540> with<00:10:33.660> the<00:10:33.750> rest<00:10:33.930> of<00:10:34.020> the<00:10:34.080> program 00:10:34.280 --> 00:10:34.290 align:start position:0% information with the rest of the program 00:10:34.290 --> 00:10:35.930 align:start position:0% information with the rest of the program right<00:10:35.070> so<00:10:35.250> you<00:10:35.310> want<00:10:35.490> some<00:10:35.670> rights<00:10:35.850> that 00:10:35.930 --> 00:10:35.940 align:start position:0% right so you want some rights that 00:10:35.940 --> 00:10:39.170 align:start position:0% right so you want some rights that little<00:10:36.420> bit<00:10:37.070> and<00:10:38.070> this<00:10:38.220> is<00:10:38.370> particularly<00:10:38.760> and 00:10:39.170 --> 00:10:39.180 align:start position:0% little bit and this is particularly and 00:10:39.180 --> 00:10:41.540 align:start position:0% little bit and this is particularly and actually<00:10:39.480> classically<00:10:39.960> useful<00:10:40.530> for<00:10:41.100> loops 00:10:41.540 --> 00:10:41.550 align:start position:0% actually classically useful for loops 00:10:41.550 --> 00:10:45.110 align:start position:0% actually classically useful for loops right<00:10:42.270> because<00:10:42.660> loops<00:10:43.170> are<00:10:43.860> the<00:10:44.250> core<00:10:44.490> of<00:10:44.790> the 00:10:45.110 --> 00:10:45.120 align:start position:0% right because loops are the core of the 00:10:45.120 --> 00:10:46.790 align:start position:0% right because loops are the core of the challenges<00:10:45.600> in<00:10:45.720> fortification<00:10:46.410> right<00:10:46.590> that's 00:10:46.790 --> 00:10:46.800 align:start position:0% challenges in fortification right that's 00:10:46.800 --> 00:10:48.800 align:start position:0% challenges in fortification right that's the<00:10:47.040> determination<00:10:47.880> for<00:10:48.060> that's<00:10:48.480> what<00:10:48.690> you 00:10:48.800 --> 00:10:48.810 align:start position:0% the determination for that's what you 00:10:48.810 --> 00:10:51.560 align:start position:0% the determination for that's what you don't<00:10:49.050> really<00:10:49.140> know<00:10:49.320> how<00:10:49.980> have<00:10:50.970> a<00:10:51.000> sold<00:10:51.330> a<00:10:51.390> nice 00:10:51.560 --> 00:10:51.570 align:start position:0% don't really know how have a sold a nice 00:10:51.570 --> 00:10:54.860 align:start position:0% don't really know how have a sold a nice way<00:10:51.840> so<00:10:52.470> which<00:10:52.740> right<00:10:52.950> is<00:10:53.210> not<00:10:54.210> we<00:10:54.420> like<00:10:54.660> just 00:10:54.860 --> 00:10:54.870 align:start position:0% way so which right is not we like just 00:10:54.870 --> 00:10:56.510 align:start position:0% way so which right is not we like just people<00:10:55.020> in<00:10:55.260> general<00:10:55.350> have<00:10:56.160> tried<00:10:56.430> to 00:10:56.510 --> 00:10:56.520 align:start position:0% people in general have tried to 00:10:56.520 --> 00:10:59.900 align:start position:0% people in general have tried to summarize<00:10:56.730> loops<00:10:57.500> in<00:10:58.500> a<00:10:58.650> way<00:10:58.860> that<00:10:59.670> it<00:10:59.790> can 00:10:59.900 --> 00:10:59.910 align:start position:0% summarize loops in a way that it can 00:10:59.910 --> 00:11:01.970 align:start position:0% summarize loops in a way that it can still<00:11:00.060> go<00:11:00.240> on<00:11:00.420> and<00:11:00.900> improve<00:11:01.350> your<00:11:01.620> your 00:11:01.970 --> 00:11:01.980 align:start position:0% still go on and improve your your 00:11:01.980 --> 00:11:05.810 align:start position:0% still go on and improve your your program<00:11:03.650> so<00:11:04.650> now<00:11:05.130> I'm<00:11:05.220> going<00:11:05.370> to<00:11:05.460> show<00:11:05.790> a 00:11:05.810 --> 00:11:05.820 align:start position:0% program so now I'm going to show a 00:11:05.820 --> 00:11:08.990 align:start position:0% program so now I'm going to show a little<00:11:06.120> loop<00:11:06.420> example<00:11:07.010> is<00:11:08.010> this<00:11:08.340> assertion 00:11:08.990 --> 00:11:09.000 align:start position:0% little loop example is this assertion 00:11:09.000 --> 00:11:15.760 align:start position:0% little loop example is this assertion correct 00:11:15.760 --> 00:11:15.770 align:start position:0% 00:11:15.770 --> 00:11:21.460 align:start position:0% it<00:11:16.250> is<00:11:16.430> like<00:11:19.000> yes<00:11:20.000> so<00:11:20.240> they're<00:11:20.450> assigning<00:11:21.380> an 00:11:21.460 --> 00:11:21.470 align:start position:0% it is like yes so they're assigning an 00:11:21.470 --> 00:11:24.400 align:start position:0% it is like yes so they're assigning an address<00:11:21.740> at<00:11:21.980> least<00:11:22.490> the<00:11:23.060> misspelling<00:11:23.690> 0<00:11:23.990> so 00:11:24.400 --> 00:11:24.410 align:start position:0% address at least the misspelling 0 so 00:11:24.410 --> 00:11:28.020 align:start position:0% address at least the misspelling 0 so that's<00:11:24.680> safe<00:11:25.210> but<00:11:26.210> I'm<00:11:26.300> gonna<00:11:26.480> run<00:11:27.020> continuing 00:11:28.020 --> 00:11:28.030 align:start position:0% that's safe but I'm gonna run continuing 00:11:28.030 --> 00:11:31.660 align:start position:0% that's safe but I'm gonna run continuing and<00:11:29.030> it<00:11:29.120> tells<00:11:29.300> it<00:11:29.480> it's<00:11:29.600> safe<00:11:29.780> and<00:11:30.340> also<00:11:31.340> much 00:11:31.660 --> 00:11:31.670 align:start position:0% and it tells it it's safe and also much 00:11:31.670 --> 00:11:37.870 align:start position:0% and it tells it it's safe and also much more<00:11:31.910> stuff<00:11:32.120> and<00:11:33.130> but<00:11:34.130> if<00:11:34.220> we<00:11:34.400> look<00:11:34.580> for<00:11:36.880> the 00:11:37.870 --> 00:11:37.880 align:start position:0% more stuff and but if we look for the 00:11:37.880 --> 00:11:39.640 align:start position:0% more stuff and but if we look for the information<00:11:38.090> that<00:11:38.390> it<00:11:38.660> gives<00:11:38.870> us<00:11:39.080> about<00:11:39.380> loop 00:11:39.640 --> 00:11:39.650 align:start position:0% information that it gives us about loop 00:11:39.650 --> 00:11:43.390 align:start position:0% information that it gives us about loop pattern<00:11:39.910> receive<00:11:40.910> this<00:11:41.920> this<00:11:42.920> is<00:11:43.070> an 00:11:43.390 --> 00:11:43.400 align:start position:0% pattern receive this this is an 00:11:43.400 --> 00:11:45.880 align:start position:0% pattern receive this this is an invariant<00:11:43.970> under<00:11:44.120> loop<00:11:44.360> pattern<00:11:44.540> and<00:11:44.840> isn't<00:11:45.800> a 00:11:45.880 --> 00:11:45.890 align:start position:0% invariant under loop pattern and isn't a 00:11:45.890 --> 00:11:47.440 align:start position:0% invariant under loop pattern and isn't a neglected<00:11:46.250> conducted<00:11:46.730> invariant<00:11:47.120> for<00:11:47.360> the 00:11:47.440 --> 00:11:47.450 align:start position:0% neglected conducted invariant for the 00:11:47.450 --> 00:11:50.230 align:start position:0% neglected conducted invariant for the loop<00:11:47.630> and<00:11:47.900> decides<00:11:48.650> that<00:11:48.950> that<00:11:49.580> is<00:11:49.700> actually<00:11:50.060> y 00:11:50.230 --> 00:11:50.240 align:start position:0% loop and decides that that is actually y 00:11:50.240 --> 00:11:52.810 align:start position:0% loop and decides that that is actually y is<00:11:50.300> X<00:11:50.840> this<00:11:51.560> is<00:11:51.620> telling<00:11:51.950> me<00:11:52.040> why<00:11:52.310> less<00:11:52.640> for 00:11:52.810 --> 00:11:52.820 align:start position:0% is X this is telling me why less for 00:11:52.820 --> 00:11:59.170 align:start position:0% is X this is telling me why less for equal<00:11:53.150> s<00:11:55.330> and<00:11:56.890> here<00:11:57.890> was<00:11:58.100> the<00:11:58.220> condition<00:11:58.610> is<00:11:58.940> y 00:11:59.170 --> 00:11:59.180 align:start position:0% equal s and here was the condition is y 00:11:59.180 --> 00:12:01.510 align:start position:0% equal s and here was the condition is y as<00:11:59.480> an<00:11:59.660> axe<00:11:59.870> so<00:12:00.230> the<00:12:00.770> difference<00:12:01.160> between<00:12:01.190> this 00:12:01.510 --> 00:12:01.520 align:start position:0% as an axe so the difference between this 00:12:01.520 --> 00:12:03.550 align:start position:0% as an axe so the difference between this series<00:12:01.880> that<00:12:02.030> violets<00:12:02.420> article<00:12:02.690> ax<00:12:02.900> is<00:12:03.350> an 00:12:03.550 --> 00:12:03.560 align:start position:0% series that violets article ax is an 00:12:03.560 --> 00:12:05.830 align:start position:0% series that violets article ax is an inductive<00:12:03.950> you<00:12:04.070> very<00:12:04.280> popular<00:12:04.790> it<00:12:05.600> still 00:12:05.830 --> 00:12:05.840 align:start position:0% inductive you very popular it still 00:12:05.840 --> 00:12:09.520 align:start position:0% inductive you very popular it still holds<00:12:06.290> after<00:12:06.520> the<00:12:07.520> the<00:12:08.030> loop<00:12:08.210> is<00:12:08.420> executed<00:12:08.690> so 00:12:09.520 --> 00:12:09.530 align:start position:0% holds after the the loop is executed so 00:12:09.530 --> 00:12:11.380 align:start position:0% holds after the the loop is executed so why<00:12:09.740> that's<00:12:10.010> our<00:12:10.100> galactic<00:12:10.280> core<00:12:10.790> property<00:12:11.240> of 00:12:11.380 --> 00:12:11.390 align:start position:0% why that's our galactic core property of 00:12:11.390 --> 00:12:18.670 align:start position:0% why that's our galactic core property of this<00:12:12.350> of<00:12:12.710> this<00:12:13.160> loop<00:12:13.400> here<00:12:16.150> this<00:12:17.150> program<00:12:17.680> the 00:12:18.670 --> 00:12:18.680 align:start position:0% this of this loop here this program the 00:12:18.680 --> 00:12:20.290 align:start position:0% this of this loop here this program the condition<00:12:19.160> of<00:12:19.280> the<00:12:19.400> loop<00:12:19.550> has<00:12:19.790> to<00:12:19.940> be<00:12:20.030> false 00:12:20.290 --> 00:12:20.300 align:start position:0% condition of the loop has to be false 00:12:20.300 --> 00:12:23.190 align:start position:0% condition of the loop has to be false right<00:12:20.630> at<00:12:21.380> this<00:12:21.950> point<00:12:22.340> here<00:12:22.580> in<00:12:22.640> the<00:12:22.730> code 00:12:23.190 --> 00:12:23.200 align:start position:0% right at this point here in the code 00:12:23.200 --> 00:12:26.020 align:start position:0% right at this point here in the code this<00:12:24.200> has<00:12:24.410> to<00:12:24.530> be<00:12:24.620> false<00:12:24.860> otherwise<00:12:25.220> it<00:12:25.730> would 00:12:26.020 --> 00:12:26.030 align:start position:0% this has to be false otherwise it would 00:12:26.030 --> 00:12:28.960 align:start position:0% this has to be false otherwise it would still<00:12:26.240> be<00:12:26.270> in<00:12:26.480> the<00:12:26.770> correct<00:12:27.770> so<00:12:28.700> we<00:12:28.820> haven't 00:12:28.960 --> 00:12:28.970 align:start position:0% still be in the correct so we haven't 00:12:28.970 --> 00:12:31.990 align:start position:0% still be in the correct so we haven't this<00:12:29.240> is<00:12:29.510> also<00:12:29.750> true<00:12:29.990> at<00:12:30.650> that<00:12:30.890> point<00:12:31.160> y 00:12:31.990 --> 00:12:32.000 align:start position:0% this is also true at that point y 00:12:32.000 --> 00:12:34.480 align:start position:0% this is also true at that point y greater<00:12:32.630> article<00:12:33.110> ax<00:12:33.290> which<00:12:34.040> is<00:12:34.130> the<00:12:34.220> negation 00:12:34.480 --> 00:12:34.490 align:start position:0% greater article ax which is the negation 00:12:34.490 --> 00:12:38.170 align:start position:0% greater article ax which is the negation of<00:12:35.290> this<00:12:36.290> condition<00:12:36.710> here<00:12:36.920> so<00:12:37.760> you<00:12:37.820> can<00:12:38.030> have 00:12:38.170 --> 00:12:38.180 align:start position:0% of this condition here so you can have 00:12:38.180 --> 00:12:40.600 align:start position:0% of this condition here so you can have these<00:12:38.330> two<00:12:38.390> things<00:12:38.990> together<00:12:39.230> we<00:12:39.770> can<00:12:40.280> imply 00:12:40.600 --> 00:12:40.610 align:start position:0% these two things together we can imply 00:12:40.610 --> 00:12:44.860 align:start position:0% these two things together we can imply that<00:12:40.640> y<00:12:41.000> equals<00:12:41.360> x<00:12:42.010> right<00:12:43.010> so<00:12:43.330> deriving<00:12:44.330> and 00:12:44.860 --> 00:12:44.870 align:start position:0% that y equals x right so deriving and 00:12:44.870 --> 00:12:47.140 align:start position:0% that y equals x right so deriving and inductive<00:12:45.290> area<00:12:45.590> for<00:12:45.800> the<00:12:45.890> loop<00:12:46.070> right<00:12:46.880> away 00:12:47.140 --> 00:12:47.150 align:start position:0% inductive area for the loop right away 00:12:47.150 --> 00:12:49.890 align:start position:0% inductive area for the loop right away nabel's<00:12:47.630> us<00:12:47.810> to<00:12:47.990> prove<00:12:48.200> a<00:12:48.440> property<00:12:48.890> that 00:12:49.890 --> 00:12:49.900 align:start position:0% nabel's us to prove a property that 00:12:49.900 --> 00:12:52.720 align:start position:0% nabel's us to prove a property that happily<00:12:50.900> uses<00:12:51.260> the<00:12:51.410> computation<00:12:51.710> of<00:12:52.190> the<00:12:52.460> of 00:12:52.720 --> 00:12:52.730 align:start position:0% happily uses the computation of the of 00:12:52.730 --> 00:12:56.110 align:start position:0% happily uses the computation of the of the<00:12:52.850> loop<00:12:54.190> and<00:12:55.190> in<00:12:55.400> that<00:12:55.550> manner<00:12:55.730> it<00:12:55.910> sings 00:12:56.110 --> 00:12:56.120 align:start position:0% the loop and in that manner it sings 00:12:56.120 --> 00:12:57.730 align:start position:0% the loop and in that manner it sings induction<00:12:56.630> pairs<00:12:56.810> can<00:12:56.960> also<00:12:57.110> be<00:12:57.320> used<00:12:57.500> to 00:12:57.730 --> 00:12:57.740 align:start position:0% induction pairs can also be used to 00:12:57.740 --> 00:12:59.140 align:start position:0% induction pairs can also be used to prove<00:12:58.010> recursive<00:12:58.460> programs<00:12:58.790> where<00:12:59.000> you<00:12:59.030> can 00:12:59.140 --> 00:12:59.150 align:start position:0% prove recursive programs where you can 00:12:59.150 --> 00:13:02.170 align:start position:0% prove recursive programs where you can buy<00:12:59.570> two<00:12:59.870> identical<00:13:00.410> brain<00:13:00.620> as<00:13:00.950> the<00:13:01.820> inductive 00:13:02.170 --> 00:13:02.180 align:start position:0% buy two identical brain as the inductive 00:13:02.180 --> 00:13:05.680 align:start position:0% buy two identical brain as the inductive hypothesis<00:13:02.870> of<00:13:03.170> the<00:13:03.770> recursive<00:13:04.070> function<00:13:04.690> but 00:13:05.680 --> 00:13:05.690 align:start position:0% hypothesis of the recursive function but 00:13:05.690 --> 00:13:10.420 align:start position:0% hypothesis of the recursive function but then<00:13:05.870> how<00:13:06.580> exactly<00:13:07.630> does<00:13:08.740> hi<00:13:09.740> exactly<00:13:10.100> doing 00:13:10.420 --> 00:13:10.430 align:start position:0% then how exactly does hi exactly doing 00:13:10.430 --> 00:13:13.020 align:start position:0% then how exactly does hi exactly doing the<00:13:10.520> same<00:13:10.730> variance<00:13:11.440> help<00:13:12.440> us<00:13:12.710> prove 00:13:13.020 --> 00:13:13.030 align:start position:0% the same variance help us prove 00:13:13.030 --> 00:13:15.790 align:start position:0% the same variance help us prove contracts<00:13:14.030> help<00:13:14.840> us<00:13:14.990> prove<00:13:15.170> contract<00:13:15.740> in 00:13:15.790 --> 00:13:15.800 align:start position:0% contracts help us prove contract in 00:13:15.800 --> 00:13:17.920 align:start position:0% contracts help us prove contract in agreeance<00:13:16.070> invariants<00:13:16.700> that<00:13:16.850> hold<00:13:17.120> on<00:13:17.450> the 00:13:17.920 --> 00:13:17.930 align:start position:0% agreeance invariants that hold on the 00:13:17.930 --> 00:13:19.900 align:start position:0% agreeance invariants that hold on the contract<00:13:18.290> level<00:13:18.440> state<00:13:18.800> variables<00:13:19.340> so 00:13:19.900 --> 00:13:19.910 align:start position:0% contract level state variables so 00:13:19.910 --> 00:13:20.560 align:start position:0% contract level state variables so invariance 00:13:20.560 --> 00:13:20.570 align:start position:0% invariance 00:13:20.570 --> 00:13:23.020 align:start position:0% invariance true<00:13:20.870> before<00:13:21.710> and<00:13:21.950> after<00:13:22.400> the<00:13:22.520> execution<00:13:22.970> of 00:13:23.020 --> 00:13:23.030 align:start position:0% true before and after the execution of 00:13:23.030 --> 00:13:24.940 align:start position:0% true before and after the execution of any<00:13:23.240> public<00:13:23.600> function<00:13:23.960> and<00:13:24.230> here<00:13:24.590> when<00:13:24.830> it 00:13:24.940 --> 00:13:24.950 align:start position:0% any public function and here when it 00:13:24.950 --> 00:13:27.100 align:start position:0% any public function and here when it when<00:13:25.280> it<00:13:25.310> when<00:13:25.610> it's<00:13:25.760> 80<00:13:25.880> variants<00:13:26.360> actually 00:13:27.100 --> 00:13:27.110 align:start position:0% when it when it's 80 variants actually 00:13:27.110 --> 00:13:28.960 align:start position:0% when it when it's 80 variants actually been<00:13:27.200> contracting<00:13:27.740> variants<00:13:28.100> in<00:13:28.550> this<00:13:28.700> sense 00:13:28.960 --> 00:13:28.970 align:start position:0% been contracting variants in this sense 00:13:28.970 --> 00:13:30.820 align:start position:0% been contracting variants in this sense before<00:13:29.150> and<00:13:29.420> after<00:13:29.630> each<00:13:29.750> function<00:13:30.170> and<00:13:30.320> not 00:13:30.820 --> 00:13:30.830 align:start position:0% before and after each function and not 00:13:30.830 --> 00:13:33.550 align:start position:0% before and after each function and not the<00:13:31.220> classical<00:13:31.640> invariant<00:13:32.410> definition<00:13:33.410> that 00:13:33.550 --> 00:13:33.560 align:start position:0% the classical invariant definition that 00:13:33.560 --> 00:13:36.510 align:start position:0% the classical invariant definition that it<00:13:33.710> has<00:13:33.860> been<00:13:34.070> through<00:13:34.280> it<00:13:34.310> ever<00:13:34.580> encountered 00:13:36.510 --> 00:13:36.520 align:start position:0% it has been through it ever encountered 00:13:36.520 --> 00:13:38.680 align:start position:0% it has been through it ever encountered such<00:13:37.520> a<00:13:37.550> deficit<00:13:38.030> at<00:13:38.120> the<00:13:38.150> beginning<00:13:38.510> you<00:13:38.660> can 00:13:38.680 --> 00:13:38.690 align:start position:0% such a deficit at the beginning you can 00:13:38.690 --> 00:13:41.830 align:start position:0% such a deficit at the beginning you can model<00:13:39.110> to<00:13:39.200> the<00:13:39.350> contract<00:13:39.800> as<00:13:40.690> discomfort<00:13:41.690> flow 00:13:41.830 --> 00:13:41.840 align:start position:0% model to the contract as discomfort flow 00:13:41.840 --> 00:13:44.440 align:start position:0% model to the contract as discomfort flow here<00:13:42.050> containing<00:13:42.590> a<00:13:42.800> loop<00:13:42.980> right<00:13:43.550> where<00:13:44.240> you 00:13:44.440 --> 00:13:44.450 align:start position:0% here containing a loop right where you 00:13:44.450 --> 00:13:46.330 align:start position:0% here containing a loop right where you go<00:13:44.600> to<00:13:44.660> interface<00:13:45.200> a<00:13:45.470> physical<00:13:45.800> structure<00:13:45.980> and 00:13:46.330 --> 00:13:46.340 align:start position:0% go to interface a physical structure and 00:13:46.340 --> 00:13:48.580 align:start position:0% go to interface a physical structure and you<00:13:46.910> always<00:13:47.120> go<00:13:47.360> back<00:13:47.540> to<00:13:47.690> interface<00:13:48.080> after 00:13:48.580 --> 00:13:48.590 align:start position:0% you always go back to interface after 00:13:48.590 --> 00:13:51.390 align:start position:0% you always go back to interface after the<00:13:48.890> execution<00:13:49.400> of<00:13:49.430> a<00:13:49.550> public<00:13:49.850> function<00:13:50.030> and 00:13:51.390 --> 00:13:51.400 align:start position:0% the execution of a public function and 00:13:51.400 --> 00:13:56.730 align:start position:0% the execution of a public function and here<00:13:52.400> the<00:13:53.090> really<00:13:53.330> nice<00:13:53.450> thing<00:13:53.810> about<00:13:54.220> this 00:13:56.730 --> 00:13:56.740 align:start position:0% here the really nice thing about this 00:13:56.740 --> 00:13:59.860 align:start position:0% here the really nice thing about this this<00:13:57.740> way<00:13:58.520> of<00:13:58.670> modeling<00:13:59.000> it<00:13:59.270> of<00:13:59.480> the<00:13:59.630> with<00:13:59.750> this 00:13:59.860 --> 00:13:59.870 align:start position:0% this way of modeling it of the with this 00:13:59.870 --> 00:14:01.780 align:start position:0% this way of modeling it of the with this way<00:13:59.990> of<00:14:00.050> seeing<00:14:00.290> it<00:14:00.500> is<00:14:00.830> that<00:14:01.010> we<00:14:01.160> can<00:14:01.370> model 00:14:01.780 --> 00:14:01.790 align:start position:0% way of seeing it is that we can model 00:14:01.790 --> 00:14:05.260 align:start position:0% way of seeing it is that we can model each<00:14:02.300> of<00:14:02.750> these<00:14:02.990> transitions<00:14:03.770> from<00:14:04.700> these 00:14:05.260 --> 00:14:05.270 align:start position:0% each of these transitions from these 00:14:05.270 --> 00:14:10.480 align:start position:0% each of these transitions from these nodes<00:14:05.740> to<00:14:06.740> run<00:14:07.580> clauses<00:14:08.830> horn<00:14:09.830> clauses<00:14:10.040> are 00:14:10.480 --> 00:14:10.490 align:start position:0% nodes to run clauses horn clauses are 00:14:10.490 --> 00:14:13.120 align:start position:0% nodes to run clauses horn clauses are for<00:14:11.180> serologic<00:14:11.720> formulas<00:14:12.230> that<00:14:12.440> have<00:14:12.860> a<00:14:12.890> very 00:14:13.120 --> 00:14:13.130 align:start position:0% for serologic formulas that have a very 00:14:13.130 --> 00:14:15.460 align:start position:0% for serologic formulas that have a very particular<00:14:13.340> shape<00:14:13.910> this<00:14:14.840> one<00:14:15.140> it's<00:14:15.350> an 00:14:15.460 --> 00:14:15.470 align:start position:0% particular shape this one it's an 00:14:15.470 --> 00:14:19.450 align:start position:0% particular shape this one it's an application<00:14:15.940> where<00:14:17.200> the<00:14:18.200> hat<00:14:18.440> or<00:14:18.830> the<00:14:19.070> implied 00:14:19.450 --> 00:14:19.460 align:start position:0% application where the hat or the implied 00:14:19.460 --> 00:14:23.200 align:start position:0% application where the hat or the implied part<00:14:19.760> of<00:14:19.820> duplication<00:14:20.420> is<00:14:20.770> been<00:14:21.770> here<00:14:22.130> when<00:14:23.090> we 00:14:23.200 --> 00:14:23.210 align:start position:0% part of duplication is been here when we 00:14:23.210 --> 00:14:24.610 align:start position:0% part of duplication is been here when we the<00:14:23.330> predicate<00:14:23.780> of<00:14:24.050> the<00:14:24.200> block<00:14:24.410> we're<00:14:24.590> going 00:14:24.610 --> 00:14:24.620 align:start position:0% the predicate of the block we're going 00:14:24.620 --> 00:14:27.520 align:start position:0% the predicate of the block we're going to<00:14:25.040> where<00:14:25.640> the<00:14:25.760> parameters<00:14:26.300> are<00:14:26.480> here<00:14:26.960> are<00:14:27.380> the 00:14:27.520 --> 00:14:27.530 align:start position:0% to where the parameters are here are the 00:14:27.530 --> 00:14:30.160 align:start position:0% to where the parameters are here are the state<00:14:27.710> variables<00:14:27.740> right<00:14:28.490> so<00:14:28.730> here<00:14:28.970> X<00:14:29.300> is<00:14:29.750> going 00:14:30.160 --> 00:14:30.170 align:start position:0% state variables right so here X is going 00:14:30.170 --> 00:14:33.280 align:start position:0% state variables right so here X is going to<00:14:30.230> be<00:14:30.520> the<00:14:31.520> parameter<00:14:31.760> for<00:14:32.060> all<00:14:32.240> my<00:14:32.450> all<00:14:32.810> my<00:14:32.870> my 00:14:33.280 --> 00:14:33.290 align:start position:0% to be the parameter for all my all my my 00:14:33.290 --> 00:14:35.470 align:start position:0% to be the parameter for all my all my my predicate<00:14:33.710> here<00:14:33.980> and<00:14:34.310> the<00:14:34.580> predicate<00:14:34.850> is<00:14:35.420> true 00:14:35.470 --> 00:14:35.480 align:start position:0% predicate here and the predicate is true 00:14:35.480 --> 00:14:38.710 align:start position:0% predicate here and the predicate is true if<00:14:36.410> that<00:14:37.070> the<00:14:37.910> predicate<00:14:38.270> is<00:14:38.300> true<00:14:38.390> for<00:14:38.690> a 00:14:38.710 --> 00:14:38.720 align:start position:0% if that the predicate is true for a 00:14:38.720 --> 00:14:41.190 align:start position:0% if that the predicate is true for a certain<00:14:39.020> value<00:14:39.200> if<00:14:39.890> that<00:14:40.310> block<00:14:40.610> is<00:14:40.790> reachable 00:14:41.190 --> 00:14:41.200 align:start position:0% certain value if that block is reachable 00:14:41.200 --> 00:14:47.860 align:start position:0% certain value if that block is reachable for<00:14:42.200> that<00:14:42.880> relative<00:14:43.880> or<00:14:44.000> X<00:14:45.910> the<00:14:46.910> rest<00:14:47.150> of<00:14:47.480> the 00:14:47.860 --> 00:14:47.870 align:start position:0% for that relative or X the rest of the 00:14:47.870 --> 00:14:49.660 align:start position:0% for that relative or X the rest of the horn<00:14:48.290> Clause<00:14:48.530> here<00:14:48.800> on<00:14:49.010> the<00:14:49.130> left<00:14:49.310> side<00:14:49.550> of 00:14:49.660 --> 00:14:49.670 align:start position:0% horn Clause here on the left side of 00:14:49.670 --> 00:14:52.000 align:start position:0% horn Clause here on the left side of implication<00:14:50.150> we<00:14:50.240> have<00:14:50.420> constraints<00:14:51.110> and<00:14:51.290> here 00:14:52.000 --> 00:14:52.010 align:start position:0% implication we have constraints and here 00:14:52.010 --> 00:14:54.070 align:start position:0% implication we have constraints and here I<00:14:52.040> get<00:14:52.490> constraints<00:14:53.060> from<00:14:53.240> the<00:14:53.480> execution<00:14:53.990> of 00:14:54.070 --> 00:14:54.080 align:start position:0% I get constraints from the execution of 00:14:54.080 --> 00:14:56.890 align:start position:0% I get constraints from the execution of the<00:14:54.230> constructor<00:14:54.710> and<00:14:55.240> the<00:14:56.240> predicate<00:14:56.540> of<00:14:56.870> the 00:14:56.890 --> 00:14:56.900 align:start position:0% the constructor and the predicate of the 00:14:56.900 --> 00:14:59.680 align:start position:0% the constructor and the predicate of the block<00:14:57.200> I'm<00:14:57.380> coming<00:14:57.710> from<00:14:58.210> also<00:14:59.210> on<00:14:59.390> the<00:14:59.510> vary 00:14:59.680 --> 00:14:59.690 align:start position:0% block I'm coming from also on the vary 00:14:59.690 --> 00:15:03.900 align:start position:0% block I'm coming from also on the vary one<00:14:59.960> of<00:14:59.990> the<00:15:00.050> variables<00:15:00.140> that<00:15:02.290> the<00:15:03.290> value<00:15:03.590> that 00:15:03.900 --> 00:15:03.910 align:start position:0% one of the variables that the value that 00:15:03.910 --> 00:15:08.230 align:start position:0% one of the variables that the value that entered<00:15:04.910> that<00:15:05.360> block 00:15:08.230 --> 00:15:08.240 align:start position:0% 00:15:08.240 --> 00:15:11.360 align:start position:0% yes<00:15:09.240> so<00:15:09.480> if<00:15:09.810> there's<00:15:10.260> only<00:15:10.410> one<00:15:10.830> creditor<00:15:11.250> than 00:15:11.360 --> 00:15:11.370 align:start position:0% yes so if there's only one creditor than 00:15:11.370 --> 00:15:12.950 align:start position:0% yes so if there's only one creditor than the<00:15:11.430> left<00:15:11.610> side<00:15:11.820> is<00:15:11.970> called<00:15:12.180> linear<00:15:12.390> or<00:15:12.750> plus 00:15:12.950 --> 00:15:12.960 align:start position:0% the left side is called linear or plus 00:15:12.960 --> 00:15:16.040 align:start position:0% the left side is called linear or plus and<00:15:13.490> if<00:15:14.490> there<00:15:14.730> is<00:15:15.180> there's<00:15:15.360> more<00:15:15.600> than<00:15:15.660> one 00:15:16.040 --> 00:15:16.050 align:start position:0% and if there is there's more than one 00:15:16.050 --> 00:15:17.540 align:start position:0% and if there is there's more than one it's<00:15:16.380> silver<00:15:16.560> claws<00:15:16.950> but<00:15:17.160> it's<00:15:17.280> called<00:15:17.460> an 00:15:17.540 --> 00:15:17.550 align:start position:0% it's silver claws but it's called an 00:15:17.550 --> 00:15:18.860 align:start position:0% it's silver claws but it's called an almond<00:15:17.790> term<00:15:17.880> plus<00:15:18.210> and<00:15:18.570> it's<00:15:18.720> a<00:15:18.750> lot<00:15:18.840> harder 00:15:18.860 --> 00:15:18.870 align:start position:0% almond term plus and it's a lot harder 00:15:18.870 --> 00:15:23.180 align:start position:0% almond term plus and it's a lot harder to<00:15:19.140> soul<00:15:20.090> and<00:15:21.090> this<00:15:21.720> is<00:15:21.870> just<00:15:22.080> an<00:15:22.200> example<00:15:22.470> of<00:15:22.830> a 00:15:23.180 --> 00:15:23.190 align:start position:0% to soul and this is just an example of a 00:15:23.190 --> 00:15:25.940 align:start position:0% to soul and this is just an example of a bunch<00:15:23.790> of<00:15:23.850> wider<00:15:24.060> rules<00:15:24.300> and<00:15:25.170> you<00:15:25.590> generate 00:15:25.940 --> 00:15:25.950 align:start position:0% bunch of wider rules and you generate 00:15:25.950 --> 00:15:29.960 align:start position:0% bunch of wider rules and you generate from<00:15:27.740> encoding<00:15:28.740> this<00:15:28.920> discomfort<00:15:29.460> flow<00:15:29.760> graph 00:15:29.960 --> 00:15:29.970 align:start position:0% from encoding this discomfort flow graph 00:15:29.970 --> 00:15:32.240 align:start position:0% from encoding this discomfort flow graph into<00:15:30.390> more<00:15:30.540> clauses<00:15:30.750> not<00:15:31.590> all<00:15:31.800> of<00:15:31.950> them<00:15:32.130> are 00:15:32.240 --> 00:15:32.250 align:start position:0% into more clauses not all of them are 00:15:32.250 --> 00:15:34.940 align:start position:0% into more clauses not all of them are here<00:15:33.200> for<00:15:34.200> the<00:15:34.290> length<00:15:34.410> of<00:15:34.530> time<00:15:34.590> I'm<00:15:34.800> not 00:15:34.940 --> 00:15:34.950 align:start position:0% here for the length of time I'm not 00:15:34.950 --> 00:15:39.080 align:start position:0% here for the length of time I'm not gonna<00:15:35.070> go<00:15:36.710> by<00:15:37.710> each<00:15:37.890> of<00:15:38.040> them<00:15:38.220> we<00:15:38.550> can<00:15:38.730> talk 00:15:39.080 --> 00:15:39.090 align:start position:0% gonna go by each of them we can talk 00:15:39.090 --> 00:15:42.230 align:start position:0% gonna go by each of them we can talk later<00:15:40.010> okay<00:15:41.010> so<00:15:41.070> as<00:15:41.550> I<00:15:41.640> mentioned<00:15:41.850> before<00:15:41.910> the 00:15:42.230 --> 00:15:42.240 align:start position:0% later okay so as I mentioned before the 00:15:42.240 --> 00:15:43.400 align:start position:0% later okay so as I mentioned before the problem<00:15:42.420> that<00:15:42.660> we're<00:15:42.780> trying<00:15:42.810> to<00:15:42.990> solve<00:15:43.200> is 00:15:43.400 --> 00:15:43.410 align:start position:0% problem that we're trying to solve is 00:15:43.410 --> 00:15:45.260 align:start position:0% problem that we're trying to solve is family<00:15:43.770> guide<00:15:43.980> on<00:15:44.220> the<00:15:44.340> Google<00:15:44.490> structure<00:15:44.850> to 00:15:45.260 --> 00:15:45.270 align:start position:0% family guide on the Google structure to 00:15:45.270 --> 00:15:48.650 align:start position:0% family guide on the Google structure to the<00:15:45.360> area<00:15:45.600> state<00:15:45.920> and<00:15:47.030> in<00:15:48.030> the<00:15:48.150> first<00:15:48.330> example 00:15:48.650 --> 00:15:48.660 align:start position:0% the area state and in the first example 00:15:48.660 --> 00:15:50.660 align:start position:0% the area state and in the first example that<00:15:48.690> I<00:15:48.810> showed<00:15:49.250> garrison<00:15:50.250> was<00:15:50.370> enriching 00:15:50.660 --> 00:15:50.670 align:start position:0% that I showed garrison was enriching 00:15:50.670 --> 00:15:53.810 align:start position:0% that I showed garrison was enriching water<00:15:50.940> and<00:15:51.930> the<00:15:52.020> way<00:15:52.140> to<00:15:52.200> finds<00:15:52.410> out<00:15:52.620> is<00:15:52.950> that 00:15:53.810 --> 00:15:53.820 align:start position:0% water and the way to finds out is that 00:15:53.820 --> 00:15:55.820 align:start position:0% water and the way to finds out is that all<00:15:54.240> this<00:15:54.570> green<00:15:54.840> members<00:15:55.260> form<00:15:55.470> a<00:15:55.560> fixed 00:15:55.820 --> 00:15:55.830 align:start position:0% all this green members form a fixed 00:15:55.830 --> 00:15:57.770 align:start position:0% all this green members form a fixed point<00:15:56.010> where<00:15:56.400> every<00:15:56.910> transition<00:15:57.270> leads<00:15:57.600> to<00:15:57.750> a 00:15:57.770 --> 00:15:57.780 align:start position:0% point where every transition leads to a 00:15:57.780 --> 00:15:59.480 align:start position:0% point where every transition leads to a node<00:15:58.020> then<00:15:58.380> it<00:15:58.470> sort<00:15:58.650> of<00:15:58.710> is<00:15:58.860> already<00:15:59.070> that's 00:15:59.480 --> 00:15:59.490 align:start position:0% node then it sort of is already that's 00:15:59.490 --> 00:16:01.760 align:start position:0% node then it sort of is already that's set<00:15:59.730> so<00:16:00.390> you<00:16:00.450> never<00:16:00.630> get<00:16:00.870> out<00:16:01.020> of<00:16:01.140> this<00:16:01.260> set<00:16:01.530> and 00:16:01.760 --> 00:16:01.770 align:start position:0% set so you never get out of this set and 00:16:01.770 --> 00:16:04.040 align:start position:0% set so you never get out of this set and you<00:16:02.460> finally<00:16:02.820> see<00:16:02.970> that<00:16:03.000> error<00:16:03.330> state<00:16:03.750> is<00:16:03.900> not 00:16:04.040 --> 00:16:04.050 align:start position:0% you finally see that error state is not 00:16:04.050 --> 00:16:06.320 align:start position:0% you finally see that error state is not reachable<00:16:04.380> at<00:16:04.590> all<00:16:04.710> and<00:16:05.100> this<00:16:05.760> is<00:16:06.000> all 00:16:06.320 --> 00:16:06.330 align:start position:0% reachable at all and this is all 00:16:06.330 --> 00:16:09.980 align:start position:0% reachable at all and this is all possible<00:16:07.760> because<00:16:08.760> of<00:16:08.940> this<00:16:09.150> really<00:16:09.540> nice<00:16:09.690> and 00:16:09.980 --> 00:16:09.990 align:start position:0% possible because of this really nice and 00:16:09.990 --> 00:16:11.390 align:start position:0% possible because of this really nice and coated<00:16:10.140> that<00:16:10.350> we<00:16:10.440> can<00:16:10.590> just<00:16:10.770> directly<00:16:10.920> from 00:16:11.390 --> 00:16:11.400 align:start position:0% coated that we can just directly from 00:16:11.400 --> 00:16:12.620 align:start position:0% coated that we can just directly from the<00:16:11.550> control<00:16:11.820> flow<00:16:11.940> graph<00:16:11.970> to<00:16:12.180> different 00:16:12.620 --> 00:16:12.630 align:start position:0% the control flow graph to different 00:16:12.630 --> 00:16:14.690 align:start position:0% the control flow graph to different buses<00:16:12.780> which<00:16:13.380> looks<00:16:13.620> very<00:16:13.680> very<00:16:14.100> very<00:16:14.310> similar 00:16:14.690 --> 00:16:14.700 align:start position:0% buses which looks very very very similar 00:16:14.700 --> 00:16:16.250 align:start position:0% buses which looks very very very similar and<00:16:15.210> this<00:16:15.330> is<00:16:15.420> only<00:16:15.540> possible<00:16:15.780> because<00:16:16.080> of 00:16:16.250 --> 00:16:16.260 align:start position:0% and this is only possible because of 00:16:16.260 --> 00:16:19.910 align:start position:0% and this is only possible because of these<00:16:16.470> two<00:16:16.620> results<00:16:16.920> so<00:16:17.220> we<00:16:17.760> gotta<00:16:18.000> go<00:16:18.710> all<00:16:19.710> the 00:16:19.910 --> 00:16:19.920 align:start position:0% these two results so we gotta go all the 00:16:19.920 --> 00:16:22.579 align:start position:0% these two results so we gotta go all the way<00:16:19.950> from<00:16:20.430> more<00:16:20.700> logic<00:16:21.150> to<00:16:21.589> expect 00:16:22.579 --> 00:16:22.589 align:start position:0% way from more logic to expect 00:16:22.589 --> 00:16:24.680 align:start position:0% way from more logic to expect existential<00:16:23.130> positive<00:16:23.520> lead<00:16:24.210> speaks<00:16:24.510> point 00:16:24.680 --> 00:16:24.690 align:start position:0% existential positive lead speaks point 00:16:24.690 --> 00:16:27.200 align:start position:0% existential positive lead speaks point logic<00:16:25.190> which<00:16:26.190> is<00:16:26.220> actually<00:16:26.670> what<00:16:26.790> we're<00:16:26.940> doing 00:16:27.200 --> 00:16:27.210 align:start position:0% logic which is actually what we're doing 00:16:27.210 --> 00:16:29.300 align:start position:0% logic which is actually what we're doing but<00:16:27.600> there<00:16:27.750> is<00:16:27.839> a<00:16:27.870> connection<00:16:28.140> between<00:16:28.500> this 00:16:29.300 --> 00:16:29.310 align:start position:0% but there is a connection between this 00:16:29.310 --> 00:16:31.790 align:start position:0% but there is a connection between this logic<00:16:29.790> and<00:16:29.970> post<00:16:30.150> remark<00:16:30.480> buzzes<00:16:30.839> which<00:16:31.470> gives 00:16:31.790 --> 00:16:31.800 align:start position:0% logic and post remark buzzes which gives 00:16:31.800 --> 00:16:35.780 align:start position:0% logic and post remark buzzes which gives us<00:16:31.920> this<00:16:32.070> really<00:16:32.220> nice<00:16:32.430> encoding<00:16:34.490> but<00:16:35.490> what<00:16:35.670> if 00:16:35.780 --> 00:16:35.790 align:start position:0% us this really nice encoding but what if 00:16:35.790 --> 00:16:39.590 align:start position:0% us this really nice encoding but what if now<00:16:36.000> I<00:16:36.030> changed<00:16:36.750> my<00:16:37.680> first<00:16:37.950> example<00:16:38.310> from<00:16:39.150> G 00:16:39.590 --> 00:16:39.600 align:start position:0% now I changed my first example from G 00:16:39.600 --> 00:16:44.180 align:start position:0% now I changed my first example from G changing<00:16:40.200> Y<00:16:40.860> from<00:16:41.130> 1<00:16:41.339> to<00:16:41.460> 0<00:16:41.490> to<00:16:41.880> 2<00:16:42.060> now<00:16:42.980> is<00:16:43.980> there 00:16:44.180 --> 00:16:44.190 align:start position:0% changing Y from 1 to 0 to 2 now is there 00:16:44.190 --> 00:16:56.990 align:start position:0% changing Y from 1 to 0 to 2 now is there today<00:16:44.550> still<00:16:45.000> unreachable<00:16:45.330> rice<00:16:46.320> vegetable 00:16:56.990 --> 00:16:57.000 align:start position:0% 00:16:57.000 --> 00:17:03.930 align:start position:0% it's<00:16:58.649> its<00:16:59.649> ritual<00:17:00.160> right<00:17:02.339> yeah<00:17:03.339> so<00:17:03.670> I'm<00:17:03.760> just 00:17:03.930 --> 00:17:03.940 align:start position:0% it's its ritual right yeah so I'm just 00:17:03.940 --> 00:17:07.710 align:start position:0% it's its ritual right yeah so I'm just gonna<00:17:04.059> quickly<00:17:04.920> and<00:17:05.920> here<00:17:06.790> it's<00:17:06.880> us<00:17:07.059> yes<00:17:07.420> your 00:17:07.710 --> 00:17:07.720 align:start position:0% gonna quickly and here it's us yes your 00:17:07.720 --> 00:17:10.530 align:start position:0% gonna quickly and here it's us yes your jewel<00:17:07.839> your<00:17:08.079> assertions<00:17:08.470> wrong<00:17:09.240> X<00:17:10.240> can<00:17:10.449> also 00:17:10.530 --> 00:17:10.540 align:start position:0% jewel your assertions wrong X can also 00:17:10.540 --> 00:17:13.319 align:start position:0% jewel your assertions wrong X can also be<00:17:10.839> too<00:17:11.079> and<00:17:11.500> what<00:17:11.980> it<00:17:12.069> also<00:17:12.250> tells<00:17:12.579> us<00:17:12.819> and<00:17:13.089> is 00:17:13.319 --> 00:17:13.329 align:start position:0% be too and what it also tells us and is 00:17:13.329 --> 00:17:14.579 align:start position:0% be too and what it also tells us and is going<00:17:13.480> to<00:17:13.569> look<00:17:13.689> better<00:17:13.839> eventually<00:17:14.350> but 00:17:14.579 --> 00:17:14.589 align:start position:0% going to look better eventually but 00:17:14.589 --> 00:17:16.679 align:start position:0% going to look better eventually but which<00:17:15.069> is<00:17:15.189> really<00:17:15.370> important<00:17:15.760> this<00:17:16.120> these 00:17:16.679 --> 00:17:16.689 align:start position:0% which is really important this these 00:17:16.689 --> 00:17:19.650 align:start position:0% which is really important this these things<00:17:17.500> here<00:17:17.829> this<00:17:18.550> is<00:17:18.670> telling<00:17:18.910> us<00:17:19.000> backwards 00:17:19.650 --> 00:17:19.660 align:start position:0% things here this is telling us backwards 00:17:19.660 --> 00:17:21.929 align:start position:0% things here this is telling us backwards which<00:17:20.110> transactions<00:17:20.829> or<00:17:21.280> which<00:17:21.490> loop 00:17:21.929 --> 00:17:21.939 align:start position:0% which transactions or which loop 00:17:21.939 --> 00:17:25.919 align:start position:0% which transactions or which loop iterations<00:17:22.540> LED<00:17:23.380> and<00:17:24.250> this<00:17:25.059> is<00:17:25.209> just<00:17:25.390> enough 00:17:25.919 --> 00:17:25.929 align:start position:0% iterations LED and this is just enough 00:17:25.929 --> 00:17:27.929 align:start position:0% iterations LED and this is just enough that<00:17:26.110> so<00:17:26.470> but<00:17:26.620> this<00:17:26.709> is<00:17:26.770> telling<00:17:27.100> us<00:17:27.160> that<00:17:27.309> we 00:17:27.929 --> 00:17:27.939 align:start position:0% that so but this is telling us that we 00:17:27.939 --> 00:17:30.150 align:start position:0% that so but this is telling us that we can<00:17:28.179> call<00:17:28.420> invariant<00:17:28.960> and<00:17:29.170> make<00:17:29.380> it<00:17:29.590> make<00:17:30.040> the 00:17:30.150 --> 00:17:30.160 align:start position:0% can call invariant and make it make the 00:17:30.160 --> 00:17:32.900 align:start position:0% can call invariant and make it make the error<00:17:30.370> reachable<00:17:30.940> but<00:17:31.360> if<00:17:31.540> because<00:17:32.050> access<00:17:32.590> to 00:17:32.900 --> 00:17:32.910 align:start position:0% error reachable but if because access to 00:17:32.910 --> 00:17:35.549 align:start position:0% error reachable but if because access to there<00:17:33.910> was<00:17:34.000> a<00:17:34.059> transaction<00:17:34.330> that<00:17:34.570> main<00:17:34.840> Axew 00:17:35.549 --> 00:17:35.559 align:start position:0% there was a transaction that main Axew 00:17:35.559 --> 00:17:38.190 align:start position:0% there was a transaction that main Axew before<00:17:35.980> that<00:17:36.190> was<00:17:36.700> actually<00:17:37.090> made<00:17:37.300> x1<00:17:37.990> and 00:17:38.190 --> 00:17:38.200 align:start position:0% before that was actually made x1 and 00:17:38.200 --> 00:17:40.980 align:start position:0% before that was actually made x1 and before<00:17:38.740> that<00:17:38.770> dress<00:17:39.250> resection<00:17:39.550> made<00:17:39.940> X<00:17:40.270> 0<00:17:40.600> and 00:17:40.980 --> 00:17:40.990 align:start position:0% before that dress resection made X 0 and 00:17:40.990 --> 00:17:47.700 align:start position:0% before that dress resection made X 0 and if<00:17:41.890> we<00:17:42.040> look<00:17:42.280> back<00:17:42.900> in<00:17:43.900> the<00:17:45.990> in<00:17:46.990> the<00:17:47.200> graph<00:17:47.410> so 00:17:47.700 --> 00:17:47.710 align:start position:0% if we look back in the in the graph so 00:17:47.710 --> 00:17:49.560 align:start position:0% if we look back in the in the graph so he<00:17:47.980> this<00:17:48.190> would<00:17:48.550> be<00:17:48.640> the<00:17:48.730> first<00:17:48.880> one<00:17:49.150> so<00:17:49.420> with 00:17:49.560 --> 00:17:49.570 align:start position:0% he this would be the first one so with 00:17:49.570 --> 00:17:51.540 align:start position:0% he this would be the first one so with the<00:17:49.660> bloody<00:17:49.870> bucket<00:17:50.020> right<00:17:50.590> so<00:17:51.040> X<00:17:51.220> is<00:17:51.370> zero 00:17:51.540 --> 00:17:51.550 align:start position:0% the bloody bucket right so X is zero 00:17:51.550 --> 00:17:54.090 align:start position:0% the bloody bucket right so X is zero said<00:17:51.850> this<00:17:52.179> is<00:17:52.360> the<00:17:52.570> real<00:17:53.530> truth<00:17:53.890> from 00:17:54.090 --> 00:17:54.100 align:start position:0% said this is the real truth from 00:17:54.100 --> 00:17:56.400 align:start position:0% said this is the real truth from constructor<00:17:54.580> to<00:17:54.760> interface<00:17:55.090> the<00:17:55.840> next<00:17:56.050> one<00:17:56.230> we 00:17:56.400 --> 00:17:56.410 align:start position:0% constructor to interface the next one we 00:17:56.410 --> 00:17:59.100 align:start position:0% constructor to interface the next one we call<00:17:56.620> function<00:17:56.980> hath<00:17:57.160> which<00:17:57.850> then<00:17:58.120> changing 00:17:59.100 --> 00:17:59.110 align:start position:0% call function hath which then changing 00:17:59.110 --> 00:18:01.350 align:start position:0% call function hath which then changing this<00:17:59.170> X<00:17:59.500> from<00:17:59.710> 1<00:17:59.920> to<00:18:00.190> 0<00:18:00.220> and<00:18:00.670> we're<00:18:01.030> back<00:18:01.150> to<00:18:01.210> the 00:18:01.350 --> 00:18:01.360 align:start position:0% this X from 1 to 0 and we're back to the 00:18:01.360 --> 00:18:04.290 align:start position:0% this X from 1 to 0 and we're back to the interface<00:18:01.750> the<00:18:02.559> next<00:18:02.830> one<00:18:03.040> she<00:18:03.670> changed<00:18:04.120> it<00:18:04.179> to 00:18:04.290 --> 00:18:04.300 align:start position:0% interface the next one she changed it to 00:18:04.300 --> 00:18:06.810 align:start position:0% interface the next one she changed it to 2<00:18:04.480> and<00:18:05.470> now<00:18:05.559> we<00:18:05.620> finally<00:18:05.950> call<00:18:06.610> books 00:18:06.810 --> 00:18:06.820 align:start position:0% 2 and now we finally call books 00:18:06.820 --> 00:18:09.180 align:start position:0% 2 and now we finally call books invariant<00:18:07.300> and<00:18:07.510> reach<00:18:07.840> the<00:18:08.020> air<00:18:08.170> where<00:18:08.980> the 00:18:09.180 --> 00:18:09.190 align:start position:0% invariant and reach the air where the 00:18:09.190 --> 00:18:11.490 align:start position:0% invariant and reach the air where the sequence<00:18:09.520> here<00:18:09.730> is<00:18:09.940> deployment<00:18:10.570> FG<00:18:11.230> and 00:18:11.490 --> 00:18:11.500 align:start position:0% sequence here is deployment FG and 00:18:11.500 --> 00:18:17.760 align:start position:0% sequence here is deployment FG and ingrained<00:18:14.760> so<00:18:16.050> this<00:18:17.050> is<00:18:17.200> how<00:18:17.350> definitely 00:18:17.760 --> 00:18:17.770 align:start position:0% ingrained so this is how definitely 00:18:17.770 --> 00:18:20.190 align:start position:0% ingrained so this is how definitely check<00:18:17.980> those<00:18:18.309> things<00:18:18.700> and<00:18:19.030> in<00:18:19.660> the<00:18:19.840> back<00:18:19.870> end 00:18:20.190 --> 00:18:20.200 align:start position:0% check those things and in the back end 00:18:20.200 --> 00:18:22.860 align:start position:0% check those things and in the back end it<00:18:20.320> uses<00:18:20.790> these<00:18:21.790> tools<00:18:22.059> before<00:18:22.240> of<00:18:22.510> similars 00:18:22.860 --> 00:18:22.870 align:start position:0% it uses these tools before of similars 00:18:22.870 --> 00:18:25.320 align:start position:0% it uses these tools before of similars which<00:18:22.990> is<00:18:23.110> he'll<00:18:23.260> into<00:18:23.620> similar<00:18:24.340> anyway<00:18:24.700> sn2 00:18:25.320 --> 00:18:25.330 align:start position:0% which is he'll into similar anyway sn2 00:18:25.330 --> 00:18:28.590 align:start position:0% which is he'll into similar anyway sn2 stores<00:18:25.660> also<00:18:25.990> uses<00:18:26.380> us<00:18:26.500> into<00:18:26.740> sores<00:18:27.070> and<00:18:27.600> corn 00:18:28.590 --> 00:18:28.600 align:start position:0% stores also uses us into sores and corn 00:18:28.600 --> 00:18:30.419 align:start position:0% stores also uses us into sores and corn slovers<00:18:28.960> basically<00:18:29.380> they<00:18:29.590> take<00:18:30.070> all<00:18:30.250> these 00:18:30.419 --> 00:18:30.429 align:start position:0% slovers basically they take all these 00:18:30.429 --> 00:18:33.150 align:start position:0% slovers basically they take all these rules<00:18:30.670> that<00:18:30.910> a<00:18:31.000> that<00:18:31.330> I<00:18:31.360> wrote<00:18:31.660> and<00:18:32.160> a 00:18:33.150 --> 00:18:33.160 align:start position:0% rules that a that I wrote and a 00:18:33.160 --> 00:18:35.870 align:start position:0% rules that a that I wrote and a reachability<00:18:33.760> query<00:18:34.179> say<00:18:34.450> say<00:18:34.660> can<00:18:35.050> I<00:18:35.080> get<00:18:35.320> two 00:18:35.870 --> 00:18:35.880 align:start position:0% reachability query say say can I get two 00:18:35.880 --> 00:18:39.840 align:start position:0% reachability query say say can I get two predicates<00:18:36.880> error<00:18:37.059> and<00:18:37.559> it<00:18:38.559> tells<00:18:38.860> you<00:18:39.070> yes<00:18:39.490> or 00:18:39.840 --> 00:18:39.850 align:start position:0% predicates error and it tells you yes or 00:18:39.850 --> 00:18:40.169 align:start position:0% predicates error and it tells you yes or no 00:18:40.169 --> 00:18:40.179 align:start position:0% no 00:18:40.179 --> 00:18:43.440 align:start position:0% no and<00:18:40.360> the<00:18:41.110> way<00:18:41.350> these<00:18:41.800> horse<00:18:42.070> loggers<00:18:42.280> do<00:18:43.120> this 00:18:43.440 --> 00:18:43.450 align:start position:0% and the way these horse loggers do this 00:18:43.450 --> 00:18:46.080 align:start position:0% and the way these horse loggers do this is<00:18:43.840> in<00:18:44.320> this<00:18:44.559> regular<00:18:44.920> instruction<00:18:45.100> all<00:18:45.820> this 00:18:46.080 --> 00:18:46.090 align:start position:0% is in this regular instruction all this 00:18:46.090 --> 00:18:49.830 align:start position:0% is in this regular instruction all this this<00:18:46.980> techniques<00:18:47.980> here<00:18:48.190> but<00:18:49.059> the<00:18:49.270> one<00:18:49.450> we<00:18:49.600> use 00:18:49.830 --> 00:18:49.840 align:start position:0% this techniques here but the one we use 00:18:49.840 --> 00:18:52.380 align:start position:0% this techniques here but the one we use is<00:18:50.260> actually<00:18:50.440> pull<00:18:50.800> off<00:18:50.920> a<00:18:51.220> certainty<00:18:52.210> based 00:18:52.380 --> 00:18:52.390 align:start position:0% is actually pull off a certainty based 00:18:52.390 --> 00:18:53.280 align:start position:0% is actually pull off a certainty based on 00:18:53.280 --> 00:18:53.290 align:start position:0% on 00:18:53.290 --> 00:18:55.890 align:start position:0% on with<00:18:54.160> a<00:18:54.190> technical<00:18:54.700> PDR<00:18:55.120> meaning<00:18:55.480> property 00:18:55.890 --> 00:18:55.900 align:start position:0% with a technical PDR meaning property 00:18:55.900 --> 00:18:58.020 align:start position:0% with a technical PDR meaning property director<00:18:56.260> ability<00:18:56.800> what<00:18:57.400> he<00:18:57.460> does<00:18:57.640> from<00:18:58.000> the 00:18:58.020 --> 00:18:58.030 align:start position:0% director ability what he does from the 00:18:58.030 --> 00:19:00.780 align:start position:0% director ability what he does from the area<00:18:58.390> state<00:18:58.630> it<00:18:59.200> tries<00:18:59.440> to<00:18:59.470> this<00:19:00.460> effect 00:19:00.780 --> 00:19:00.790 align:start position:0% area state it tries to this effect 00:19:00.790 --> 00:19:02.970 align:start position:0% area state it tries to this effect burger<00:19:01.030> to<00:19:01.240> ability<00:19:01.390> check<00:19:01.810> trying<00:19:02.680> to<00:19:02.830> get 00:19:02.970 --> 00:19:02.980 align:start position:0% burger to ability check trying to get 00:19:02.980 --> 00:19:05.190 align:start position:0% burger to ability check trying to get all<00:19:03.190> the<00:19:03.370> way<00:19:03.520> to<00:19:03.850> the<00:19:04.300> constructor<00:19:04.720> which<00:19:05.080> is 00:19:05.190 --> 00:19:05.200 align:start position:0% all the way to the constructor which is 00:19:05.200 --> 00:19:06.750 align:start position:0% all the way to the constructor which is the<00:19:05.290> only<00:19:05.530> fact<00:19:05.860> it's<00:19:06.070> the<00:19:06.160> only<00:19:06.220> predicate 00:19:06.750 --> 00:19:06.760 align:start position:0% the only fact it's the only predicate 00:19:06.760 --> 00:19:08.580 align:start position:0% the only fact it's the only predicate that<00:19:06.790> is<00:19:07.030> not<00:19:07.150> actually<00:19:07.330> applied<00:19:07.810> but<00:19:08.410> many 00:19:08.580 --> 00:19:08.590 align:start position:0% that is not actually applied but many 00:19:08.590 --> 00:19:12.510 align:start position:0% that is not actually applied but many other<00:19:08.770> predicates<00:19:09.250> and<00:19:10.920> it<00:19:11.920> does<00:19:12.100> that<00:19:12.250> by 00:19:12.510 --> 00:19:12.520 align:start position:0% other predicates and it does that by 00:19:12.520 --> 00:19:14.070 align:start position:0% other predicates and it does that by generating<00:19:12.670> a<00:19:13.120> bunch<00:19:13.300> of<00:19:13.390> quantifier<00:19:13.840> free 00:19:14.070 --> 00:19:14.080 align:start position:0% generating a bunch of quantifier free 00:19:14.080 --> 00:19:17.100 align:start position:0% generating a bunch of quantifier free SMT<00:19:14.530> queries<00:19:14.920> in<00:19:15.550> brokenness<00:19:16.000> into<00:19:16.270> solar<00:19:16.510> and 00:19:17.100 --> 00:19:17.110 align:start position:0% SMT queries in brokenness into solar and 00:19:17.110 --> 00:19:19.560 align:start position:0% SMT queries in brokenness into solar and use<00:19:17.230> interpolation<00:19:17.920> as<00:19:18.160> as<00:19:18.940> a<00:19:19.000> method<00:19:19.420> for 00:19:19.560 --> 00:19:19.570 align:start position:0% use interpolation as as a method for 00:19:19.570 --> 00:19:22.020 align:start position:0% use interpolation as as a method for obstruction<00:19:20.110> to<00:19:20.260> find<00:19:21.100> predecessors<00:19:21.790> in<00:19:21.940> a 00:19:22.020 --> 00:19:22.030 align:start position:0% obstruction to find predecessors in a 00:19:22.030 --> 00:19:24.270 align:start position:0% obstruction to find predecessors in a state<00:19:22.270> doing<00:19:22.690> the<00:19:22.840> backwards<00:19:22.990> of<00:19:23.470> utility<00:19:23.980> and 00:19:24.270 --> 00:19:24.280 align:start position:0% state doing the backwards of utility and 00:19:24.280 --> 00:19:28.470 align:start position:0% state doing the backwards of utility and generate<00:19:24.700> dilemmas<00:19:25.240> and<00:19:25.510> invariance<00:19:27.300> so<00:19:28.300> this 00:19:28.470 --> 00:19:28.480 align:start position:0% generate dilemmas and invariance so this 00:19:28.480 --> 00:19:30.930 align:start position:0% generate dilemmas and invariance so this is<00:19:28.600> implemented<00:19:29.140> in<00:19:29.710> this<00:19:29.950> little<00:19:30.370> weather<00:19:30.550> in 00:19:30.930 --> 00:19:30.940 align:start position:0% is implemented in this little weather in 00:19:30.940 --> 00:19:32.850 align:start position:0% is implemented in this little weather in the<00:19:31.360> model<00:19:31.660> much<00:19:31.930> will<00:19:32.080> call<00:19:32.260> this<00:19:32.350> MC<00:19:32.620> checker 00:19:32.850 --> 00:19:32.860 align:start position:0% the model much will call this MC checker 00:19:32.860 --> 00:19:35.430 align:start position:0% the model much will call this MC checker right<00:19:33.570> you<00:19:34.570> know<00:19:34.720> there's<00:19:34.900> a<00:19:34.960> lot<00:19:35.170> of<00:19:35.200> support 00:19:35.430 --> 00:19:35.440 align:start position:0% right you know there's a lot of support 00:19:35.440 --> 00:19:37.530 align:start position:0% right you know there's a lot of support to<00:19:35.680> the<00:19:35.800> language<00:19:36.070> there's<00:19:36.430> a<00:19:36.490> few<00:19:36.940> things 00:19:37.530 --> 00:19:37.540 align:start position:0% to the language there's a few things 00:19:37.540 --> 00:19:40.470 align:start position:0% to the language there's a few things missing<00:19:38.260> but<00:19:38.800> it<00:19:39.490> can<00:19:39.700> reversed<00:19:40.120> by<00:19:40.270> a<00:19:40.300> lot<00:19:40.450> of 00:19:40.470 --> 00:19:40.480 align:start position:0% missing but it can reversed by a lot of 00:19:40.480 --> 00:19:46.500 align:start position:0% missing but it can reversed by a lot of things<00:19:41.250> and<00:19:42.250> this<00:19:44.040> module<00:19:45.040> this<00:19:45.730> part<00:19:46.180> of<00:19:46.330> it 00:19:46.500 --> 00:19:46.510 align:start position:0% things and this module this part of it 00:19:46.510 --> 00:19:51.420 align:start position:0% things and this module this part of it the<00:19:47.080> horn<00:19:47.380> based<00:19:48.690> algorithms<00:19:49.800> can<00:19:50.800> I<00:19:50.830> find 00:19:51.420 --> 00:19:51.430 align:start position:0% the horn based algorithms can I find 00:19:51.430 --> 00:19:56.400 align:start position:0% the horn based algorithms can I find books<00:19:52.330> or<00:19:52.570> proven<00:19:53.140> variants<00:19:53.500> for<00:19:55.410> multi 00:19:56.400 --> 00:19:56.410 align:start position:0% books or proven variants for multi 00:19:56.410 --> 00:19:58.470 align:start position:0% books or proven variants for multi multiple<00:19:56.860> section<00:19:57.280> properties<00:19:57.460> so<00:19:58.150> all 00:19:58.470 --> 00:19:58.480 align:start position:0% multiple section properties so all 00:19:58.480 --> 00:20:01.500 align:start position:0% multiple section properties so all different<00:19:58.780> sections<00:19:59.050> safety<00:19:59.350> properties<00:20:00.510> but 00:20:01.500 --> 00:20:01.510 align:start position:0% different sections safety properties but 00:20:01.510 --> 00:20:03.450 align:start position:0% different sections safety properties but there's<00:20:01.750> still<00:20:01.930> thing<00:20:02.230> reason<00:20:02.800> so<00:20:03.070> what's 00:20:03.450 --> 00:20:03.460 align:start position:0% there's still thing reason so what's 00:20:03.460 --> 00:20:06.330 align:start position:0% there's still thing reason so what's next<00:20:04.140> function<00:20:05.140> Falls<00:20:05.320> was<00:20:05.500> important<00:20:05.890> and<00:20:06.040> we 00:20:06.330 --> 00:20:06.340 align:start position:0% next function Falls was important and we 00:20:06.340 --> 00:20:07.770 align:start position:0% next function Falls was important and we went<00:20:06.520> into<00:20:06.610> that<00:20:06.730> by<00:20:07.060> creating<00:20:07.270> monocle 00:20:07.770 --> 00:20:07.780 align:start position:0% went into that by creating monocle 00:20:07.780 --> 00:20:09.180 align:start position:0% went into that by creating monocle functions<00:20:08.140> somewhere<00:20:08.440> inside<00:20:08.740> there<00:20:08.890> so 00:20:09.180 --> 00:20:09.190 align:start position:0% functions somewhere inside there so 00:20:09.190 --> 00:20:11.070 align:start position:0% functions somewhere inside there so agreed<00:20:09.400> this<00:20:09.490> bunch<00:20:09.730> of<00:20:09.850> summaries<00:20:10.180> and<00:20:10.450> then 00:20:11.070 --> 00:20:11.080 align:start position:0% agreed this bunch of summaries and then 00:20:11.080 --> 00:20:13.800 align:start position:0% agreed this bunch of summaries and then you<00:20:11.560> can<00:20:11.830> assert<00:20:12.370> them<00:20:12.580> that<00:20:12.790> summary<00:20:13.210> is<00:20:13.420> true 00:20:13.800 --> 00:20:13.810 align:start position:0% you can assert them that summary is true 00:20:13.810 --> 00:20:15.720 align:start position:0% you can assert them that summary is true for<00:20:14.350> a<00:20:14.410> certain<00:20:14.680> certain<00:20:14.890> set<00:20:15.190> of<00:20:15.220> variables 00:20:15.720 --> 00:20:15.730 align:start position:0% for a certain certain set of variables 00:20:15.730 --> 00:20:18.690 align:start position:0% for a certain certain set of variables and<00:20:16.140> this<00:20:17.140> can<00:20:17.350> also<00:20:17.470> be<00:20:17.590> nice<00:20:17.860> to<00:20:18.460> show<00:20:18.640> that 00:20:18.690 --> 00:20:18.700 align:start position:0% and this can also be nice to show that 00:20:18.700 --> 00:20:20.400 align:start position:0% and this can also be nice to show that there's<00:20:18.910> no<00:20:19.120> changes<00:20:19.510> in<00:20:19.630> the<00:20:19.720> state<00:20:19.930> of<00:20:20.170> the 00:20:20.400 --> 00:20:20.410 align:start position:0% there's no changes in the state of the 00:20:20.410 --> 00:20:23.160 align:start position:0% there's no changes in the state of the caller<00:20:20.770> contract<00:20:21.340> so<00:20:22.000> this<00:20:22.210> is<00:20:22.390> related<00:20:23.140> to 00:20:23.160 --> 00:20:23.170 align:start position:0% caller contract so this is related to 00:20:23.170 --> 00:20:26.250 align:start position:0% caller contract so this is related to re-enter<00:20:23.620> ax<00:20:23.680> C<00:20:24.690> synthesis<00:20:25.690> of<00:20:25.780> external 00:20:26.250 --> 00:20:26.260 align:start position:0% re-enter ax C synthesis of external 00:20:26.260 --> 00:20:27.900 align:start position:0% re-enter ax C synthesis of external functions<00:20:26.710> that<00:20:26.980> don't<00:20:27.190> have<00:20:27.400> access<00:20:27.790> to 00:20:27.900 --> 00:20:27.910 align:start position:0% functions that don't have access to 00:20:27.910 --> 00:20:30.310 align:start position:0% functions that don't have access to decode<00:20:28.270> my<00:20:28.960> also<00:20:29.170> deny<00:20:29.560> expansion 00:20:30.310 --> 00:20:30.320 align:start position:0% decode my also deny expansion 00:20:30.320 --> 00:20:35.560 align:start position:0% decode my also deny expansion examples<00:20:31.120> this<00:20:32.120> all<00:20:32.389> would<00:20:32.600> lead<00:20:32.779> to<00:20:34.570> the 00:20:35.560 --> 00:20:35.570 align:start position:0% examples this all would lead to the 00:20:35.570 --> 00:20:37.450 align:start position:0% examples this all would lead to the possibility<00:20:35.750> of<00:20:36.200> verifying<00:20:36.710> really<00:20:37.070> complex 00:20:37.450 --> 00:20:37.460 align:start position:0% possibility of verifying really complex 00:20:37.460 --> 00:20:40.539 align:start position:0% possibility of verifying really complex contracts<00:20:38.269> and<00:20:38.570> and<00:20:38.870> setups<00:20:39.289> when<00:20:40.279> you<00:20:40.370> like 00:20:40.539 --> 00:20:40.549 align:start position:0% contracts and and setups when you like 00:20:40.549 --> 00:20:43.330 align:start position:0% contracts and and setups when you like when<00:20:40.700> you<00:20:40.789> have<00:20:40.940> multi<00:20:41.389> contract<00:20:42.340> multi 00:20:43.330 --> 00:20:43.340 align:start position:0% when you have multi contract multi 00:20:43.340 --> 00:20:46.330 align:start position:0% when you have multi contract multi transaction<00:20:44.029> properties<00:20:44.350> that<00:20:45.350> might<00:20:46.220> be 00:20:46.330 --> 00:20:46.340 align:start position:0% transaction properties that might be 00:20:46.340 --> 00:20:47.680 align:start position:0% transaction properties that might be really<00:20:46.549> hard<00:20:46.820> to<00:20:46.909> find<00:20:46.970> otherwise 00:20:47.680 --> 00:20:47.690 align:start position:0% really hard to find otherwise 00:20:47.690 --> 00:20:50.649 align:start position:0% really hard to find otherwise and<00:20:48.169> maybe<00:20:48.830> eventually<00:20:49.700> model<00:20:50.509> the<00:20:50.600> entire 00:20:50.649 --> 00:20:50.659 align:start position:0% and maybe eventually model the entire 00:20:50.659 --> 00:20:52.659 align:start position:0% and maybe eventually model the entire state<00:20:51.200> of<00:20:51.350> the<00:20:51.740> blockchain 00:20:52.659 --> 00:20:52.669 align:start position:0% state of the blockchain 00:20:52.669 --> 00:20:55.600 align:start position:0% state of the blockchain another<00:20:53.509> thing<00:20:53.720> is<00:20:53.990> showing<00:20:54.950> nice-looking 00:20:55.600 --> 00:20:55.610 align:start position:0% another thing is showing nice-looking 00:20:55.610 --> 00:20:57.930 align:start position:0% another thing is showing nice-looking other<00:20:55.759> examples<00:20:56.149> in<00:20:56.240> agreeance<00:20:56.509> so<00:20:57.440> I<00:20:57.470> showed 00:20:57.930 --> 00:20:57.940 align:start position:0% other examples in agreeance so I showed 00:20:57.940 --> 00:21:00.279 align:start position:0% other examples in agreeance so I showed up<00:20:58.940> good<00:20:59.149> from<00:20:59.299> the<00:20:59.360> fighters<00:20:59.750> so<00:20:59.899> that's<00:21:00.110> of 00:21:00.279 --> 00:21:00.289 align:start position:0% up good from the fighters so that's of 00:21:00.289 --> 00:21:02.169 align:start position:0% up good from the fighters so that's of course<00:21:00.590> I<00:21:00.889> had<00:21:01.340> to<00:21:01.370> change<00:21:01.909> something 00:21:02.169 --> 00:21:02.179 align:start position:0% course I had to change something 00:21:02.179 --> 00:21:03.700 align:start position:0% course I had to change something internally<00:21:02.659> to<00:21:02.809> build<00:21:03.110> that<00:21:03.259> stuff<00:21:03.500> that's 00:21:03.700 --> 00:21:03.710 align:start position:0% internally to build that stuff that's 00:21:03.710 --> 00:21:06.070 align:start position:0% internally to build that stuff that's not<00:21:03.919> supposed<00:21:04.190> to<00:21:04.309> show<00:21:04.580> all<00:21:05.389> bad<00:21:05.629> Dell<00:21:05.870> ways 00:21:06.070 --> 00:21:06.080 align:start position:0% not supposed to show all bad Dell ways 00:21:06.080 --> 00:21:09.639 align:start position:0% not supposed to show all bad Dell ways it's<00:21:06.470> has<00:21:06.919> to<00:21:07.070> be<00:21:07.299> nicer<00:21:08.299> better<00:21:08.990> usability<00:21:09.259> in 00:21:09.639 --> 00:21:09.649 align:start position:0% it's has to be nicer better usability in 00:21:09.649 --> 00:21:12.399 align:start position:0% it's has to be nicer better usability in terms<00:21:09.950> of<00:21:10.220> right<00:21:11.179> now<00:21:11.360> dealing<00:21:11.690> way<00:21:11.929> to<00:21:12.259> use 00:21:12.399 --> 00:21:12.409 align:start position:0% terms of right now dealing way to use 00:21:12.409 --> 00:21:14.440 align:start position:0% terms of right now dealing way to use this<00:21:12.500> empty<00:21:12.679> checkers<00:21:13.039> actually<00:21:13.429> go<00:21:14.120> finally 00:21:14.440 --> 00:21:14.450 align:start position:0% this empty checkers actually go finally 00:21:14.450 --> 00:21:17.610 align:start position:0% this empty checkers actually go finally to<00:21:14.480> go<00:21:14.690> pilot<00:21:15.019> yourself<00:21:15.409> with<00:21:15.799> c3<00:21:16.519> or<00:21:16.820> CVC<00:21:17.299> for 00:21:17.610 --> 00:21:17.620 align:start position:0% to go pilot yourself with c3 or CVC for 00:21:17.620 --> 00:21:21.369 align:start position:0% to go pilot yourself with c3 or CVC for linked<00:21:18.620> to<00:21:18.950> it<00:21:19.100> but<00:21:19.549> we<00:21:19.970> are<00:21:20.120> working<00:21:20.509> on<00:21:20.809> have 00:21:21.369 --> 00:21:21.379 align:start position:0% linked to it but we are working on have 00:21:21.379 --> 00:21:24.159 align:start position:0% linked to it but we are working on have an<00:21:21.500> enabled<00:21:22.009> biases<00:21:22.429> ajs<00:21:22.820> and<00:21:23.149> the<00:21:23.840> just<00:21:24.049> read 00:21:24.159 --> 00:21:24.169 align:start position:0% an enabled biases ajs and the just read 00:21:24.169 --> 00:21:26.019 align:start position:0% an enabled biases ajs and the just read version<00:21:24.559> which<00:21:24.980> I<00:21:25.129> guess<00:21:25.279> what<00:21:25.580> most<00:21:25.730> people 00:21:26.019 --> 00:21:26.029 align:start position:0% version which I guess what most people 00:21:26.029 --> 00:21:29.100 align:start position:0% version which I guess what most people use<00:21:26.059> by<00:21:26.480> in<00:21:26.629> the<00:21:26.809> quite<00:21:27.769> a<00:21:27.799> few<00:21:28.159> families<00:21:28.580> and 00:21:29.100 --> 00:21:29.110 align:start position:0% use by in the quite a few families and 00:21:29.110 --> 00:21:31.840 align:start position:0% use by in the quite a few families and where<00:21:30.110> we<00:21:30.440> are<00:21:30.470> also<00:21:30.889> working<00:21:31.250> with<00:21:31.429> other 00:21:31.840 --> 00:21:31.850 align:start position:0% where we are also working with other 00:21:31.850 --> 00:21:34.299 align:start position:0% where we are also working with other people<00:21:32.779> from<00:21:32.960> consistent<00:21:33.679> certification<00:21:34.220> and 00:21:34.299 --> 00:21:34.309 align:start position:0% people from consistent certification and 00:21:34.309 --> 00:21:36.340 align:start position:0% people from consistent certification and other<00:21:34.399> projects<00:21:34.879> on<00:21:35.240> creating<00:21:35.929> a<00:21:36.019> very<00:21:36.259> very 00:21:36.340 --> 00:21:36.350 align:start position:0% other projects on creating a very very 00:21:36.350 --> 00:21:39.129 align:start position:0% other projects on creating a very very simple<00:21:37.570> specification<00:21:38.570> landform 00:21:39.129 --> 00:21:39.139 align:start position:0% simple specification landform 00:21:39.139 --> 00:21:41.080 align:start position:0% simple specification landform specification<00:21:39.710> language<00:21:40.070> and<00:21:40.399> we<00:21:40.730> welcome 00:21:41.080 --> 00:21:41.090 align:start position:0% specification language and we welcome 00:21:41.090 --> 00:21:43.710 align:start position:0% specification language and we welcome anyone<00:21:41.389> ever<00:21:42.320> wanted<00:21:42.830> to<00:21:42.860> be<00:21:43.159> part<00:21:43.429> of 00:21:43.710 --> 00:21:43.720 align:start position:0% anyone ever wanted to be part of 00:21:43.720 --> 00:21:46.330 align:start position:0% anyone ever wanted to be part of creating<00:21:44.720> this<00:21:44.929> language<00:21:45.320> its<00:21:45.769> we<00:21:46.220> are 00:21:46.330 --> 00:21:46.340 align:start position:0% creating this language its we are 00:21:46.340 --> 00:21:48.399 align:start position:0% creating this language its we are discussing<00:21:46.700> things<00:21:47.059> in<00:21:47.240> this<00:21:47.330> rainbow<00:21:47.690> so 00:21:48.399 --> 00:21:48.409 align:start position:0% discussing things in this rainbow so 00:21:48.409 --> 00:21:52.840 align:start position:0% discussing things in this rainbow so feel<00:21:48.590> free<00:21:48.620> to<00:21:48.769> come<00:21:49.370> in<00:21:49.519> and<00:21:50.110> give<00:21:51.110> ideas<00:21:51.850> so 00:21:52.840 --> 00:21:52.850 align:start position:0% feel free to come in and give ideas so 00:21:52.850 --> 00:21:56.110 align:start position:0% feel free to come in and give ideas so finally<00:21:53.299> to<00:21:54.080> conclude<00:21:54.379> my<00:21:54.710> talk<00:21:54.919> so<00:21:55.460> CT 00:21:56.110 --> 00:21:56.120 align:start position:0% finally to conclude my talk so CT 00:21:56.120 --> 00:21:57.909 align:start position:0% finally to conclude my talk so CT solvers<00:21:56.480> are<00:21:56.690> very<00:21:57.200> broke<00:21:57.440> with<00:21:57.679> and<00:21:57.889> very 00:21:57.909 --> 00:21:57.919 align:start position:0% solvers are very broke with and very 00:21:57.919 --> 00:22:01.389 align:start position:0% solvers are very broke with and very fast<00:21:58.340> at<00:21:58.610> least<00:21:58.850> we<00:21:59.120> try<00:22:00.019> to<00:22:00.049> sell<00:22:00.950> them<00:22:01.129> that 00:22:01.389 --> 00:22:01.399 align:start position:0% fast at least we try to sell them that 00:22:01.399 --> 00:22:04.720 align:start position:0% fast at least we try to sell them that way<00:22:02.529> eventually<00:22:03.529> those<00:22:03.799> Tapia 00:22:04.720 --> 00:22:04.730 align:start position:0% way eventually those Tapia 00:22:04.730 --> 00:22:07.780 align:start position:0% way eventually those Tapia because<00:22:05.090> they<00:22:05.210> tried<00:22:05.480> too<00:22:05.810> hard<00:22:06.790> the 00:22:07.780 --> 00:22:07.790 align:start position:0% because they tried too hard the 00:22:07.790 --> 00:22:09.550 align:start position:0% because they tried too hard the technique<00:22:08.090> we<00:22:08.210> use<00:22:08.330> here<00:22:08.600> is<00:22:08.690> PDR<00:22:09.080> it's<00:22:09.470> an 00:22:09.550 --> 00:22:09.560 align:start position:0% technique we use here is PDR it's an 00:22:09.560 --> 00:22:11.920 align:start position:0% technique we use here is PDR it's an unbonded<00:22:09.890> model<00:22:10.250> second<00:22:10.520> technique<00:22:10.790> to<00:22:11.630> solve 00:22:11.920 --> 00:22:11.930 align:start position:0% unbonded model second technique to solve 00:22:11.930 --> 00:22:14.440 align:start position:0% unbonded model second technique to solve the<00:22:12.770> word<00:22:12.980> implies<00:22:13.190> that<00:22:13.430> model<00:22:13.820> our<00:22:14.030> control 00:22:14.440 --> 00:22:14.450 align:start position:0% the word implies that model our control 00:22:14.450 --> 00:22:17.440 align:start position:0% the word implies that model our control flow<00:22:14.600> graph<00:22:14.780> and<00:22:15.340> the<00:22:16.340> goal<00:22:16.550> we<00:22:16.820> have<00:22:17.030> here<00:22:17.300> is 00:22:17.440 --> 00:22:17.450 align:start position:0% flow graph and the goal we have here is 00:22:17.450 --> 00:22:19.930 align:start position:0% flow graph and the goal we have here is to<00:22:17.600> prove<00:22:17.810> that<00:22:18.430> safety<00:22:19.430> properties<00:22:19.820> are 00:22:19.930 --> 00:22:19.940 align:start position:0% to prove that safety properties are 00:22:19.940 --> 00:22:21.970 align:start position:0% to prove that safety properties are sound<00:22:20.180> even<00:22:20.480> under<00:22:20.630> consider<00:22:20.960> an<00:22:21.200> unbounded 00:22:21.970 --> 00:22:21.980 align:start position:0% sound even under consider an unbounded 00:22:21.980 --> 00:22:27.160 align:start position:0% sound even under consider an unbounded number<00:22:22.100> of<00:22:23.560> of<00:22:24.560> transactions<00:22:25.160> this<00:22:26.150> is<00:22:26.330> all<00:22:26.480> in 00:22:27.160 --> 00:22:27.170 align:start position:0% number of of transactions this is all in 00:22:27.170 --> 00:22:29.080 align:start position:0% number of of transactions this is all in the<00:22:27.260> cylindrical<00:22:27.470> whether<00:22:27.890> you<00:22:28.340> get<00:22:28.520> it<00:22:28.640> for 00:22:29.080 --> 00:22:29.090 align:start position:0% the cylindrical whether you get it for 00:22:29.090 --> 00:22:30.940 align:start position:0% the cylindrical whether you get it for free<00:22:29.210> simply<00:22:30.140> by<00:22:30.290> using<00:22:30.350> the<00:22:30.560> pregnant 00:22:30.940 --> 00:22:30.950 align:start position:0% free simply by using the pregnant 00:22:30.950 --> 00:22:32.680 align:start position:0% free simply by using the pregnant experimental<00:22:31.520> sneaky<00:22:31.730> checker<00:22:31.940> what<00:22:32.510> I<00:22:32.540> need 00:22:32.680 --> 00:22:32.690 align:start position:0% experimental sneaky checker what I need 00:22:32.690 --> 00:22:34.510 align:start position:0% experimental sneaky checker what I need to<00:22:32.780> have<00:22:32.900> assertions<00:22:33.350> takes<00:22:34.010> a<00:22:34.100> property 00:22:34.510 --> 00:22:34.520 align:start position:0% to have assertions takes a property 00:22:34.520 --> 00:22:36.460 align:start position:0% to have assertions takes a property direct<00:22:34.910> admission<00:22:35.120> ability<00:22:35.570> as<00:22:36.080> addition<00:22:36.410> to 00:22:36.460 --> 00:22:36.470 align:start position:0% direct admission ability as addition to 00:22:36.470 --> 00:22:37.990 align:start position:0% direct admission ability as addition to force<00:22:36.710> it<00:22:36.890> needs<00:22:36.920> to<00:22:37.340> have<00:22:37.430> a<00:22:37.460> property<00:22:37.880> to 00:22:37.990 --> 00:22:38.000 align:start position:0% force it needs to have a property to 00:22:38.000 --> 00:22:39.910 align:start position:0% force it needs to have a property to verify<00:22:38.420> it's<00:22:38.900> not<00:22:39.020> going<00:22:39.170> to<00:22:39.230> tell<00:22:39.350> you<00:22:39.590> random 00:22:39.910 --> 00:22:39.920 align:start position:0% verify it's not going to tell you random 00:22:39.920 --> 00:22:41.920 align:start position:0% verify it's not going to tell you random things<00:22:40.190> just<00:22:41.000> out<00:22:41.150> of<00:22:41.180> the<00:22:41.330> code<00:22:41.510> itself<00:22:41.870> I 00:22:41.920 --> 00:22:41.930 align:start position:0% things just out of the code itself I 00:22:41.930 --> 00:22:44.290 align:start position:0% things just out of the code itself I need<00:22:42.080> to<00:22:42.230> have<00:22:42.380> estates<00:22:42.710> the<00:22:42.830> properties<00:22:43.220> in<00:22:44.150> a 00:22:44.290 --> 00:22:44.300 align:start position:0% need to have estates the properties in a 00:22:44.300 --> 00:22:49.240 align:start position:0% need to have estates the properties in a permit<00:22:45.160> and<00:22:46.160> finally<00:22:47.620> the<00:22:48.620> contract<00:22:49.040> in<00:22:49.130> the 00:22:49.240 --> 00:22:49.250 align:start position:0% permit and finally the contract in the 00:22:49.250 --> 00:22:50.770 align:start position:0% permit and finally the contract in the three<00:22:49.460> variants<00:22:49.880> that<00:22:49.940> we<00:22:50.150> generate<00:22:50.570> and 00:22:50.770 --> 00:22:50.780 align:start position:0% three variants that we generate and 00:22:50.780 --> 00:22:53.230 align:start position:0% three variants that we generate and would<00:22:51.050> output<00:22:51.500> from<00:22:52.280> the<00:22:52.430> compiler<00:22:52.760> can<00:22:52.970> also 00:22:53.230 --> 00:22:53.240 align:start position:0% would output from the compiler can also 00:22:53.240 --> 00:22:55.630 align:start position:0% would output from the compiler can also help<00:22:53.630> verification<00:22:54.470> of<00:22:54.500> bytecode<00:22:55.010> afterwards 00:22:55.630 --> 00:22:55.640 align:start position:0% help verification of bytecode afterwards 00:22:55.640 --> 00:23:18.529 align:start position:0% help verification of bytecode afterwards which<00:22:59.620> everyone 00:23:18.529 --> 00:23:18.539 align:start position:0% 00:23:18.539 --> 00:23:22.049 align:start position:0% all<00:23:19.539> the<00:23:19.690> asserted<00:23:20.169> sworn<00:23:20.710> or<00:23:21.130> also<00:23:21.639> requires 00:23:22.049 --> 00:23:22.059 align:start position:0% all the asserted sworn or also requires 00:23:22.059 --> 00:23:24.659 align:start position:0% all the asserted sworn or also requires the<00:23:22.840> answer<00:23:23.049> requires<00:23:23.409> are<00:23:23.830> used<00:23:24.460> as 00:23:24.659 --> 00:23:24.669 align:start position:0% the answer requires are used as 00:23:24.669 --> 00:23:32.669 align:start position:0% the answer requires are used as assumptions<00:23:30.510> so<00:23:31.510> right<00:23:31.659> now<00:23:31.809> this<00:23:32.019> works<00:23:32.529> at 00:23:32.669 --> 00:23:32.679 align:start position:0% assumptions so right now this works at 00:23:32.679 --> 00:23:41.460 align:start position:0% assumptions so right now this works at the<00:23:32.799> level<00:23:33.100> of<00:23:33.220> a<00:23:33.340> single<00:23:36.000> track<00:23:40.470> successfully 00:23:41.460 --> 00:23:41.470 align:start position:0% the level of a single track successfully 00:23:41.470 --> 00:23:45.000 align:start position:0% the level of a single track successfully what<00:23:42.250> assertions<00:23:42.789> in<00:23:43.000> that<00:23:43.740> point<00:23:44.740> we<00:23:44.830> have<00:23:44.950> a 00:23:45.000 --> 00:23:45.010 align:start position:0% what assertions in that point we have a 00:23:45.010 --> 00:23:47.250 align:start position:0% what assertions in that point we have a searching<00:23:45.340> the<00:23:45.460> first<00:23:45.700> contract<00:23:46.139> and<00:23:47.139> are 00:23:47.250 --> 00:23:47.260 align:start position:0% searching the first contract and are 00:23:47.260 --> 00:23:49.560 align:start position:0% searching the first contract and are calling<00:23:47.529> a<00:23:47.649> second<00:23:47.980> contract<00:23:48.309> the<00:23:49.210> difference 00:23:49.560 --> 00:23:49.570 align:start position:0% calling a second contract the difference 00:23:49.570 --> 00:23:50.700 align:start position:0% calling a second contract the difference is<00:23:49.659> that<00:23:49.690> the<00:23:49.870> psychical<00:23:50.230> check<00:23:50.440> point<00:23:50.649> two 00:23:50.700 --> 00:23:50.710 align:start position:0% is that the psychical check point two 00:23:50.710 --> 00:23:52.919 align:start position:0% is that the psychical check point two things<00:23:51.100> you're<00:23:51.279> not<00:23:51.539> really<00:23:52.539> I<00:23:52.570> don't<00:23:52.779> really 00:23:52.919 --> 00:23:52.929 align:start position:0% things you're not really I don't really 00:23:52.929 --> 00:23:55.259 align:start position:0% things you're not really I don't really know<00:23:53.080> what<00:23:53.200> it's<00:23:53.289> doing<00:23:53.639> or<00:23:54.639> sometimes<00:23:54.970> you<00:23:55.090> do 00:23:55.259 --> 00:23:55.269 align:start position:0% know what it's doing or sometimes you do 00:23:55.269 --> 00:23:57.659 align:start position:0% know what it's doing or sometimes you do and<00:23:55.600> there<00:23:56.559> might<00:23:56.740> be<00:23:56.769> a<00:23:56.919> reaction<00:23:57.130> see<00:23:57.429> things 00:23:57.659 --> 00:23:57.669 align:start position:0% and there might be a reaction see things 00:23:57.669 --> 00:23:59.759 align:start position:0% and there might be a reaction see things that<00:23:57.970> changes<00:23:58.299> the<00:23:58.419> state<00:23:58.630> of<00:23:58.690> the<00:23:59.500> first 00:23:59.759 --> 00:23:59.769 align:start position:0% that changes the state of the first 00:23:59.769 --> 00:24:01.409 align:start position:0% that changes the state of the first contract<00:24:00.250> and<00:24:00.460> then<00:24:00.730> would<00:24:00.909> affect<00:24:01.240> the 00:24:01.409 --> 00:24:01.419 align:start position:0% contract and then would affect the 00:24:01.419 --> 00:24:02.250 align:start position:0% contract and then would affect the property<00:24:01.750> that<00:24:01.840> you<00:24:01.929> want<00:24:02.049> to<00:24:02.110> prove 00:24:02.250 --> 00:24:02.260 align:start position:0% property that you want to prove 00:24:02.260 --> 00:24:07.049 align:start position:0% property that you want to prove afterwards<00:24:03.240> so<00:24:04.740> yeah<00:24:05.740> this<00:24:05.950> is<00:24:06.010> how<00:24:06.700> you<00:24:06.760> can 00:24:07.049 --> 00:24:07.059 align:start position:0% afterwards so yeah this is how you can 00:24:07.059 --> 00:24:10.190 align:start position:0% afterwards so yeah this is how you can change<00:24:07.590> work<00:24:08.590> by<00:24:08.710> now<00:24:08.860> it's<00:24:09.070> mostly 00:24:10.190 --> 00:24:10.200 align:start position:0% change work by now it's mostly 00:24:10.200 --> 00:24:26.090 align:start position:0% change work by now it's mostly implementation<00:24:11.200> effort<00:24:11.789> just 00:24:26.090 --> 00:24:26.100 align:start position:0% 00:24:26.100 --> 00:24:33.170 align:start position:0% [Applause] 00:24:33.170 --> 00:24:33.180 align:start position:0% 00:24:33.180 --> 00:24:35.240 align:start position:0% you