-
Notifications
You must be signed in to change notification settings - Fork 26
/
Copy pathZen.thy
3319 lines (2866 loc) · 262 KB
/
Zen.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
section \<open>Safety Properties\<close>
text \<open>This section describes the invariants that hold in the system, shows that the implementation
preserves the invariants, and shows that the invariants imply the required safety properties.\<close>
theory Zen
imports Implementation OneSlot
begin
subsection \<open>Invariants on messages\<close>
text \<open>Firstly, a set of invariants that hold on the set of messages that
have ever been sent, without considering the state of any individual
node.\<close>
fun nat_inductive_def :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
where
"nat_inductive_def zeroCase sucCase 0 = zeroCase"
| "nat_inductive_def zeroCase sucCase (Suc i) = sucCase i (nat_inductive_def zeroCase sucCase i)"
locale zenMessages =
fixes messages :: "RoutedMessage set"
fixes isMessageFromTo :: "Node \<Rightarrow> Message \<Rightarrow> Destination \<Rightarrow> bool" ("(_) \<midarrow>\<langle> _ \<rangle>\<rightarrow> (_)" [1000,55,1000])
defines "s \<midarrow>\<langle> m \<rangle>\<rightarrow> d \<equiv> \<lparr> sender = s, destination = d, payload = m \<rparr> \<in> messages"
fixes isMessageFrom :: "Node \<Rightarrow> Message \<Rightarrow> bool" ("(_) \<midarrow>\<langle> _ \<rangle>\<leadsto>" [1000,55])
defines "s \<midarrow>\<langle> m \<rangle>\<leadsto> \<equiv> \<exists> d. s \<midarrow>\<langle> m \<rangle>\<rightarrow> d"
fixes isMessageTo :: "Message \<Rightarrow> Destination \<Rightarrow> bool" ("\<langle> _ \<rangle>\<rightarrow> (_)" [55,1000])
defines "\<langle> m \<rangle>\<rightarrow> d \<equiv> \<exists> s. s \<midarrow>\<langle> m \<rangle>\<rightarrow> d"
fixes isMessage :: "Message \<Rightarrow> bool" ("\<langle> _ \<rangle>\<leadsto>" [55])
defines "\<langle> m \<rangle>\<leadsto> \<equiv> \<exists> s. s \<midarrow>\<langle> m \<rangle>\<leadsto>"
(* value proposed in a slot & a term *)
fixes v :: "Slot \<Rightarrow> Term \<Rightarrow> Value"
defines "v i t \<equiv> THE x. \<langle> PublishRequest i t x \<rangle>\<leadsto>"
(* whether a slot is committed *)
fixes isCommitted :: "Slot \<Rightarrow> bool"
defines "isCommitted i \<equiv> \<exists> t. \<langle> ApplyCommit i t \<rangle>\<leadsto>"
(* whether all preceding slots are committed *)
fixes committedTo :: "Slot \<Rightarrow> bool" ("committed\<^sub><")
defines "committed\<^sub>< i \<equiv> \<forall> j < i. isCommitted j"
(* the committed value in a slot *)
fixes v\<^sub>c :: "Slot \<Rightarrow> Value"
defines "v\<^sub>c i \<equiv> v i (SOME t. \<langle> ApplyCommit i t \<rangle>\<leadsto>)"
(* the configuration of a slot *)
fixes V :: "Slot \<Rightarrow> Node set"
defines "V \<equiv> nat_inductive_def V\<^sub>0 (\<lambda>i Vi. if isReconfiguration (v\<^sub>c i) then getConf (v\<^sub>c i) else Vi)"
(* predicate to say whether an applicable Vote has been sent *)
fixes promised :: "Slot \<Rightarrow> Node \<Rightarrow> Node \<Rightarrow> Term \<Rightarrow> bool"
defines "promised i s dn t \<equiv> \<exists> i' \<le> i. \<exists> a. s \<midarrow>\<langle> Vote i' t a \<rangle>\<rightarrow> (OneNode dn)"
(* set of previously-accepted terms *)
fixes prevAccepted :: "Slot \<Rightarrow> Term \<Rightarrow> Node set \<Rightarrow> Term set"
defines "prevAccepted i t senders
\<equiv> {t'. \<exists> s \<in> senders. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> }"
fixes lastCommittedClusterStateBefore :: "Slot \<Rightarrow> ClusterState"
defines "lastCommittedClusterStateBefore \<equiv> nat_inductive_def CS\<^sub>0
(\<lambda>i CSi. case v\<^sub>c i of ClusterStateDiff diff \<Rightarrow> diff CSi | _ \<Rightarrow> CSi)"
(* ASSUMPTIONS *)
assumes Vote_future:
"\<And>i i' s t t' a.
\<lbrakk> s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>; i < i'; t' < t \<rbrakk>
\<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i' t' \<rangle>\<leadsto>"
assumes Vote_None:
"\<And>i s t t'.
\<lbrakk> s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto>; t' < t \<rbrakk>
\<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>"
assumes Vote_Some_lt:
"\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>
\<Longrightarrow> t' < t"
assumes Vote_Some_PublishResponse:
"\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>
\<Longrightarrow> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>"
assumes Vote_Some_max:
"\<And>i s t t' t''. \<lbrakk> s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>; t' < t''; t'' < t \<rbrakk>
\<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t'' \<rangle>\<leadsto>"
assumes Vote_not_broadcast:
"\<And>i t a d. \<langle> Vote i t a \<rangle>\<rightarrow> d \<Longrightarrow> d \<noteq> Broadcast"
assumes Vote_unique_destination:
"\<And>i s t a a' d d'. \<lbrakk> s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow> d; s \<midarrow>\<langle> Vote i' t a' \<rangle>\<rightarrow> d' \<rbrakk>
\<Longrightarrow> d = d'"
assumes PublishRequest_committedTo:
"\<And>i t x. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> committedTo i"
assumes PublishRequest_quorum:
"\<And>i s t x. s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>
\<Longrightarrow> \<exists> q \<in> majorities (V i). (\<forall> n \<in> q. promised i n s t) \<and>
(prevAccepted i t q = {}
\<or> (\<exists> t'. v i t = v i t' \<and> maxTerm (prevAccepted i t q) \<le> t'
\<and> \<langle> PublishResponse i t' \<rangle>\<leadsto> \<and> t' < t))"
assumes PublishRequest_function:
"\<And>i t x x'. \<lbrakk> \<langle> PublishRequest i t x \<rangle>\<leadsto>; \<langle> PublishRequest i t x' \<rangle>\<leadsto> \<rbrakk>
\<Longrightarrow> x = x'"
assumes finite_messages:
"finite messages"
assumes PublishResponse_PublishRequest:
"\<And>i s t. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto> \<Longrightarrow> \<exists> x. \<langle> PublishRequest i t x \<rangle>\<leadsto>"
assumes ApplyCommit_quorum:
"\<And>i t. \<langle> ApplyCommit i t \<rangle>\<leadsto>
\<Longrightarrow> \<exists> q \<in> majorities (V i). \<forall> s \<in> q. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>"
assumes CatchUpResponse_committedTo:
"\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i"
assumes CatchUpResponse_V:
"\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> V i = conf"
assumes CatchUpResponse_lastCommittedClusterStateBefore:
"\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> lastCommittedClusterStateBefore i = cs"
definition (in zenMessages) votedFor :: "Node \<Rightarrow> Node \<Rightarrow> Term \<Rightarrow> bool"
where "votedFor n\<^sub>1 n\<^sub>2 t \<equiv> \<exists> i. promised i n\<^sub>1 n\<^sub>2 t"
lemma (in zenMessages) votedFor_unique:
assumes "votedFor n n\<^sub>1 t"
assumes "votedFor n n\<^sub>2 t"
shows "n\<^sub>1 = n\<^sub>2"
using assms unfolding votedFor_def by (meson Destination.inject Vote_unique_destination promised_def)
lemma (in zenMessages) V_simps[simp]:
"V 0 = V\<^sub>0"
"V (Suc i) = (if isReconfiguration (v\<^sub>c i) then getConf (v\<^sub>c i) else V i)"
unfolding V_def by simp_all
lemma (in zenMessages) lastCommittedClusterStateBefore_simps[simp]:
"lastCommittedClusterStateBefore 0 = CS\<^sub>0"
"lastCommittedClusterStateBefore (Suc i) = (case v\<^sub>c i of ClusterStateDiff diff \<Rightarrow> diff | _ \<Rightarrow> id) (lastCommittedClusterStateBefore i)"
unfolding lastCommittedClusterStateBefore_def by (simp, cases "v\<^sub>c i", auto)
declare [[goals_limit = 40]]
subsubsection \<open>Utility lemmas\<close>
text \<open>Some results that are useful later:\<close>
lemma (in zenMessages) V_finite: "finite (V i)"
by (induct i, simp_all add: finite_V\<^sub>0 getConf_finite)
lemma (in zenMessages) V_intersects: "majorities (V i) \<frown> majorities (V i)"
using V_finite majorities_intersect by simp
lemma (in zenMessages) ApplyCommit_PublishResponse:
assumes "\<langle> ApplyCommit i t \<rangle>\<leadsto>"
obtains s where "s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>"
by (meson ApplyCommit_quorum majorities_member assms)
lemma (in zenMessages) ApplyCommit_PublishRequest:
assumes "\<langle> ApplyCommit i t \<rangle>\<leadsto>"
shows "\<langle> PublishRequest i t (v i t) \<rangle>\<leadsto>"
by (metis ApplyCommit_PublishResponse PublishResponse_PublishRequest assms the_equality v_def PublishRequest_function)
lemma (in zenMessages) PublishRequest_Vote:
assumes "s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>"
obtains i' n a where "i' \<le> i" "n \<midarrow>\<langle> Vote i' t a \<rangle>\<rightarrow> (OneNode s)"
by (meson PublishRequest_quorum majorities_member assms isMessage_def promised_def)
lemma (in zenMessages) finite_prevAccepted: "finite (prevAccepted i t ns)"
proof -
fix t\<^sub>0
define f :: "RoutedMessage \<Rightarrow> Term" where "f \<equiv> \<lambda> m. case payload m of Vote _ _ (SomeTerm t') \<Rightarrow> t' | _ \<Rightarrow> t\<^sub>0"
have "prevAccepted i t ns \<subseteq> f ` messages"
apply (simp add: prevAccepted_def f_def isMessageFrom_def isMessageFromTo_def, intro subsetI)
using image_iff by fastforce
with finite_messages show ?thesis using finite_surj by auto
qed
lemma (in zenMessages) promised_long_def: "\<exists>d. promised i s d t
\<equiv> (s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto>
\<or> (\<exists>i'<i. \<exists>a. s \<midarrow>\<langle> Vote i' t a \<rangle>\<leadsto>))
\<or> (\<exists>t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>)"
(is "?LHS == ?RHS")
proof -
have "?LHS = ?RHS"
apply (intro iffI)
apply (metis TermOption.exhaust isMessageFrom_def nat_less_le promised_def)
by (metis Destination.exhaust Vote_not_broadcast isMessageFrom_def isMessageTo_def nat_less_le not_le promised_def)
thus "?LHS == ?RHS" by simp
qed
lemma (in zenMessages) Vote_value_function:
assumes "s \<midarrow>\<langle> Vote i t a\<^sub>1 \<rangle>\<leadsto>" and "s \<midarrow>\<langle> Vote i t a\<^sub>2 \<rangle>\<leadsto>"
shows "a\<^sub>1 = a\<^sub>2"
proof (cases a\<^sub>1)
case NO_TERM
with assms show ?thesis
by (metis TermOption.exhaust Vote_None Vote_Some_PublishResponse Vote_Some_lt)
next
case (SomeTerm t\<^sub>1)
with assms obtain t\<^sub>2 where a\<^sub>2: "a\<^sub>2 = SomeTerm t\<^sub>2"
using Vote_None Vote_Some_PublishResponse Vote_Some_lt TermOption.exhaust by metis
from SomeTerm a\<^sub>2 assms show ?thesis
by (metis Vote_Some_PublishResponse Vote_Some_lt less_linear Vote_Some_max)
qed
lemma (in zenMessages) shows finite_messages_insert: "finite (insert m messages)"
using finite_messages by auto
lemma (in zenMessages) isCommitted_committedTo:
assumes "isCommitted i"
shows "committed\<^sub>< i"
using ApplyCommit_PublishRequest PublishRequest_committedTo assms isCommitted_def by blast
lemma (in zenMessages) isCommitted_committedTo_Suc:
assumes "isCommitted i"
shows "committed\<^sub>< (Suc i)"
using assms committedTo_def isCommitted_committedTo less_antisym by blast
lemma (in zenMessages) promised_unique:
assumes "promised i s d t" and "promised i' s d' t"
shows "d = d'"
by (meson Destination.inject Vote_unique_destination assms promised_def)
lemma (in zenMessages) PublishResponse_PublishRequest_v:
assumes "\<langle> PublishResponse i t \<rangle>\<leadsto>"
shows "\<langle> PublishRequest i t (v i t) \<rangle>\<leadsto>"
proof -
from assms obtain s where "s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>" unfolding isMessage_def by blast
with PublishResponse_PublishRequest
obtain x where x: "\<langle> PublishRequest i t x \<rangle>\<leadsto>" by blast
have "v i t = x" unfolding v_def using x by (intro the_equality PublishRequest_function)
with x show ?thesis by simp
qed
lemma (in zenMessages) Vote_PublishRequest_v:
assumes "\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>"
shows "\<langle> PublishRequest i t' (v i t') \<rangle>\<leadsto>"
using assms Vote_Some_PublishResponse PublishResponse_PublishRequest_v
unfolding isMessage_def by metis
subsubsection \<open>Relationship to @{term oneSlot}\<close>
text \<open>This shows that each slot @{term i} in Zen satisfies the assumptions of the @{term
oneSlot} model above.\<close>
lemma (in zenMessages) zen_is_oneSlot:
fixes i
shows "oneSlot (majorities (V i)) (v i)
(\<lambda> s t. s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto>
\<or> (\<exists> i' < i. \<exists> a. s \<midarrow>\<langle> Vote i' t a \<rangle>\<leadsto>))
(\<lambda> s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>)
(\<lambda> t. \<exists> x. \<langle> PublishRequest i t x \<rangle>\<leadsto>)
(\<lambda> s t. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>)
(\<lambda> t. \<langle> ApplyCommit i t \<rangle>\<leadsto>)"
proof (unfold_locales, fold prevAccepted_def promised_long_def)
from V_intersects show "majorities (V i) \<frown> majorities (V i)".
next
fix s t t'
assume "t' < t" "s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto> \<or> (\<exists>i'<i. \<exists>a. s \<midarrow>\<langle> Vote i' t a \<rangle>\<leadsto>)"
thus "\<not> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>"
using Vote_None Vote_future by auto
next
fix s t t'
assume j: "s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>"
from j show "t' < t" using Vote_Some_lt by blast
from j show "s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>" using Vote_Some_PublishResponse by blast
fix t'' assume "t' < t''" "t'' < t"
with j show "\<not> s \<midarrow>\<langle> PublishResponse i t'' \<rangle>\<leadsto>" using Vote_Some_max by blast
next
fix t
assume "\<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>"
then obtain x s where "s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>" by (auto simp add: isMessage_def)
from PublishRequest_quorum [OF this] PublishResponse_PublishRequest
show "\<exists>q \<in> majorities (V i). (\<forall>n\<in>q. \<exists>d. promised i n d t) \<and> (prevAccepted i t q = {} \<or> (\<exists>t'. v i t = v i t' \<and> maxTerm (prevAccepted i t q) \<le> t' \<and> (\<exists>x. \<langle> PublishRequest i t' x \<rangle>\<leadsto>) \<and> t' < t))"
unfolding isMessageFrom_def by (meson PublishResponse_PublishRequest_v)
next
fix s t assume "s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>"
thus "\<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>"
by (simp add: PublishResponse_PublishRequest)
next
fix t assume "\<langle> ApplyCommit i t \<rangle>\<leadsto>"
thus "\<exists>q \<in> majorities (V i). \<forall>s\<in>q. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>"
by (simp add: ApplyCommit_quorum)
next
fix t\<^sub>0
define f :: "RoutedMessage \<Rightarrow> Term"
where "f \<equiv> \<lambda> m. case payload m of PublishRequest i t x \<Rightarrow> t | _ \<Rightarrow> t\<^sub>0"
have "{t. \<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>} \<subseteq> f ` messages"
apply (unfold isMessage_def isMessageFrom_def isMessageFromTo_def)
using f_def image_iff by fastforce
moreover have "finite (f ` messages)"
by (simp add: finite_messages)
ultimately show "finite {t. \<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>}"
using finite_subset by blast
qed
text \<open>From this it follows that all committed values are equal.\<close>
theorem (in zenMessages) consistent:
assumes "\<langle> ApplyCommit i t\<^sub>1 \<rangle>\<leadsto>"
assumes "\<langle> ApplyCommit i t\<^sub>2 \<rangle>\<leadsto>"
assumes "\<langle> PublishRequest i t\<^sub>1 v\<^sub>1 \<rangle>\<leadsto>"
assumes "\<langle> PublishRequest i t\<^sub>2 v\<^sub>2 \<rangle>\<leadsto>"
shows "v\<^sub>1 = v\<^sub>2"
proof -
from oneSlot.consistent [OF zen_is_oneSlot] assms
have "v i t\<^sub>1 = v i t\<^sub>2" by blast
moreover have "v\<^sub>1 = v i t\<^sub>1" using ApplyCommit_PublishRequest assms PublishRequest_function by blast
moreover have "v\<^sub>2 = v i t\<^sub>2" using ApplyCommit_PublishRequest assms PublishRequest_function by blast
ultimately show ?thesis by simp
qed
lemma (in zenMessages) ApplyCommit_v\<^sub>c:
assumes "\<langle> ApplyCommit i t \<rangle>\<leadsto>"
shows "v\<^sub>c i = v i t"
proof (unfold v\<^sub>c_def, intro someI2 [where Q = "\<lambda>t'. v i t' = v i t"])
from assms show "\<langle> ApplyCommit i t \<rangle>\<leadsto>" .
fix t' assume "\<langle> ApplyCommit i t' \<rangle>\<leadsto>"
thus "v i t' = v i t" by (intro oneSlot.consistent [OF zen_is_oneSlot] assms)
qed
lemma (in zenMessages) ApplyCommit_PublishRequest_v\<^sub>c:
assumes "\<langle> ApplyCommit i t \<rangle>\<leadsto>"
shows "\<langle> PublishRequest i t (v\<^sub>c i) \<rangle>\<leadsto>"
unfolding ApplyCommit_v\<^sub>c [OF assms]
using ApplyCommit_PublishRequest assms .
subsection \<open>Invariants on node states\<close>
text \<open>A set of invariants which relate the states of the individual nodes to the set of messages sent.\<close>
locale zen = zenMessages +
fixes nodeState :: "Node \<Rightarrow> NodeData"
assumes currentNode_nodeState: "\<And>n. currentNode (nodeState n) = n"
assumes committedTo_firstUncommittedSlot:
"\<And>n. committed\<^sub>< (firstUncommittedSlot (nodeState n))"
assumes currentVotingNodes_firstUncommittedSlot:
"\<And>n. currentVotingNodes (nodeState n) = V (firstUncommittedSlot (nodeState n))"
assumes firstUncommittedSlot_PublishRequest:
"\<And>i n t x. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>"
assumes firstUncommittedSlot_PublishResponse:
"\<And>i n t. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>"
assumes lastAcceptedTerm_None: "\<And>n t. lastAcceptedTerm (nodeState n) = NO_TERM
\<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>"
assumes lastAcceptedTerm_Some_sent: "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t
\<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>"
assumes lastAcceptedTerm_Some_max: "\<And>n t t'. lastAcceptedTerm (nodeState n) = SomeTerm t
\<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t' \<rangle>\<leadsto>
\<Longrightarrow> t' \<le> t"
assumes lastAcceptedTerm_Some_currentTerm: "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t
\<Longrightarrow> t \<le> currentTerm (nodeState n)"
assumes lastAcceptedTerm_Some_value: "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t
\<Longrightarrow> \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t (lastAcceptedValue (nodeState n)) \<rangle>\<leadsto>"
assumes Vote_currentTerm:
"\<And>n i t a. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState n)"
assumes Vote_slot_function:
"\<And>n i i' t a a'. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> n \<midarrow>\<langle> Vote i' t a' \<rangle>\<leadsto> \<Longrightarrow> i = i'"
assumes PublishRequest_currentTerm:
"\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto>
\<Longrightarrow> t \<le> currentTerm (nodeState n)"
assumes PublishRequest_publishPermitted_currentTerm:
"\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto>
\<Longrightarrow> publishPermitted (nodeState n)
\<Longrightarrow> t < currentTerm (nodeState n)"
assumes joinVotes:
"\<And> n n'. n' \<in> joinVotes (nodeState n)
\<Longrightarrow> promised (firstUncommittedSlot (nodeState n)) n' n (currentTerm (nodeState n))"
assumes electionWon_isQuorum:
"\<And>n. electionWon (nodeState n) \<Longrightarrow> isQuorum (nodeState n) (joinVotes (nodeState n))"
assumes joinVotes_max: "\<And>n n' a'.
\<lbrakk> \<not> (\<exists> x. \<langle> PublishRequest (firstUncommittedSlot (nodeState n))
(currentTerm (nodeState n)) x \<rangle>\<leadsto>);
n' \<in> joinVotes (nodeState n);
n' \<midarrow>\<langle> Vote (firstUncommittedSlot (nodeState n))
(currentTerm (nodeState n))
a' \<rangle>\<rightarrow> (OneNode n) \<rbrakk>
\<Longrightarrow> a' \<le> lastAcceptedTerm (nodeState n)"
assumes publishVotes: "\<And>n n'. n' \<in> publishVotes (nodeState n)
\<Longrightarrow> n' \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n))
(currentTerm (nodeState n)) \<rangle>\<leadsto>"
assumes currentClusterState_lastCommittedClusterStateBefore:
"\<And>n. currentClusterState (nodeState n)
= lastCommittedClusterStateBefore (firstUncommittedSlot (nodeState n))"
lemma (in zen) joinVotes_votedFor:
assumes "n' \<in> joinVotes (nodeState n)"
shows "votedFor n' n (currentTerm (nodeState n))"
using joinVotes assms unfolding votedFor_def by auto
locale zenStep = zen +
fixes messages' :: "RoutedMessage set"
fixes nodeState' :: "Node \<Rightarrow> NodeData"
fixes n\<^sub>0 :: Node
assumes messages_subset: "messages \<subseteq> messages'"
fixes nd :: NodeData
defines "nd \<equiv> nodeState n\<^sub>0"
fixes nd' :: NodeData
defines "nd' \<equiv> nodeState' n\<^sub>0"
assumes nodeState_unchanged: "\<And>n. n \<noteq> n\<^sub>0 \<Longrightarrow> nodeState' n = nodeState n"
(* updated definitions from zenMessages *)
fixes isMessageFromTo' :: "Node \<Rightarrow> Message \<Rightarrow> Destination \<Rightarrow> bool" ("(_) \<midarrow>\<langle> _ \<rangle>\<rightarrow>' (_)" [1000,55,1000])
defines "s \<midarrow>\<langle> m \<rangle>\<rightarrow>' d \<equiv> \<lparr> sender = s, destination = d, payload = m \<rparr> \<in> messages'"
fixes isMessageFrom' :: "Node \<Rightarrow> Message \<Rightarrow> bool" ("(_) \<midarrow>\<langle> _ \<rangle>\<leadsto>'" [1000,55])
defines "s \<midarrow>\<langle> m \<rangle>\<leadsto>' \<equiv> \<exists> d. s \<midarrow>\<langle> m \<rangle>\<rightarrow>' d"
fixes isMessageTo' :: "Message \<Rightarrow> Destination \<Rightarrow> bool" ("\<langle> _ \<rangle>\<rightarrow>' (_)" [55,1000])
defines "\<langle> m \<rangle>\<rightarrow>' d \<equiv> \<exists> s. s \<midarrow>\<langle> m \<rangle>\<rightarrow>' d"
fixes isMessage' :: "Message \<Rightarrow> bool" ("\<langle> _ \<rangle>\<leadsto>'" [55])
defines "\<langle> m \<rangle>\<leadsto>' \<equiv> \<exists> s. s \<midarrow>\<langle> m \<rangle>\<leadsto>'"
(* value proposed in a slot & a term *)
fixes v' :: "nat \<Rightarrow> Term \<Rightarrow> Value"
defines "v' i t \<equiv> THE x. \<langle> PublishRequest i t x \<rangle>\<leadsto>'"
(* whether a slot is committed *)
fixes isCommitted' :: "nat \<Rightarrow> bool"
defines "isCommitted' i \<equiv> \<exists> t. \<langle> ApplyCommit i t \<rangle>\<leadsto>'"
(* whether all preceding slots are committed *)
fixes committedTo' :: "nat \<Rightarrow> bool" ("committed\<^sub><'")
defines "committed\<^sub><' i \<equiv> \<forall> j < i. isCommitted' j"
(* the committed value in a slot *)
fixes v\<^sub>c' :: "nat \<Rightarrow> Value"
defines "v\<^sub>c' i \<equiv> v' i (SOME t. \<langle> ApplyCommit i t \<rangle>\<leadsto>')"
(* the configuration of a slot *)
fixes V' :: "Slot \<Rightarrow> Node set"
defines "V' \<equiv> nat_inductive_def V\<^sub>0 (\<lambda>i Vi. if isReconfiguration (v\<^sub>c' i) then getConf (v\<^sub>c' i) else Vi)"
(* predicate to say whether an applicable Vote has been sent *)
fixes promised' :: "nat \<Rightarrow> Node \<Rightarrow> Node \<Rightarrow> Term \<Rightarrow> bool"
defines "promised' i s dn t \<equiv> \<exists> i' \<le> i. \<exists> a. s \<midarrow>\<langle> Vote i' t a \<rangle>\<rightarrow>' (OneNode dn)"
(* set of previously-accepted terms *)
fixes prevAccepted' :: "nat \<Rightarrow> Term \<Rightarrow> Node set \<Rightarrow> Term set"
defines "prevAccepted' i t senders
\<equiv> {t'. \<exists> s \<in> senders. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>' }"
fixes lastCommittedClusterStateBefore' :: "nat \<Rightarrow> ClusterState"
defines "lastCommittedClusterStateBefore' \<equiv> nat_inductive_def CS\<^sub>0
(\<lambda>i CSi. case v\<^sub>c' i of ClusterStateDiff diff \<Rightarrow> diff CSi | _ \<Rightarrow> CSi)"
fixes sendTo :: "Destination \<Rightarrow> (NodeData * Message option) \<Rightarrow> RoutedMessage set"
defines "sendTo d result \<equiv> case snd result of
None \<Rightarrow> messages | Some m \<Rightarrow> insert \<lparr> sender = n\<^sub>0, destination = d, payload = m \<rparr> messages"
lemma (in zenStep) nodeState'_def: "nodeState' n \<equiv> if n = n\<^sub>0 then nd' else nodeState n"
using nodeState_unchanged nd'_def by presburger
lemma (in zenStep) V'_simps[simp]:
"V' 0 = V\<^sub>0"
"V' (Suc i) = (if isReconfiguration (v\<^sub>c' i) then getConf (v\<^sub>c' i) else V' i)"
unfolding V'_def by simp_all
lemma (in zenStep) lastCommittedClusterStateBefore'_simps[simp]:
"lastCommittedClusterStateBefore' 0 = CS\<^sub>0"
"lastCommittedClusterStateBefore' (Suc i) = (case v\<^sub>c' i of ClusterStateDiff diff \<Rightarrow> diff | _ \<Rightarrow> id) (lastCommittedClusterStateBefore' i)"
unfolding lastCommittedClusterStateBefore'_def by (simp, cases "v\<^sub>c' i", auto)
lemma (in zenStep) sendTo_simps[simp]:
"sendTo d (nd'', None) = messages"
"sendTo d (nd'', Some m) = insert \<lparr> sender = n\<^sub>0, destination = d, payload = m \<rparr> messages"
by (auto simp add: sendTo_def)
lemma currentTerm_ensureCurrentTerm[simp]: "currentTerm nd \<le> t \<Longrightarrow> currentTerm (ensureCurrentTerm t nd) = t"
by (auto simp add: ensureCurrentTerm_def)
lemma (in zenStep)
assumes "\<And>i i' s t t' a. s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>' \<Longrightarrow> i < i' \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i' t' \<rangle>\<leadsto>'"
assumes "\<And>i s t t'. s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto>' \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>'"
assumes "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>' \<Longrightarrow> t' < t"
assumes "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>' \<Longrightarrow> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>'"
assumes "\<And>i s t t' t''. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>' \<Longrightarrow> t' < t'' \<Longrightarrow> t'' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t'' \<rangle>\<leadsto>'"
assumes "\<And>i t a d. \<langle> Vote i t a \<rangle>\<rightarrow>' d \<Longrightarrow> d \<noteq> Broadcast"
assumes "\<And>i' i s t a a' d d'. s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow>' d \<Longrightarrow> s \<midarrow>\<langle> Vote i' t a' \<rangle>\<rightarrow>' d' \<Longrightarrow> d = d'"
assumes "\<And>i t x. \<langle> PublishRequest i t x \<rangle>\<leadsto>' \<Longrightarrow> committed\<^sub><' i"
assumes "\<And>i s t x. s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>' \<Longrightarrow> \<exists>q\<in>majorities (V' i). (\<forall>n\<in>q. promised' i n s t) \<and> (prevAccepted' i t q = {} \<or> (\<exists>t'. v' i t = v' i t' \<and> maxTerm (prevAccepted' i t q) \<le> t' \<and> \<langle> PublishResponse i t' \<rangle>\<leadsto>' \<and> t' < t))"
assumes "\<And>i t x x'. \<langle> PublishRequest i t x \<rangle>\<leadsto>' \<Longrightarrow> \<langle> PublishRequest i t x' \<rangle>\<leadsto>' \<Longrightarrow> x = x'"
assumes "finite messages'"
assumes "\<And>i s t. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>' \<Longrightarrow> \<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>'"
assumes "\<And>i t. \<langle> ApplyCommit i t \<rangle>\<leadsto>' \<Longrightarrow> \<exists>q\<in>majorities (V' i). \<forall>s\<in>q. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>'"
assumes "\<And>n. currentNode (nodeState' n) = n"
assumes "\<And>n. committed\<^sub><' (firstUncommittedSlot (nodeState' n))"
assumes "\<And>n. currentVotingNodes (nodeState' n) = V' (firstUncommittedSlot (nodeState' n))"
assumes "\<And>i n t x. firstUncommittedSlot (nodeState' n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>'"
assumes "\<And>i n t. firstUncommittedSlot (nodeState' n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>'"
assumes "\<And>n t. lastAcceptedTerm (nodeState' n) = NO_TERM \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState' n)) t \<rangle>\<leadsto>'"
assumes "\<And>n t. lastAcceptedTerm (nodeState' n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState' n)) t \<rangle>\<leadsto>'"
assumes "\<And>n t t'. lastAcceptedTerm (nodeState' n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState' n)) t' \<rangle>\<leadsto>' \<Longrightarrow> t' \<le> t"
assumes "\<And>n t. lastAcceptedTerm (nodeState' n) = SomeTerm t \<Longrightarrow> \<langle> PublishRequest (firstUncommittedSlot (nodeState' n)) t (lastAcceptedValue (nodeState' n)) \<rangle>\<leadsto>'"
assumes "\<And>n t. lastAcceptedTerm (nodeState' n) = SomeTerm t \<Longrightarrow> t \<le> currentTerm (nodeState' n)"
assumes "\<And>n i t a. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>' \<Longrightarrow> t \<le> currentTerm (nodeState' n)"
assumes "\<And>n i i' t a a'. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>' \<Longrightarrow> n \<midarrow>\<langle> Vote i' t a' \<rangle>\<leadsto>' \<Longrightarrow> i = i'"
assumes "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState' n)) t x \<rangle>\<leadsto>' \<Longrightarrow> t \<le> currentTerm (nodeState' n)"
assumes "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState' n)) t x \<rangle>\<leadsto>' \<Longrightarrow> publishPermitted (nodeState' n) \<Longrightarrow> t < currentTerm (nodeState' n)"
assumes "\<And>n n'. n' \<in> joinVotes (nodeState' n) \<Longrightarrow> promised' (firstUncommittedSlot (nodeState' n)) n' n (currentTerm (nodeState' n))"
assumes "\<And>n. electionWon (nodeState' n) \<Longrightarrow> isQuorum (nodeState' n) (joinVotes (nodeState' n))"
assumes "\<And>n n' a'. \<not> (\<exists>x. \<langle> PublishRequest (firstUncommittedSlot (nodeState' n)) (currentTerm (nodeState' n)) x \<rangle>\<leadsto>') \<Longrightarrow> n' \<in> joinVotes (nodeState' n) \<Longrightarrow> n' \<midarrow>\<langle> Vote (firstUncommittedSlot (nodeState' n)) (currentTerm (nodeState' n)) a' \<rangle>\<rightarrow>' (OneNode n) \<Longrightarrow> a' \<le> lastAcceptedTerm (nodeState' n)"
assumes "\<And>n n'. n' \<in> publishVotes (nodeState' n) \<Longrightarrow> n' \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState' n)) (currentTerm (nodeState' n)) \<rangle>\<leadsto>'"
assumes "\<And>n. currentClusterState (nodeState' n) = lastCommittedClusterStateBefore' (firstUncommittedSlot (nodeState' n))"
assumes "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>' \<Longrightarrow> committed\<^sub><' i"
assumes "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>' \<Longrightarrow> V' i = conf"
assumes "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>' \<Longrightarrow> lastCommittedClusterStateBefore' i = cs"
shows zenI: "zen messages' nodeState'"
apply (unfold_locales)
apply (fold isMessageFromTo'_def)
apply (fold isMessageTo'_def)
apply (fold isMessageFrom'_def)
apply (fold isMessage'_def)
apply (fold v'_def)
apply (fold isCommitted'_def)
apply (fold committedTo'_def)
apply (fold v\<^sub>c'_def)
apply (fold V'_def)
apply (fold promised'_def)
apply (fold prevAccepted'_def)
apply (fold lastCommittedClusterStateBefore'_def)
using assms proof - qed
lemma (in zenStep)
assumes "zen messages' nodeState'" "messages' \<subseteq> messages''" "\<And>n. n \<noteq> n\<^sub>0 \<Longrightarrow> nodeState' n = nodeState'' n"
shows zenStepI1: "zenStep messages' nodeState' messages'' nodeState'' n\<^sub>0"
proof (intro_locales)
from `zen messages' nodeState'`
show "zenMessages messages'" "zen_axioms messages' nodeState'"
unfolding zen_def by simp_all
from assms
show "zenStep_axioms messages' nodeState' messages'' nodeState'' n\<^sub>0"
by (intro zenStep_axioms.intro, auto)
qed
lemma (in zenStep)
assumes "messages \<subseteq> messages''" "\<And>n. n \<noteq> n\<^sub>0 \<Longrightarrow> nodeState n = nodeState'' n"
shows zenStepI2: "zenStep messages nodeState messages'' nodeState'' n\<^sub>0"
proof (intro_locales)
from assms
show "zenStep_axioms messages nodeState messages'' nodeState'' n\<^sub>0"
by (intro zenStep_axioms.intro, auto)
qed
lemma (in zenStep) Broadcast_to_OneNode:
fixes x
assumes nodeState': "nodeState' = nodeState"
assumes sent: "n\<^sub>0 \<midarrow>\<langle> m \<rangle>\<rightarrow> Broadcast"
assumes messages': "messages' = sendTo (OneNode d) (nd'', Some m)"
shows "zen messages' nodeState'"
proof -
have messages': "messages' = insert \<lparr>sender = n\<^sub>0, destination = OneNode d, payload = m \<rparr> messages"
by (simp add: messages')
from Vote_not_broadcast sent have not_Vote: "\<And>i t a. m \<noteq> Vote i t a"
unfolding isMessageTo_def by blast
from sent not_Vote have message_simps:
"\<And>s m'. (s \<midarrow>\<langle> m' \<rangle>\<leadsto>') = (s \<midarrow>\<langle> m' \<rangle>\<leadsto>)"
"\<And>m'. (\<langle> m' \<rangle>\<leadsto>') = (\<langle> m' \<rangle>\<leadsto>)"
"\<And>s d i t a. (s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow> d)"
"\<And>d i t a. (\<langle> Vote i t a \<rangle>\<rightarrow>' d) = (\<langle> Vote i t a \<rangle>\<rightarrow> d)"
by (auto simp add: isMessageFromTo'_def isMessageTo'_def isMessage'_def isMessageFrom'_def,
auto simp add: isMessageFromTo_def isMessageTo_def isMessage_def isMessageFrom_def messages')
have property_simps[simp]:
"\<And>n. currentNode (nodeState' n) = currentNode (nodeState n)"
"\<And>n. firstUncommittedSlot (nodeState' n) = firstUncommittedSlot (nodeState n)"
"\<And>n. currentVotingNodes (nodeState' n) = currentVotingNodes (nodeState n)"
"\<And>n q. isQuorum (nodeState' n) q = isQuorum (nodeState n) q"
"\<And>n. currentTerm (nodeState' n) = currentTerm (nodeState n)"
"\<And>n. publishPermitted (nodeState' n) = publishPermitted (nodeState n)"
"\<And>n. joinVotes (nodeState' n) = joinVotes (nodeState n)"
"\<And>n. electionWon (nodeState' n) = electionWon (nodeState n)"
"\<And>n. publishVotes (nodeState' n) = publishVotes (nodeState n)"
"\<And>n. currentClusterState (nodeState' n) = currentClusterState (nodeState n)"
"\<And>n. lastAcceptedTerm (nodeState' n) = lastAcceptedTerm (nodeState n)"
"\<And>n. lastAcceptedValue (nodeState' n) = lastAcceptedValue (nodeState n)"
by (unfold nodeState', auto)
have v_eq[simp]: "v' = v" by (intro ext, auto simp add: v'_def v_def message_simps)
have v\<^sub>c_eq[simp]: "v\<^sub>c' = v\<^sub>c" by (intro ext, auto simp add: v\<^sub>c'_def v\<^sub>c_def message_simps)
have isCommitted_eq[simp]: "isCommitted' = isCommitted" by (intro ext, auto simp add: isCommitted'_def isCommitted_def message_simps)
have committedTo_eq[simp]: "committed\<^sub><' = committed\<^sub><" by (intro ext, auto simp add: committedTo'_def committedTo_def)
have V_eq[simp]: "V' = V" using v\<^sub>c_eq V'_def V_def by blast
have lastCommittedClusterStateBefore_eq[simp]: "lastCommittedClusterStateBefore' = lastCommittedClusterStateBefore"
unfolding lastCommittedClusterStateBefore_def lastCommittedClusterStateBefore'_def v\<^sub>c_eq ..
have promised_eq[simp]: "promised' = promised" by (intro ext, auto simp add: promised'_def promised_def message_simps)
have prevAccepted_eq[simp]: "prevAccepted' = prevAccepted" by (intro ext, auto simp add: prevAccepted'_def prevAccepted_def message_simps)
show ?thesis
apply (intro zenI)
apply (unfold message_simps committedTo_eq V_eq v_eq
lastCommittedClusterStateBefore_eq property_simps promised_eq prevAccepted_eq)
proof -
from finite_messages show "finite messages'" by (simp add: messages')
from Vote_future show "\<And>i i' s t t' a. s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> i < i' \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i' t' \<rangle>\<leadsto>".
from Vote_None show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto> \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>".
from Vote_Some_lt show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> t' < t".
from Vote_Some_PublishResponse show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>".
from Vote_Some_max show "\<And>i s t t' t''. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> t' < t'' \<Longrightarrow> t'' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t'' \<rangle>\<leadsto>".
from Vote_not_broadcast show "\<And>i t a d. \<langle> Vote i t a \<rangle>\<rightarrow> d \<Longrightarrow> d \<noteq> Broadcast".
from Vote_unique_destination show "\<And>i' i s t a a' d d'. s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow> d \<Longrightarrow> s \<midarrow>\<langle> Vote i' t a' \<rangle>\<rightarrow> d' \<Longrightarrow> d = d'".
from currentNode_nodeState show "\<And>n. currentNode (nodeState n) = n" .
from committedTo_firstUncommittedSlot show "\<And>n. committed\<^sub>< (firstUncommittedSlot (nodeState n))" .
from firstUncommittedSlot_PublishResponse show "\<And>n i t. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>" .
from lastAcceptedTerm_None show "\<And>n i t. lastAcceptedTerm (nodeState n) = NO_TERM \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_sent show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_max show "\<And>n t t'. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t' \<rangle>\<leadsto> \<Longrightarrow> t' \<le> t".
from Vote_currentTerm show "\<And>n i t a. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState n)".
from Vote_slot_function show "\<And>n i i' t a a'. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> n \<midarrow>\<langle> Vote i' t a' \<rangle>\<leadsto> \<Longrightarrow> i = i'".
from electionWon_isQuorum show "\<And>n. electionWon (nodeState n) \<Longrightarrow> isQuorum (nodeState n) (joinVotes (nodeState n))".
from joinVotes_max show " \<And>n n' a'. \<not> (\<exists>x. \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) x \<rangle>\<leadsto>) \<Longrightarrow> n' \<in> joinVotes (nodeState n) \<Longrightarrow> n' \<midarrow>\<langle> Vote (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) a' \<rangle>\<rightarrow> (OneNode n) \<Longrightarrow> a' \<le> lastAcceptedTerm (nodeState n)".
from publishVotes show "\<And>n n'. n' \<in> publishVotes (nodeState n) \<Longrightarrow> n' \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) \<rangle>\<leadsto>".
from currentClusterState_lastCommittedClusterStateBefore show "\<And>n. currentClusterState (nodeState n) = lastCommittedClusterStateBefore (firstUncommittedSlot (nodeState n))".
from joinVotes show "\<And>n n'. n' \<in> joinVotes (nodeState n) \<Longrightarrow> promised (firstUncommittedSlot (nodeState n)) n' n (currentTerm (nodeState n))".
from PublishRequest_committedTo show "\<And>i t x. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from PublishRequest_quorum show "\<And>i s t x. s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> \<exists>q\<in>majorities (V i). (\<forall>n\<in>q. promised i n s t) \<and> (prevAccepted i t q = {} \<or> (\<exists>t'. v i t = v i t' \<and> maxTerm (prevAccepted i t q) \<le> t' \<and> \<langle> PublishResponse i t' \<rangle>\<leadsto> \<and> t' < t))".
from PublishRequest_function show "\<And>i t x x'. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> \<langle> PublishRequest i t x' \<rangle>\<leadsto> \<Longrightarrow> x = x'".
from PublishResponse_PublishRequest show "\<And>i s t. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>".
from ApplyCommit_quorum show "\<And>i t. \<langle> ApplyCommit i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>q\<in>majorities (V i). \<forall>s\<in>q. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>".
from currentVotingNodes_firstUncommittedSlot show "\<And>n. currentVotingNodes (nodeState n) = V (firstUncommittedSlot (nodeState n))".
from firstUncommittedSlot_PublishRequest show "\<And>i n t x. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_value show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t (lastAcceptedValue (nodeState n)) \<rangle>\<leadsto>".
from PublishRequest_currentTerm show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState n)".
from PublishRequest_publishPermitted_currentTerm show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> publishPermitted (nodeState n) \<Longrightarrow> t < currentTerm (nodeState n)".
from CatchUpResponse_committedTo show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from CatchUpResponse_V show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> V i = conf".
from CatchUpResponse_lastCommittedClusterStateBefore show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> lastCommittedClusterStateBefore i = cs".
from lastAcceptedTerm_Some_currentTerm show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> t \<le> currentTerm (nodeState n)".
qed
qed
lemma (in zenStep) send_spontaneous_message:
assumes messages': "messages' = sendTo d\<^sub>0 (nd, Some m)"
assumes spontaneous: "case m of StartJoin _ \<Rightarrow> True | ClientValue _ \<Rightarrow> True | Reboot \<Rightarrow> True | CatchUpRequest \<Rightarrow> True | _ \<Rightarrow> False"
assumes nodeState': "nodeState' = nodeState"
shows "zen messages' nodeState'"
proof -
have messages': "messages' = insert \<lparr>sender = n\<^sub>0, destination = d\<^sub>0, payload = m \<rparr> messages"
by (simp add: messages')
from spontaneous
have message_simps[simp]:
"\<And>s d i t a. (s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow> d)"
"\<And>s d i t. (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<rightarrow> d)"
"\<And>s d i t x. (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<rightarrow> d)"
"\<And>s d i t. (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<rightarrow> d)"
"\<And>d i t a. (\<langle> Vote i t a \<rangle>\<rightarrow>' d) = (\<langle> Vote i t a \<rangle>\<rightarrow> d)"
"\<And>d i t. (\<langle> PublishResponse i t \<rangle>\<rightarrow>' d) = (\<langle> PublishResponse i t \<rangle>\<rightarrow> d)"
"\<And>d i t x. (\<langle> PublishRequest i t x \<rangle>\<rightarrow>' d) = (\<langle> PublishRequest i t x \<rangle>\<rightarrow> d)"
"\<And>d i t. (\<langle> ApplyCommit i t \<rangle>\<rightarrow>' d) = (\<langle> ApplyCommit i t \<rangle>\<rightarrow> d)"
"\<And>s i t a. (s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>') = (s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>)"
"\<And>s i t. (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>') = (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>)"
"\<And>s i t x. (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>') = (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>)"
"\<And>s i t. (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<leadsto>') = (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<leadsto>)"
"\<And>d i t a. (\<langle> Vote i t a \<rangle>\<leadsto>') = (\<langle> Vote i t a \<rangle>\<leadsto>)"
"\<And>d i t. (\<langle> PublishResponse i t \<rangle>\<leadsto>') = (\<langle> PublishResponse i t \<rangle>\<leadsto>)"
"\<And>d i t x. (\<langle> PublishRequest i t x \<rangle>\<leadsto>') = (\<langle> PublishRequest i t x \<rangle>\<leadsto>)"
"\<And>d i t. (\<langle> ApplyCommit i t \<rangle>\<leadsto>') = (\<langle> ApplyCommit i t \<rangle>\<leadsto>)"
"\<And>s d i conf cs. (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow> d)"
"\<And>d i conf cs. (\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow>' d) = (\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow> d)"
"\<And>s i conf cs. (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>') = (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>)"
"\<And>d i conf cs. (\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>') = (\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>)"
by (auto simp add: isMessageFromTo'_def isMessageTo'_def isMessage'_def isMessageFrom'_def,
auto simp add: isMessageFromTo_def isMessageTo_def isMessage_def isMessageFrom_def messages')
have property_simps[simp]:
"\<And>n. currentNode (nodeState' n) = currentNode (nodeState n)"
"\<And>n. firstUncommittedSlot (nodeState' n) = firstUncommittedSlot (nodeState n)"
"\<And>n. currentVotingNodes (nodeState' n) = currentVotingNodes (nodeState n)"
"\<And>n q. isQuorum (nodeState' n) q = isQuorum (nodeState n) q"
"\<And>n. currentTerm (nodeState' n) = currentTerm (nodeState n)"
"\<And>n. publishPermitted (nodeState' n) = publishPermitted (nodeState n)"
"\<And>n. joinVotes (nodeState' n) = joinVotes (nodeState n)"
"\<And>n. electionWon (nodeState' n) = electionWon (nodeState n)"
"\<And>n. publishVotes (nodeState' n) = publishVotes (nodeState n)"
"\<And>n. currentClusterState (nodeState' n) = currentClusterState (nodeState n)"
"\<And>n. lastAcceptedTerm (nodeState' n) = lastAcceptedTerm (nodeState n)"
"\<And>n. lastAcceptedValue (nodeState' n) = lastAcceptedValue (nodeState n)"
by (unfold nodeState', auto)
have v_eq[simp]: "v' = v" by (intro ext, auto simp add: v'_def v_def)
have v\<^sub>c_eq[simp]: "v\<^sub>c' = v\<^sub>c" by (intro ext, auto simp add: v\<^sub>c'_def v\<^sub>c_def)
have isCommitted_eq[simp]: "isCommitted' = isCommitted" by (intro ext, auto simp add: isCommitted'_def isCommitted_def)
have committedTo_eq[simp]: "committed\<^sub><' = committed\<^sub><" by (intro ext, auto simp add: committedTo'_def committedTo_def)
have V_eq[simp]: "V' = V" using v\<^sub>c_eq V'_def V_def by blast
have lastCommittedClusterStateBefore_eq[simp]: "lastCommittedClusterStateBefore' = lastCommittedClusterStateBefore"
unfolding lastCommittedClusterStateBefore_def lastCommittedClusterStateBefore'_def v\<^sub>c_eq ..
have promised_eq[simp]: "promised' = promised" by (intro ext, auto simp add: promised'_def promised_def)
have prevAccepted_eq[simp]: "prevAccepted' = prevAccepted" by (intro ext, auto simp add: prevAccepted'_def prevAccepted_def)
show ?thesis
apply (intro zenI)
apply (unfold message_simps committedTo_eq V_eq v_eq
lastCommittedClusterStateBefore_eq property_simps promised_eq prevAccepted_eq)
proof -
from finite_messages show "finite messages'" by (simp add: messages')
from Vote_future show "\<And>i i' s t t' a. s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> i < i' \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i' t' \<rangle>\<leadsto>".
from Vote_None show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto> \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>".
from Vote_Some_lt show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> t' < t".
from Vote_Some_PublishResponse show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>".
from Vote_Some_max show "\<And>i s t t' t''. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> t' < t'' \<Longrightarrow> t'' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t'' \<rangle>\<leadsto>".
from Vote_not_broadcast show "\<And>i t a d. \<langle> Vote i t a \<rangle>\<rightarrow> d \<Longrightarrow> d \<noteq> Broadcast".
from Vote_unique_destination show "\<And>i' i s t a a' d d'. s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow> d \<Longrightarrow> s \<midarrow>\<langle> Vote i' t a' \<rangle>\<rightarrow> d' \<Longrightarrow> d = d'".
from currentNode_nodeState show "\<And>n. currentNode (nodeState n) = n" .
from committedTo_firstUncommittedSlot show "\<And>n. committed\<^sub>< (firstUncommittedSlot (nodeState n))" .
from firstUncommittedSlot_PublishResponse show "\<And>n i t. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>" .
from lastAcceptedTerm_None show "\<And>n i t. lastAcceptedTerm (nodeState n) = NO_TERM \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_sent show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_max show "\<And>n t t'. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t' \<rangle>\<leadsto> \<Longrightarrow> t' \<le> t".
from Vote_currentTerm show "\<And>n i t a. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState n)".
from Vote_slot_function show "\<And>n i i' t a a'. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> n \<midarrow>\<langle> Vote i' t a' \<rangle>\<leadsto> \<Longrightarrow> i = i'".
from electionWon_isQuorum show "\<And>n. electionWon (nodeState n) \<Longrightarrow> isQuorum (nodeState n) (joinVotes (nodeState n))".
from joinVotes_max show " \<And>n n' a'. \<not> (\<exists>x. \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) x \<rangle>\<leadsto>) \<Longrightarrow> n' \<in> joinVotes (nodeState n) \<Longrightarrow> n' \<midarrow>\<langle> Vote (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) a' \<rangle>\<rightarrow> (OneNode n) \<Longrightarrow> a' \<le> lastAcceptedTerm (nodeState n)".
from publishVotes show "\<And>n n'. n' \<in> publishVotes (nodeState n) \<Longrightarrow> n' \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) \<rangle>\<leadsto>".
from currentClusterState_lastCommittedClusterStateBefore show "\<And>n. currentClusterState (nodeState n) = lastCommittedClusterStateBefore (firstUncommittedSlot (nodeState n))".
from joinVotes show "\<And>n n'. n' \<in> joinVotes (nodeState n) \<Longrightarrow> promised (firstUncommittedSlot (nodeState n)) n' n (currentTerm (nodeState n))".
from PublishRequest_committedTo show "\<And>i t x. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from PublishRequest_quorum show "\<And>i s t x. s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> \<exists>q\<in>majorities (V i). (\<forall>n\<in>q. promised i n s t) \<and> (prevAccepted i t q = {} \<or> (\<exists>t'. v i t = v i t' \<and> maxTerm (prevAccepted i t q) \<le> t' \<and> \<langle> PublishResponse i t' \<rangle>\<leadsto> \<and> t' < t))".
from PublishRequest_function show "\<And>i t x x'. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> \<langle> PublishRequest i t x' \<rangle>\<leadsto> \<Longrightarrow> x = x'".
from PublishResponse_PublishRequest show "\<And>i s t. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>".
from ApplyCommit_quorum show "\<And>i t. \<langle> ApplyCommit i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>q\<in>majorities (V i). \<forall>s\<in>q. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>".
from currentVotingNodes_firstUncommittedSlot show "\<And>n. currentVotingNodes (nodeState n) = V (firstUncommittedSlot (nodeState n))".
from firstUncommittedSlot_PublishRequest show "\<And>i n t x. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_value show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t (lastAcceptedValue (nodeState n)) \<rangle>\<leadsto>".
from PublishRequest_currentTerm show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState n)".
from PublishRequest_publishPermitted_currentTerm show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> publishPermitted (nodeState n) \<Longrightarrow> t < currentTerm (nodeState n)".
from CatchUpResponse_committedTo show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from CatchUpResponse_V show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> V i = conf".
from CatchUpResponse_lastCommittedClusterStateBefore show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> lastCommittedClusterStateBefore i = cs".
from lastAcceptedTerm_Some_currentTerm show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> t \<le> currentTerm (nodeState n)".
qed
qed
lemma (in zenStep) send_StartJoin:
assumes messages': "messages' = sendTo d\<^sub>0 (nd, Some (StartJoin t\<^sub>0))"
assumes nodeState': "nodeState' = nodeState"
shows "zen messages' nodeState'"
using assms by (intro send_spontaneous_message, auto)
lemma (in zenStep) send_ClientValue:
assumes messages': "messages' = sendTo d\<^sub>0 (nd, Some (ClientValue x\<^sub>0))"
assumes nodeState': "nodeState' = nodeState"
shows "zen messages' nodeState'"
using assms by (intro send_spontaneous_message, auto)
lemma (in zenStep) send_CatchUpRequest:
assumes messages': "messages' = sendTo d\<^sub>0 (nd, Some CatchUpRequest)"
assumes nodeState': "nodeState' = nodeState"
shows "zen messages' nodeState'"
using assms by (intro send_spontaneous_message, auto)
lemma (in zenStep) send_Reboot:
assumes messages': "messages' = sendTo d\<^sub>0 (nd, Some Reboot)"
assumes nodeState': "nodeState' = nodeState"
shows "zen messages' nodeState'"
using assms by (intro send_spontaneous_message, auto)
lemma (in zenStep) ensureCurrentTerm_invariants:
assumes nd': "nd' = ensureCurrentTerm t nd"
assumes messages': "messages' = messages"
shows "zen messages' nodeState'"
proof (cases "t \<le> currentTerm nd")
case True
hence "nodeState' = nodeState"
by (intro ext, unfold nodeState'_def, auto simp add: nd' ensureCurrentTerm_def nd_def)
with zen_axioms messages' show ?thesis by simp
next
case False hence t: "currentTerm nd < t" by simp
have message_simps[simp]:
"\<And>s p d. (s \<midarrow>\<langle> p \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> p \<rangle>\<rightarrow> d)"
"\<And>p d. (\<langle> p \<rangle>\<rightarrow>' d) = (\<langle> p \<rangle>\<rightarrow> d)"
"\<And>s p. (s \<midarrow>\<langle> p \<rangle>\<leadsto>') = (s \<midarrow>\<langle> p \<rangle>\<leadsto>)"
"\<And>p. (\<langle> p \<rangle>\<leadsto>') = (\<langle> p \<rangle>\<leadsto>)"
by (unfold isMessageFromTo'_def isMessageTo'_def isMessageFrom'_def isMessage'_def,
auto simp add: messages' isMessageFromTo_def isMessageTo_def isMessageFrom_def isMessage_def)
have property_simps[simp]:
"\<And>n. currentNode (nodeState' n) = currentNode (nodeState n)"
"\<And>n. firstUncommittedSlot (nodeState' n) = firstUncommittedSlot (nodeState n)"
"\<And>n. currentClusterState (nodeState' n) = currentClusterState (nodeState n)"
"\<And>n. currentVotingNodes (nodeState' n) = currentVotingNodes (nodeState n)"
"\<And>n q. isQuorum (nodeState' n) q = isQuorum (nodeState n) q"
"\<And>n. lastAcceptedTerm (nodeState' n) = lastAcceptedTerm (nodeState n)"
"\<And>n. lastAcceptedValue (nodeState' n) = lastAcceptedValue (nodeState n)"
"currentTerm (nodeState' n\<^sub>0) = t"
"electionWon (nodeState' n\<^sub>0) = False"
"joinVotes (nodeState' n\<^sub>0) = {}"
"publishPermitted (nodeState' n\<^sub>0) = True"
"publishVotes (nodeState' n\<^sub>0) = {}"
using t
by (unfold nodeState'_def, auto simp add: nd_def isQuorum_def nd' ensureCurrentTerm_def
lastAcceptedTerm_def lastAcceptedValue_def)
have currentTerm_increases: "\<And>n. currentTerm (nodeState n) \<le> currentTerm (nodeState' n)"
using nd_def nodeState'_def property_simps t by auto
have v_eq[simp]: "v' = v" by (intro ext, auto simp add: v'_def v_def)
have v\<^sub>c_eq[simp]: "v\<^sub>c' = v\<^sub>c" by (intro ext, auto simp add: v\<^sub>c'_def v\<^sub>c_def)
have isCommitted_eq[simp]: "isCommitted' = isCommitted" by (intro ext, auto simp add: isCommitted'_def isCommitted_def)
have committedTo_eq[simp]: "committed\<^sub><' = committed\<^sub><" by (intro ext, auto simp add: committedTo'_def committedTo_def)
have V_eq[simp]: "V' = V" using v\<^sub>c_eq V'_def V_def by blast
have lastCommittedClusterStateBefore_eq[simp]: "lastCommittedClusterStateBefore' = lastCommittedClusterStateBefore"
unfolding lastCommittedClusterStateBefore_def lastCommittedClusterStateBefore'_def v\<^sub>c_eq ..
have promised_eq: "\<And>i n n' t. promised' i n n' t = promised i n n' t" by (simp add: promised_def promised'_def)
have prevAccepted_eq: "\<And>i t q. prevAccepted' i t q = prevAccepted i t q" by (simp add: prevAccepted_def prevAccepted'_def)
show ?thesis
apply (intro zenI)
apply (unfold message_simps committedTo_eq V_eq v_eq
lastCommittedClusterStateBefore_eq property_simps promised_eq prevAccepted_eq)
proof -
from finite_messages show "finite messages'" by (simp add: messages')
from Vote_future show "\<And>i i' s t t' a. s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> i < i' \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i' t' \<rangle>\<leadsto>".
from Vote_None show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto> \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>".
from Vote_Some_lt show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> t' < t".
from Vote_Some_PublishResponse show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>".
from Vote_Some_max show "\<And>i s t t' t''. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto> \<Longrightarrow> t' < t'' \<Longrightarrow> t'' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t'' \<rangle>\<leadsto>".
from Vote_not_broadcast show "\<And>i t a d. \<langle> Vote i t a \<rangle>\<rightarrow> d \<Longrightarrow> d \<noteq> Broadcast".
from Vote_unique_destination show "\<And>i' i s t a a' d d'. s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow> d \<Longrightarrow> s \<midarrow>\<langle> Vote i' t a' \<rangle>\<rightarrow> d' \<Longrightarrow> d = d'".
from currentNode_nodeState show "\<And>n. currentNode (nodeState n) = n" .
from committedTo_firstUncommittedSlot show "\<And>n. committed\<^sub>< (firstUncommittedSlot (nodeState n))" .
from firstUncommittedSlot_PublishResponse show "\<And>n i t. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>" .
from lastAcceptedTerm_None show "\<And>n i t. lastAcceptedTerm (nodeState n) = NO_TERM \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_sent show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_max show "\<And>n t t'. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t' \<rangle>\<leadsto> \<Longrightarrow> t' \<le> t".
from Vote_slot_function show "\<And>n i i' t a a'. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> n \<midarrow>\<langle> Vote i' t a' \<rangle>\<leadsto> \<Longrightarrow> i = i'".
from currentClusterState_lastCommittedClusterStateBefore show "\<And>n. currentClusterState (nodeState n) = lastCommittedClusterStateBefore (firstUncommittedSlot (nodeState n))".
from PublishRequest_committedTo show "\<And>i t x. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from PublishRequest_function show "\<And>i t x x'. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> \<langle> PublishRequest i t x' \<rangle>\<leadsto> \<Longrightarrow> x = x'".
from PublishResponse_PublishRequest show "\<And>i s t. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>".
from ApplyCommit_quorum show "\<And>i t. \<langle> ApplyCommit i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>q\<in>majorities (V i). \<forall>s\<in>q. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>".
from currentVotingNodes_firstUncommittedSlot show "\<And>n. currentVotingNodes (nodeState n) = V (firstUncommittedSlot (nodeState n))".
from firstUncommittedSlot_PublishRequest show "\<And>i n t x. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_value show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t (lastAcceptedValue (nodeState n)) \<rangle>\<leadsto>".
from PublishRequest_quorum show "\<And>i s t x. s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> \<exists>q\<in>majorities (V i). (\<forall>n\<in>q. promised i n s t) \<and> (prevAccepted i t q = {} \<or> (\<exists>t'. v i t = v i t' \<and> maxTerm (prevAccepted i t q) \<le> t' \<and> \<langle> PublishResponse i t' \<rangle>\<leadsto> \<and> t' < t))".
from CatchUpResponse_committedTo show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from CatchUpResponse_V show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> V i = conf".
from CatchUpResponse_lastCommittedClusterStateBefore show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> lastCommittedClusterStateBefore i = cs".
from Vote_currentTerm currentTerm_increases
show "\<And>n i t a. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState' n)"
using dual_order.trans by blast
from PublishRequest_publishPermitted_currentTerm currentTerm_increases property_simps
show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> publishPermitted (nodeState' n) \<Longrightarrow> t < currentTerm (nodeState' n)"
by (metis False PublishRequest_currentTerm dual_order.trans leI nd_def nodeState_unchanged)
from joinVotes
show "\<And>n n'. n' \<in> joinVotes (nodeState' n) \<Longrightarrow> promised (firstUncommittedSlot (nodeState n)) n' n (currentTerm (nodeState' n))"
unfolding nodeState'_def by (auto simp add: nd'_def)
from PublishRequest_currentTerm currentTerm_increases
show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState' n)"
using dual_order.trans by blast
from publishVotes
show "\<And>n n'. n' \<in> publishVotes (nodeState' n) \<Longrightarrow> n' \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState' n)) \<rangle>\<leadsto>"
unfolding nodeState'_def by (auto simp add: nd'_def)
from electionWon_isQuorum show "\<And>n. electionWon (nodeState' n) \<Longrightarrow> isQuorum (nodeState n) (joinVotes (nodeState' n))"
unfolding nodeState'_def by (auto simp add: nd'_def)
from lastAcceptedTerm_Some_currentTerm currentTerm_increases
show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> t \<le> currentTerm (nodeState' n)"
using dual_order.trans by blast
show "\<And>n n' a'. \<not> (\<exists>x. \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState' n)) x \<rangle>\<leadsto>) \<Longrightarrow> n' \<in> joinVotes (nodeState' n) \<Longrightarrow> n' \<midarrow>\<langle> Vote (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState' n)) a' \<rangle>\<rightarrow> (OneNode n) \<Longrightarrow> a' \<le> lastAcceptedTerm (nodeState n)"
by (metis ex_in_conv joinVotes_max nodeState_unchanged property_simps(10))
qed
qed
lemma (in zenStep) sendVote_invariants:
assumes messages': "messages' = sendTo (OneNode d\<^sub>0) (nd'',
Some (Vote (firstUncommittedSlot nd) (currentTerm nd) (lastAcceptedTerm nd)))"
assumes nd': "nd' = nd"
assumes not_sent: "\<And>i a. \<not> n\<^sub>0 \<midarrow>\<langle> Vote i (currentTerm nd) a \<rangle>\<leadsto>"
assumes not_accepted: "\<And>t'. lastAcceptedTerm nd = SomeTerm t' \<Longrightarrow> t' < currentTerm nd"
shows "zen messages' nodeState'"
proof -
have messages': "messages' = insert \<lparr>sender = n\<^sub>0, destination = OneNode d\<^sub>0,
payload = Vote (firstUncommittedSlot nd) (currentTerm nd) (lastAcceptedTerm nd)\<rparr> messages"
by (simp add: messages')
have nodeState'[simp]: "nodeState' = nodeState"
by (intro ext, auto simp add: nodeState'_def nd' nd_def)
have message_simps[simp]:
"\<And>s d i t. (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<rightarrow> d)"
"\<And>s d i t x. (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<rightarrow> d)"
"\<And>s d i t. (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<rightarrow> d)"
"\<And>d i t. (\<langle> ApplyCommit i t \<rangle>\<rightarrow>' d) = (\<langle> ApplyCommit i t \<rangle>\<rightarrow> d)"
"\<And>d i t x. (\<langle> PublishRequest i t x \<rangle>\<rightarrow>' d) = (\<langle> PublishRequest i t x \<rangle>\<rightarrow> d)"
"\<And>d i t. (\<langle> PublishResponse i t \<rangle>\<rightarrow>' d) = (\<langle> PublishResponse i t \<rangle>\<rightarrow> d)"
"\<And>s i t. (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<leadsto>') = (s \<midarrow>\<langle> ApplyCommit i t \<rangle>\<leadsto>)"
"\<And>s i t x. (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>') = (s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>)"
"\<And>s i t. (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>') = (s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>)"
"\<And>i t. (\<langle> ApplyCommit i t \<rangle>\<leadsto>') = (\<langle> ApplyCommit i t \<rangle>\<leadsto>)"
"\<And>i t x. (\<langle> PublishRequest i t x \<rangle>\<leadsto>') = (\<langle> PublishRequest i t x \<rangle>\<leadsto>)"
"\<And>i t. (\<langle> PublishResponse i t \<rangle>\<leadsto>') = (\<langle> PublishResponse i t \<rangle>\<leadsto>)"
"\<And>s d i conf cs. (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow>' d) = (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow> d)"
"\<And>d i conf cs. (\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow>' d) = (\<langle> CatchUpResponse i conf cs \<rangle>\<rightarrow> d)"
"\<And>s i conf cs. (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>') = (s \<midarrow>\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>)"
"\<And>d i conf cs. (\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>') = (\<langle> CatchUpResponse i conf cs \<rangle>\<leadsto>)"
by (unfold isMessageFromTo'_def isMessageTo'_def isMessageFrom'_def isMessage'_def,
auto simp add: messages' isMessageFromTo_def isMessageTo_def isMessageFrom_def isMessage_def)
have Vote':
"\<And>s d i t' a. (s \<midarrow>\<langle> Vote i t' a \<rangle>\<rightarrow>' d) =
((s \<midarrow>\<langle> Vote i t' a \<rangle>\<rightarrow> d)
\<or> (s, i, t', a, d) = (n\<^sub>0, firstUncommittedSlot nd, currentTerm nd, lastAcceptedTerm nd, OneNode d\<^sub>0))"
"\<And>d i t' a. (\<langle> Vote i t' a \<rangle>\<rightarrow>' d) =
((\<langle> Vote i t' a \<rangle>\<rightarrow> d)
\<or> (i, t', a, d) = (firstUncommittedSlot nd, currentTerm nd, lastAcceptedTerm nd, OneNode d\<^sub>0))"
"\<And>s i t' a. (s \<midarrow>\<langle> Vote i t' a \<rangle>\<leadsto>') =
((s \<midarrow>\<langle> Vote i t' a \<rangle>\<leadsto>)
\<or> (s, i, t', a) = (n\<^sub>0, firstUncommittedSlot nd, currentTerm nd, lastAcceptedTerm nd))"
"\<And>i t' a. (\<langle> Vote i t' a \<rangle>\<leadsto>') =
((\<langle> Vote i t' a \<rangle>\<leadsto>)
\<or> (i, t', a) = (firstUncommittedSlot nd, currentTerm nd, lastAcceptedTerm nd))"
by (unfold isMessageFromTo'_def isMessageFromTo_def isMessageTo'_def isMessageTo_def
isMessageFrom'_def isMessageFrom_def isMessage'_def isMessage_def, auto simp add: messages')
have v_eq[simp]: "v' = v" by (intro ext, auto simp add: v'_def v_def)
have v\<^sub>c_eq[simp]: "v\<^sub>c' = v\<^sub>c" by (intro ext, auto simp add: v\<^sub>c'_def v\<^sub>c_def)
have isCommitted_eq[simp]: "isCommitted' = isCommitted" by (intro ext, auto simp add: isCommitted'_def isCommitted_def)
have committedTo_eq[simp]: "committed\<^sub><' = committed\<^sub><" by (intro ext, auto simp add: committedTo'_def committedTo_def)
have V_eq[simp]: "V' = V" using v\<^sub>c_eq V'_def V_def by blast
have lastCommittedClusterStateBefore_eq[simp]: "lastCommittedClusterStateBefore' = lastCommittedClusterStateBefore"
unfolding lastCommittedClusterStateBefore_def lastCommittedClusterStateBefore'_def v\<^sub>c_eq ..
have promised_eq: "\<And>i s dn t. promised' i s dn t = (promised i s dn t \<or> (firstUncommittedSlot nd \<le> i \<and> s = n\<^sub>0 \<and> dn = d\<^sub>0 \<and> t = currentTerm nd))"
unfolding promised'_def promised_def Vote' by auto
have prevAccepted_eq: "\<And>i t q. prevAccepted' i t q = prevAccepted i t q \<union> {t'. n\<^sub>0 \<in> q \<and> i = firstUncommittedSlot nd \<and> t = currentTerm nd \<and> lastAcceptedTerm nd = SomeTerm t'}"
unfolding prevAccepted_def prevAccepted'_def Vote' by auto
have property_simps[simp]:
"\<And>n. currentNode (nodeState' n) = currentNode (nodeState n)"
"\<And>n. firstUncommittedSlot (nodeState' n) = firstUncommittedSlot (nodeState n)"
"\<And>n. currentVotingNodes (nodeState' n) = currentVotingNodes (nodeState n)"
"\<And>n q. isQuorum (nodeState' n) q = isQuorum (nodeState n) q"
"\<And>n. lastAcceptedTerm (nodeState' n) = lastAcceptedTerm (nodeState n)"
"\<And>n. lastAcceptedValue (nodeState' n) = lastAcceptedValue (nodeState n)"
"\<And>n. currentTerm (nodeState' n) = currentTerm (nodeState n)"
"\<And>n. publishPermitted (nodeState' n) = publishPermitted (nodeState n)"
"\<And>n. publishVotes (nodeState' n) = publishVotes (nodeState n)"
"\<And>n. currentClusterState (nodeState' n) = currentClusterState (nodeState n)"
"\<And>n. electionWon (nodeState' n) = electionWon (nodeState n)"
"\<And>n. joinVotes (nodeState' n) = joinVotes (nodeState n)"
by (unfold nodeState'_def, auto simp add: nd_def isQuorum_def nd' addElectionVote_def Let_def)
show "zen messages' nodeState'"
apply (intro zenI)
apply (unfold message_simps property_simps committedTo_eq V_eq lastCommittedClusterStateBefore_eq v_eq)
proof -
from finite_messages show "finite messages'" by (simp add: messages')
from currentNode_nodeState show "\<And>n. currentNode (nodeState n) = n" .
from committedTo_firstUncommittedSlot show "\<And>n. committed\<^sub>< (firstUncommittedSlot (nodeState n))" .
from firstUncommittedSlot_PublishResponse show "\<And>n i t. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>" .
from lastAcceptedTerm_None show "\<And>n i t. lastAcceptedTerm (nodeState n) = NO_TERM \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_sent show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_max show "\<And>n t t'. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> n \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) t' \<rangle>\<leadsto> \<Longrightarrow> t' \<le> t".
from electionWon_isQuorum show "\<And>n. electionWon (nodeState n) \<Longrightarrow> isQuorum (nodeState n) (joinVotes (nodeState n))".
from publishVotes show "\<And>n n'. n' \<in> publishVotes (nodeState n) \<Longrightarrow> n' \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) \<rangle>\<leadsto>".
from currentClusterState_lastCommittedClusterStateBefore show "\<And>n. currentClusterState (nodeState n) = lastCommittedClusterStateBefore (firstUncommittedSlot (nodeState n))".
from PublishRequest_committedTo show "\<And>i t x. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from PublishRequest_function show "\<And>i t x x'. \<langle> PublishRequest i t x \<rangle>\<leadsto> \<Longrightarrow> \<langle> PublishRequest i t x' \<rangle>\<leadsto> \<Longrightarrow> x = x'".
from PublishResponse_PublishRequest show "\<And>i s t. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>x. \<langle> PublishRequest i t x \<rangle>\<leadsto>".
from ApplyCommit_quorum show "\<And>i t. \<langle> ApplyCommit i t \<rangle>\<leadsto> \<Longrightarrow> \<exists>q\<in>majorities (V i). \<forall>s\<in>q. s \<midarrow>\<langle> PublishResponse i t \<rangle>\<leadsto>".
from currentVotingNodes_firstUncommittedSlot show "\<And>n. currentVotingNodes (nodeState n) = V (firstUncommittedSlot (nodeState n))".
from firstUncommittedSlot_PublishRequest show "\<And>i n t x. firstUncommittedSlot (nodeState n) < i \<Longrightarrow> \<not> n \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>".
from lastAcceptedTerm_Some_value show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t (lastAcceptedValue (nodeState n)) \<rangle>\<leadsto>".
from PublishRequest_currentTerm show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> t \<le> currentTerm (nodeState n)".
from PublishRequest_publishPermitted_currentTerm show "\<And>n t x. n \<midarrow>\<langle> PublishRequest (firstUncommittedSlot (nodeState n)) t x \<rangle>\<leadsto> \<Longrightarrow> publishPermitted (nodeState n) \<Longrightarrow> t < currentTerm (nodeState n)".
from CatchUpResponse_committedTo show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> committed\<^sub>< i".
from CatchUpResponse_V show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> V i = conf".
from CatchUpResponse_lastCommittedClusterStateBefore show "\<And>i conf cs. \<langle> CatchUpResponse i conf cs \<rangle>\<leadsto> \<Longrightarrow> lastCommittedClusterStateBefore i = cs".
from lastAcceptedTerm_Some_currentTerm show "\<And>n t. lastAcceptedTerm (nodeState n) = SomeTerm t \<Longrightarrow> t \<le> currentTerm (nodeState n)".
from Vote_currentTerm show "\<And>n i t a. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>' \<Longrightarrow> t \<le> currentTerm (nodeState n)"
unfolding Vote' by (auto simp add: nd_def)
from joinVotes show "\<And>n n'. n' \<in> joinVotes (nodeState n) \<Longrightarrow> promised' (firstUncommittedSlot (nodeState n)) n' n (currentTerm (nodeState n))"
unfolding promised_eq by simp
from Vote_future firstUncommittedSlot_PublishResponse
show "\<And>i i' s t t' a. s \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>' \<Longrightarrow> i < i' \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i' t' \<rangle>\<leadsto>"
unfolding Vote' nd_def by auto
from Vote_None show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t NO_TERM \<rangle>\<leadsto>' \<Longrightarrow> t' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>"
unfolding Vote' using Vote_future lastAcceptedTerm_None nd' nd'_def by auto
from Vote_Some_lt show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>' \<Longrightarrow> t' < t"
unfolding Vote' using not_accepted lastAcceptedTerm_def
by (smt fst_conv TermOption.distinct(1) snd_conv)
from Vote_Some_PublishResponse show "\<And>i s t t'. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>' \<Longrightarrow> s \<midarrow>\<langle> PublishResponse i t' \<rangle>\<leadsto>"
unfolding Vote' using lastAcceptedTerm_Some_sent nd' nd'_def nd_def
by (smt Pair_inject TermOption.distinct(1))
from Vote_Some_max show "\<And>i s t t' t''. s \<midarrow>\<langle> Vote i t (SomeTerm t') \<rangle>\<leadsto>' \<Longrightarrow> t' < t'' \<Longrightarrow> t'' < t \<Longrightarrow> \<not> s \<midarrow>\<langle> PublishResponse i t'' \<rangle>\<leadsto>"
unfolding Vote' nd_def
by (smt Pair_inject TermOption.distinct(1) \<open>\<And>t' t na. \<lbrakk>lastAcceptedTerm (nodeState na) = SomeTerm t; na \<midarrow>\<langle> PublishResponse (firstUncommittedSlot (nodeState na)) t' \<rangle>\<leadsto>\<rbrakk> \<Longrightarrow> t' \<le> t\<close> leD)
from Vote_not_broadcast show "\<And>i t a d. \<langle> Vote i t a \<rangle>\<rightarrow>' d \<Longrightarrow> d \<noteq> Broadcast"
unfolding Vote' by blast
from Vote_unique_destination show "\<And>i' i s t a a' d d'. s \<midarrow>\<langle> Vote i t a \<rangle>\<rightarrow>' d \<Longrightarrow> s \<midarrow>\<langle> Vote i' t a' \<rangle>\<rightarrow>' d' \<Longrightarrow> d = d'"
unfolding Vote' using isMessageFrom_def not_sent by auto
from Vote_slot_function show "\<And>n i i' t a a'. n \<midarrow>\<langle> Vote i t a \<rangle>\<leadsto>' \<Longrightarrow> n \<midarrow>\<langle> Vote i' t a' \<rangle>\<leadsto>' \<Longrightarrow> i = i'"
unfolding Vote'
by (metis Vote'(3) Message.inject(2) RoutedMessage.ext_inject insert_iff isMessageFrom'_def isMessageFromTo'_def isMessageFromTo_def isMessageFrom_def messages' not_sent)
from joinVotes_max show "\<And>n n' a'. \<not> (\<exists>x. \<langle> PublishRequest (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) x \<rangle>\<leadsto>) \<Longrightarrow> n' \<in> joinVotes (nodeState n) \<Longrightarrow> n' \<midarrow>\<langle> Vote (firstUncommittedSlot (nodeState n)) (currentTerm (nodeState n)) a' \<rangle>\<rightarrow>' (OneNode n) \<Longrightarrow> a' \<le> lastAcceptedTerm (nodeState n)"
unfolding Vote'
by (smt Vote'(1) Message.inject(2) RoutedMessage.ext_inject insert_iff isMessageFromTo'_def isMessageFrom_def joinVotes messages' not_sent promised_def zen.Vote_slot_function zenMessages.Vote_value_function zenMessages_axioms zen_axioms)
fix i s t x
assume "s \<midarrow>\<langle> PublishRequest i t x \<rangle>\<leadsto>"