-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathProcess_Epoch_O_Specs.thy
6087 lines (5152 loc) · 364 KB
/
Process_Epoch_O_Specs.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
theory Process_Epoch_O_Specs
imports ProcessEpoch_O sqrt_proof Hoare_VCG Sep_Logic_Incomplete
begin
locale extended_hl_pre = extended_vc + hoare_logic +
assumes churn_limit_quotient_config_nonempty[simp]: "CHURN_LIMIT_QUOTIENT config \<noteq> 0"
and effective_balance_safe[simp]:
"MAX_EFFECTIVE_BALANCE \<le> MAX_EFFECTIVE_BALANCE + EFFECTIVE_BALANCE_INCREMENT config"
and EBI_ge_zero[intro]: "EFFECTIVE_BALANCE_INCREMENT config > 0"
and SLOTS_PER_EPOCH_ATLEAST[simp]: "1 < SLOTS_PER_EPOCH config"
and EPOCHS_PER_ETH1_VOTING_PERIOD_ATLEAST[simp]: "EPOCHS_PER_ETH1_VOTING_PERIOD config \<noteq> 0"
and EBI_nonzero[simp]: "EFFECTIVE_BALANCE_INCREMENT config \<noteq> 0"
and brf_ebi_times_bounded[simp]:
"EFFECTIVE_BALANCE_INCREMENT config *
BASE_REWARD_FACTOR config div EFFECTIVE_BALANCE_INCREMENT config =
BASE_REWARD_FACTOR config"
and EBI_multiple_of_HYSTERESIS_QUOTIENT:
"\<exists>n. HYSTERESIS_QUOTIENT * n div n = HYSTERESIS_QUOTIENT \<and> EFFECTIVE_BALANCE_INCREMENT config = HYSTERESIS_QUOTIENT * n"
and ISB_not_zero[simp]: "INACTIVITY_SCORE_BIAS config \<noteq> 0"
and brf_not_zero: "BASE_REWARD_FACTOR config \<noteq> 0"
and upward_threshold_safe: "((EFFECTIVE_BALANCE_INCREMENT config div HYSTERESIS_QUOTIENT) * HYSTERESIS_UPWARD_MULTIPLIER)
div (EFFECTIVE_BALANCE_INCREMENT config div HYSTERESIS_QUOTIENT) = HYSTERESIS_UPWARD_MULTIPLIER"
begin
declare [[show_sorts=false]]
declare [[show_types=false]]
term free
lemma read_beacon_wp[wp]: "(\<And>x. x = v \<Longrightarrow> hoare_triple ( lift (P x)) (c x) (Q )) \<Longrightarrow> hoare_triple (lift (maps_to l v \<and>* (maps_to l v \<longrightarrow>* (P v )))) (do {v <- read_beacon l ; c v}) (Q )"
apply (clarsimp simp: hoare_triple_def bindCont_def run_def read_beacon_def getState_def )
apply (clarsimp simp: Sup_le_iff)
apply (safe)
apply (clarsimp simp: fail_def assert_galois_test)
defer
apply (clarsimp simp: fail_def assert_galois_test return_def)
apply (case_tac "y = v"; clarsimp?)
apply (subst seq_assoc[symmetric])
apply (subst test_seq_test)
apply (rule order_trans, rule seq_mono_left)
apply (rule test.hom_mono[where p="Collect (lift (P v))"])
apply (clarsimp)
apply (sep_solve)
apply (blast)
apply (subst seq_assoc[symmetric])
apply (subst test_seq_test)
apply (rule order_trans, rule seq_mono_left)
apply (rule test.hom_mono[where p="{}"])
apply (clarsimp)
defer
apply (clarsimp)
apply (subst seq_assoc[symmetric])
apply (subst test_seq_test)
apply (rule order_trans, rule seq_mono_left)
apply (rule test.hom_mono[where p="{}"])
apply (clarsimp)
defer
apply (clarsimp)
apply (drule maps_to_get_wf, clarsimp)
apply (drule maps_to_get_wf, clarsimp)
done
lemma get_current_epoch_wp[wp]: "hoare_triple (lift (P (slot_to_epoch config v))) (f (slot_to_epoch config v)) Q \<Longrightarrow>
hoare_triple (lift (maps_to beacon_slots v \<and>* (maps_to beacon_slots v \<longrightarrow>* P (slot_to_epoch config v)))) (bindCont get_current_epoch f) Q"
apply (clarsimp simp: get_current_epoch_def)
apply (rule hoare_weaken_pre)
apply (clarsimp simp: bindCont_assoc[symmetric] bindCont_return')
apply (rule read_beacon_wp, fastforce)
apply (rule order_refl)
done
lemma valid_lens_withdrawable_epoch[simp]:"valid_lens withdrawable_epoch"
by (clarsimp simp: valid_lens_def withdrawable_epoch_def get_set_def set_get_def set_set_def)
lemma get_previous_epoch_wp':"(\<And>x. hoare_triple (lift (P x)) (f x) Q) \<Longrightarrow> hoare_triple (lift (maps_to beacon_slots v \<and>*
(maps_to beacon_slots v \<longrightarrow>*
(if slot_to_epoch config v = GENESIS_EPOCH then P GENESIS_EPOCH
else (\<lambda>s. 1 \<le> epoch_to_u64 (slot_to_epoch config v) \<and>
(1 \<le> epoch_to_u64 (slot_to_epoch config v) \<longrightarrow> P (Epoch (epoch_to_u64 (slot_to_epoch config v) - 1)) s)))))) (bindCont get_previous_epoch f) Q"
apply (simp only: get_previous_epoch_def, rule hoare_weaken_pre)
apply (subst bindCont_assoc[symmetric])
apply (rule get_current_epoch_wp)
apply (rule if_wp)
apply (rule return_triple', assumption)
apply (simp add: epoch_unsigned_sub_def, wp)
apply (rule order_refl)
done
lemma previous_genesis[simp]: "previous_epoch GENESIS_EPOCH = GENESIS_EPOCH"
by (clarsimp simp: previous_epoch_def)
lemma previous_is_self_simp[simp]: "previous_epoch e = e \<longleftrightarrow> e = GENESIS_EPOCH"
apply (clarsimp simp: previous_epoch_def GENESIS_EPOCH_def)
by (metis diff_0_right diff_left_imp_eq epoch_to_u64.simps zero_neq_one)
lemma get_previous_epoch_wp[wp]:"hoare_triple (lift (P (previous_epoch (slot_to_epoch config v)))) (f (previous_epoch (slot_to_epoch config v))) Q \<Longrightarrow>
hoare_triple (lift (maps_to beacon_slots v \<and>* (maps_to beacon_slots v \<longrightarrow>*
P (previous_epoch (slot_to_epoch config v)) ))) (bindCont get_previous_epoch f) Q"
apply (simp only: get_previous_epoch_def, rule hoare_weaken_pre)
apply (wp)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (drule sym[where s="slot_to_epoch config v"], drule sym, clarsimp, assumption)
apply (simp add: epoch_unsigned_sub_def, wp)
apply (clarsimp simp: previous_epoch_def split: if_splits, assumption)
apply (clarsimp)
apply (sep_cancel)+
apply (intro conjI impI allI; clarsimp)
apply (sep_mp)
apply (clarsimp simp: GENESIS_EPOCH_def)
apply (clarsimp simp: slot_to_epoch_def)
using lt1_neq0 apply blast
apply (sep_mp)
apply (clarsimp simp: previous_epoch_def split: if_splits)
done
lemma get_active_validator_indices_wp[wp]:
"hoare_triple (lift (P (active_validator_indices epoch v))) (f (active_validator_indices epoch v)) Q \<Longrightarrow>
hoare_triple (lift (maps_to validators v \<and>* (maps_to validators v \<longrightarrow>* P (active_validator_indices epoch v)))) (bindCont (get_active_validator_indices epoch) f) Q"
apply (unfold get_active_validator_indices_def, rule hoare_weaken_pre)
apply (clarsimp simp: liftM_def)
apply (wp)
apply (clarsimp simp: comp_def)
apply (erule hoare_eqI')
apply (clarsimp)
apply (rule exI, sep_cancel)+
apply (sep_cancel)+
apply (sep_mp)
apply (clarsimp)
done
lemma if_refl: "(if (P = P) then Q else R) = Q"
by (clarsimp)
lemma get_current_unslashed_participating_indices_wp[wp]:" hoare_triple (lift (pre {x \<in> list.set (active_validator_indices (slot_to_epoch config current_slot) valids). has_flag (unsafe_var_list_index cep x) flag_index \<and> \<not> slashed_f (unsafe_var_list_index valids x)})) (f {x \<in> list.set (active_validator_indices (slot_to_epoch config current_slot) valids). has_flag (unsafe_var_list_index cep x) flag_index \<and> \<not> slashed_f (unsafe_var_list_index valids x)}) Q \<Longrightarrow>
hoare_triple
(lift (maps_to beacon_slots current_slot \<and>* maps_to current_epoch_participation cep \<and>* maps_to validators valids \<and>*
((maps_to beacon_slots current_slot \<and>* maps_to current_epoch_participation cep \<and>* maps_to validators valids) \<longrightarrow>* pre ({x \<in> list.set (active_validator_indices (slot_to_epoch config current_slot) valids). has_flag (unsafe_var_list_index cep x) flag_index \<and> \<not> slashed_f (unsafe_var_list_index valids x)})) )) (bindCont (get_unslashed_participating_indices flag_index (slot_to_epoch config current_slot)) f) Q"
apply (unfold get_unslashed_participating_indices_def, rule hoare_weaken_pre)
apply (simp only: bindCont_assoc[symmetric])
apply (rule get_previous_epoch_wp)
apply (rule get_current_epoch_wp)
apply (rule assert_wp')
apply (simp)
apply (rule read_beacon_wp[where v=cep], simp)
apply (clarsimp, wp, clarsimp)
apply (assumption)
apply (clarsimp)
apply (sep_cancel)
apply (sep_cancel)+
apply (simp)
apply (sep_mp)
apply (clarsimp)
done
lemma get_previous_unslashed_participating_indices_wp[wp]:" (\<And>x. hoare_triple (lift (pre {x \<in> list.set (active_validator_indices (previous_epoch (slot_to_epoch config current_slot)) valids). has_flag (unsafe_var_list_index pep x) flag_index \<and> \<not> slashed_f (unsafe_var_list_index valids x)})) (f {x \<in> list.set (active_validator_indices (previous_epoch (slot_to_epoch config current_slot)) valids). has_flag (unsafe_var_list_index pep x) flag_index \<and> \<not> slashed_f (unsafe_var_list_index valids x)}) Q) \<Longrightarrow> (slot_to_epoch config current_slot) \<noteq> GENESIS_EPOCH \<Longrightarrow> hoare_triple
(lift (maps_to beacon_slots current_slot \<and>* maps_to previous_epoch_participation pep \<and>* maps_to current_epoch_participation cep \<and>* maps_to validators valids \<and>*
((maps_to beacon_slots current_slot \<and>* maps_to previous_epoch_participation pep \<and>* maps_to current_epoch_participation cep \<and>* maps_to validators valids) \<longrightarrow>* pre ({x \<in> list.set (active_validator_indices (previous_epoch (slot_to_epoch config current_slot)) valids). has_flag (unsafe_var_list_index pep x) flag_index \<and> \<not> slashed_f (unsafe_var_list_index valids x)})) ))
(bindCont (get_unslashed_participating_indices flag_index (previous_epoch (slot_to_epoch config current_slot))) f) Q"
apply (unfold get_unslashed_participating_indices_def, rule hoare_weaken_pre)
apply (simp only: bindCont_assoc[symmetric])
apply (rule get_previous_epoch_wp)
apply (rule get_current_epoch_wp)
apply (rule assert_wp')
apply (simp)
apply (rule read_beacon_wp[where v=pep], simp)
apply (clarsimp, wp, clarsimp)
apply (assumption)
apply (clarsimp)
apply (sep_cancel)
apply (sep_cancel)+
apply (simp)
apply (sep_mp)
apply (clarsimp)
done
lemma unat_sum_list_simp:"sum_list (map unat xs) \<le> 2^64 - 1 \<Longrightarrow> unat (sum_list (xs :: u64 list)) = sum_list (map unat xs)"
apply (induct xs; clarsimp)
apply (unat_arith; clarsimp)
done
lemma safe_sum_distinct_wb: " (sum_list (map unat xs)) \<le> 2^64 - 1 \<Longrightarrow> safe_sum xs = return (sum_list xs)"
apply (induct xs; clarsimp simp: safe_sum_def)
apply (subst foldrM_shift)
apply (clarsimp)
apply (clarsimp simp: word_unsigned_add_def Let_unfold, safe; (clarsimp simp: bindCont_return split: if_splits)?)
apply (metis add.commute)
apply (erule notE)
apply (unat_arith; clarsimp)
apply (clarsimp simp: unat_sum_list_simp)
done
lemma sum_list_wp[wp]: "hoare_triple (lift (P (sum_list xs))) (f (sum_list xs)) Q \<Longrightarrow>
hoare_triple (lift (\<lambda>s. (sum_list (map unat xs)) \<le> 2^64 - 1 \<and> ((sum_list (map unat xs)) \<le> 2^64 - 1 \<longrightarrow> P (sum_list xs) s))) (do {b <- safe_sum xs; f b}) Q"
apply ( rule hoare_assert_stateI, clarsimp)
apply (subst safe_sum_distinct_wb, clarsimp)
apply (clarsimp)
apply (rule hoare_weaken_pre, assumption)
apply (clarsimp)
done
lemma plus_one_helper_nat[elim!]:
"x < n + (1 :: nat) \<Longrightarrow> x \<le> n"
by (simp add: word_less_nat_alt word_le_nat_alt field_simps)
lemma count_list_remove1: "Suc n \<le> count_list ys a \<Longrightarrow> n \<le> count_list (remove1 a ys) a"
apply (induct ys; clarsimp)
by (metis Suc_eq_plus1 add.commute nat_add_left_cancel_le)
lemma count_ge_suc_in_set: "Suc n \<le> count_list ys a \<Longrightarrow> a \<in> list.set ys"
apply (induct ys; clarsimp)
using linorder_not_le by fastforce
lemma count_neq_remove1[simp]: "x \<noteq> a \<Longrightarrow> count_list (remove1 a ys) x = count_list ys x"
by (induct ys; clarsimp)
lemma sum_list_map_leI:"(\<And>x. count_list ys x \<ge> count_list xs x) \<Longrightarrow> (\<Sum>a\<leftarrow>xs. (f a) :: nat) \<le> sum_list (map f ys)"
apply (induct xs arbitrary: ys ; clarsimp)
apply (atomize)
apply (erule_tac x="remove1 a ys" in allE)
apply (drule mp)
apply (clarsimp)
apply (erule_tac x=x in allE)
apply (clarsimp split: if_splits)
apply (erule count_list_remove1)
apply (subst sum_list_map_remove1) back
apply (erule_tac x=a in allE; clarsimp)
apply (erule count_ge_suc_in_set)
using add_left_mono apply blast
done
lemma sum_map_map:"(\<Sum>a\<leftarrow>xs. f (g a)) = (\<Sum>a\<leftarrow>(map g xs). (f a))"
apply (clarsimp)
apply (clarsimp simp: comp_def)
done
lemma lists_of_set_reduce_count: "xs \<in> lists_of ys' \<Longrightarrow> ys' \<subseteq> list.set ys \<Longrightarrow> count_list xs a \<le> count_list ys a"
apply (induct ys arbitrary: ys'; clarsimp simp: lists_of_def)
apply (safe)
apply (metis Diff_insert_absorb Set.set_insert count_ge_suc_in_set count_list_remove1 not_less_eq_eq set_remove1_eq)
by (metis Diff_iff count_ge_suc_in_set count_list_0_iff count_list_remove1 insert_iff not_less_eq_eq order_antisym_conv set_remove1_eq subset_code(1))
lemma [simp]: "var_list_inner (VariableList vs) = vs"
by (simp add: var_list_inner_def)
lemma map_unsafe_var_list[simp]: "(map (unsafe_var_list_index (VariableList vs)) xs) = map (\<lambda>v. vs ! unat v) xs"
by (clarsimp simp: unsafe_var_list_index_def)
lemma distinct_index_list_map: "distinct (Invariants.var_list_inner v) \<Longrightarrow>
distinct xs \<Longrightarrow> \<forall>x\<in>(list.set xs). x < var_list_len v \<Longrightarrow>
distinct (map (unsafe_var_list_index v) xs)"
apply (induct xs; clarsimp)
apply (case_tac v; clarsimp simp: unsafe_var_list_index_def)
by (metis distinct_the_index_is_index unat_less_helper word_unat.Rep_inverse)
lemma nth_mem' [intro]: "n < length xs \<Longrightarrow> xs ! n = a \<Longrightarrow> a \<in> list.set xs"
by (auto simp add: set_conv_nth)
lemma in_set_zip_iff: "(a,b) \<in> list.set (zip xs ys) \<longleftrightarrow> (\<exists>n. n < length xs \<and> n < length ys \<and> xs ! n = a \<and> ys ! n = b)"
apply (safe; clarsimp?)
apply (induct xs arbitrary: ys ; clarsimp)
apply (case_tac ys; clarsimp)
apply (safe)
apply auto[1]
apply (metis Suc_less_eq nth_Cons_Suc)
apply (rule_tac n=n in nth_mem', clarsimp)
apply (clarsimp)
done
lemma bounded_enumerate: "(i, v) \<in> list.set (local.enumerate (local.var_list_inner vs)) \<Longrightarrow> length (var_list_inner vs) \<le> 2^64 - 1 \<Longrightarrow> i < var_list_len vs"
apply (case_tac vs; clarsimp)
apply (clarsimp simp: enumerate_def)
apply (clarsimp simp: in_set_zip_iff)
apply (rule of_nat_mono_maybe, clarsimp)
apply (clarsimp)
done
lemma index_in_length_in_set[intro!]: "xb < var_list_len v \<Longrightarrow> local.var_list_inner v ! unat xb \<in> list.set (Invariants.var_list_inner v)"
apply (case_tac v; clarsimp)
by (simp add: unat_less_helper)
declare range.simps[simp del ]
lemma get_total_balance_wp[wp]:"(\<And>x xs (v :: Validator VariableList). distinct xs \<Longrightarrow> list.set xs = S \<Longrightarrow> x = max (EFFECTIVE_BALANCE_INCREMENT config) (sum_list (map (Validator.effective_balance_f \<circ> unsafe_var_list_index v) xs)) \<Longrightarrow>
hoare_triple (lift (P x)) (f x) Q)
\<Longrightarrow> hoare_triple (lift ((maps_to validators v \<and>* (maps_to validators v \<longrightarrow>* (\<lambda>s. (\<forall>x\<in>S. x < var_list_len v) \<and> ((\<forall>x\<in>S. x < var_list_len v) \<longrightarrow> (\<forall>xs\<in>lists_of S. P (max (EFFECTIVE_BALANCE_INCREMENT config) (sum_list (map (Validator.effective_balance_f \<circ> unsafe_var_list_index v) xs))) s) )))) ))
(do {b <- get_total_balance S; f b}) Q"
apply (clarsimp simp: get_total_balance_def, rule hoare_weaken_pre)
apply (wp)
apply (clarsimp)
apply (atomize)
apply (erule_tac allE)
apply (erule_tac x=a in allE)
apply (fastforce)
apply (clarsimp)
apply (rule exI)
apply (sep_cancel)
apply (sep_cancel)
apply (clarsimp)
apply (intro conjI impI)
apply (clarsimp simp: lists_of_def)
apply (sep_frule (direct) maps_to_is_valid[where l=validators])
apply (clarsimp)
apply (rule plus_one_helper_nat, clarsimp)
apply (clarsimp simp: Let_unfold)
apply (erule le_less_trans[rotated])
apply (clarsimp simp: comp_def)
apply (subst sum_map_map, rule sum_list_map_leI[where ys="Invariants.var_list_inner v"])
apply (clarsimp simp: unsafe_var_list_index_def)
apply (rule order_trans, rule lists_of_set_reduce_count[where ys="Invariants.var_list_inner v"])
apply (clarsimp simp: lists_of_def)
apply (intro conjI)
apply (rule distinct_index_list_map, assumption, assumption)
apply (sep_mp, clarsimp)
apply (rule refl)
apply (clarsimp)
apply (clarsimp simp: unsafe_var_list_index_def)
apply (sep_mp, clarsimp, rule order_refl)
apply (sep_mp, clarsimp)
apply (erule_tac x=x in ballE, clarsimp)
by (clarsimp simp: lists_of_def)
(* TODO add in real spec *)
lemma weigh_justification_and_finalization_wp[wp]: "(hoare_triple (lift (P ())) (f ()) Q) \<Longrightarrow>
hoare_triple (lift (P ())) (do {b <- weigh_justification_and_finalization total_b previous current ; f b}) Q"
sorry
lemma gen_epoch_add_zero[simp]:" epoch_unsigned_add GENESIS_EPOCH x = return x"
apply (clarsimp simp: GENESIS_EPOCH_def)
apply (intro ext, clarsimp simp: return_def epoch_unsigned_add_def bindCont_def word_unsigned_add_def)
by (metis Epoch.collapse epoch_to_u64.simps)
lemma [simp]: "((\<lambda>a. the (u64_of a)) \<circ> u64) = id "
by (intro ext; clarsimp)
lemma [simp]: "ProgressiveBalancesCache.fields (total_active_balance_f pbc) (previous_epoch_flag_attesting_balances_f pbc) (current_epoch_flag_attesting_balances_f pbc) = pbc"
by (clarsimp simp: ProgressiveBalancesCache.defs)
lemma process_fast_spec: "hoare_triple (lift (maps_to beacon_slots b \<and>* maps_to progressive_balances_cache pbc \<and>* R)) process_justification_and_finalization_fast
(lift (maps_to beacon_slots b \<and>* maps_to progressive_balances_cache pbc \<and>* R))"
apply (unfold process_justification_and_finalization_fast_def, rule hoare_weaken_pre, wp)
apply (simp only: gen_epoch_add_zero)
apply (wp)
apply (clarsimp, safe)
apply (sep_cancel)+
apply (rule exI)
by (sep_cancel)+
lemma active_validator_indices_are_bound: "x \<in> list.set (active_validator_indices e v) \<Longrightarrow> length (local.var_list_inner v) \<le> 2 ^ 64 - 1 \<Longrightarrow> x < var_list_len v"
apply (clarsimp simp: active_validator_indices_def)
apply (erule bounded_enumerate)
apply (clarsimp)
done
lemma "hoare_triple (lift (maps_to beacon_slots b \<and>* maps_to previous_epoch_participation pep \<and>* maps_to current_epoch_participation cep \<and>* maps_to validators v \<and>* R \<and>* R')) process_justification_and_finalization
(lift (maps_to beacon_slots b \<and>* maps_to validators v \<and>* maps_to previous_epoch_participation pep \<and>* maps_to current_epoch_participation cep \<and>* R \<and>* R'))"
apply (subgoal_tac "epoch_to_u64 GENESIS_EPOCH \<le> epoch_to_u64 GENESIS_EPOCH + 1")
apply (unfold process_justification_and_finalization_def)
apply (rule hoare_weaken_pre)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule get_previous_epoch_wp[where v=b])
apply (rule get_current_epoch_wp[where v=b])
apply (wp)
apply (clarsimp simp: get_total_active_balance_def, wp)
using less_eq_Epoch_def apply force
apply (rule le_funI)
apply (simp)
apply (safe)
apply (sep_cancel)+
apply (clarsimp)
apply (safe)
defer
apply (sep_cancel)+
apply (clarsimp)
apply (intro conjI impI)
apply (clarsimp)
defer
apply (clarsimp)
apply (sep_cancel)+
apply (intro conjI)
apply (clarsimp)
apply (safe; clarsimp?)
apply (sep_solve)
defer
defer
apply (erule active_validator_indices_are_bound)
apply (sep_frule (direct) maps_to_is_valid[where l=validators])
apply (clarsimp simp: Let_unfold)
apply (case_tac v; clarsimp)
apply (clarsimp)
apply (erule active_validator_indices_are_bound)
apply (sep_frule (direct) maps_to_is_valid[where l=validators])
apply (clarsimp simp: Let_unfold)
apply (case_tac v; clarsimp)
done
lemma get_validator_churn_limit_fast_spec: "hoare_triple (\<lless>num_active_validators \<mapsto>\<^sub>l n \<and>* R\<then>) get_validator_churn_limit_fast (lift (num_active_validators \<mapsto>\<^sub>l n \<and>* R))"
apply (clarsimp simp: get_validator_churn_limit_fast_def, rule hoare_weaken_pre)
apply (wp)
apply (clarsimp)
apply (rule exI)
apply (sep_solve)
done
lemma get_validator_churn_limit_fast_wp[wp]: "(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple (\<lless>num_active_validators \<mapsto>\<^sub>l n \<and>* (num_active_validators \<mapsto>\<^sub>l n \<longrightarrow>* P (max (MIN_PER_EPOCH_CHURN_LIMIT config) (n div CHURN_LIMIT_QUOTIENT config)))\<then>)
(bindCont get_validator_churn_limit_fast c) (Q)"
apply (clarsimp simp: get_validator_churn_limit_fast_def, rule hoare_weaken_pre)
apply (wp)
by (fastforce)
lemma get_validator_churn_limit_spec: "hoare_triple (\<lless>beacon_slots \<mapsto>\<^sub>l v \<and>* validators \<mapsto>\<^sub>l vs \<and>* R\<then>) get_validator_churn_limit (lift (beacon_slots \<mapsto>\<^sub>l v \<and>* validators \<mapsto>\<^sub>l vs \<and>* R))"
apply (clarsimp simp: get_validator_churn_limit_def, rule hoare_weaken_pre)
apply (wp)
apply (clarsimp)
apply (sep_cancel)+
done
lemma get_validator_churn_limit_spec': "(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple (\<lless>beacon_slots \<mapsto>\<^sub>l v \<and>* validators \<mapsto>\<^sub>l vs \<and>* (beacon_slots \<mapsto>\<^sub>l v \<and>* validators \<mapsto>\<^sub>l vs \<longrightarrow>* P (max (MIN_PER_EPOCH_CHURN_LIMIT config) (word_of_nat (length (active_validator_indices (slot_to_epoch config v) vs)) div CHURN_LIMIT_QUOTIENT config))) \<then>) (bindCont get_validator_churn_limit c) (Q)"
apply (clarsimp simp: get_validator_churn_limit_def, rule hoare_weaken_pre)
apply (wp)
apply (clarsimp)
apply (sep_cancel)+
apply (sep_mp)
apply (sep_cancel)+
done
definition "next_epoch b_slots \<equiv> epoch_to_u64 (slot_to_epoch config b_slots) + 1"
lemma process_eth1_data_reset: "hoare_triple (lift (beacon_slots \<mapsto>\<^sub>l b \<and>* eth1_data_votes \<mapsto>\<^sub>l data_votes \<and>* R))
process_eth1_data_reset
(lift (beacon_slots \<mapsto>\<^sub>l b \<and>*
eth1_data_votes \<mapsto>\<^sub>l (if (next_epoch b) mod (EPOCHS_PER_ETH1_VOTING_PERIOD config) = 0 then (VariableList []) else data_votes) \<and>* R))"
apply (unfold process_eth1_data_reset_def epoch_unsigned_add_def, rule hoare_weaken_pre)
apply (wp)
apply (safe)
apply (sep_cancel)+
apply (intro conjI impI)
apply (clarsimp)
apply (clarsimp simp: slot_to_epoch_def)
apply (subgoal_tac "SLOTS_PER_EPOCH config > 1")
apply (metis (no_types, opaque_lifting) div_by_0 div_less_dividend_word div_word_self less_is_non_zero_p1 lt1_neq0 olen_add_eqv word_div_lt_eq_0)
apply (clarsimp)
apply (clarsimp)
apply (clarsimp simp: next_epoch_def)
apply (rule exI)
by (sep_cancel)+
definition "previous_epochs bs = {e. e \<le> previous_epoch (slot_to_epoch config bs)}"
lemma raw_epoch_simp: "raw_epoch = epoch_to_u64"
by (intro ext, case_tac x; clarsimp)
lemma get_finality_delay_wp[wp]:
"hoare_triple (lift (P (raw_epoch (previous_epoch (slot_to_epoch config bs)) - raw_epoch (epoch_f f_c))))
(c ((raw_epoch (previous_epoch (slot_to_epoch config bs)) - raw_epoch (epoch_f f_c)))) R \<Longrightarrow>
hoare_triple (lift (\<lambda>s. epoch_f f_c \<in> previous_epochs bs \<and> (epoch_f f_c \<in> previous_epochs bs \<longrightarrow>
(beacon_slots \<mapsto>\<^sub>l bs \<and>* finalized_checkpoint \<mapsto>\<^sub>l f_c \<and>* (beacon_slots \<mapsto>\<^sub>l bs \<and>* finalized_checkpoint \<mapsto>\<^sub>l f_c \<longrightarrow>* P (raw_epoch (previous_epoch (slot_to_epoch config bs)) - raw_epoch (epoch_f f_c)))) s) ) )
(bindCont get_finality_delay c) ( R )"
apply (unfold get_finality_delay_def, rule hoare_weaken_pre)
apply (wp)
apply (clarsimp simp: raw_epoch_simp)
apply (erule hoare_eqI')
apply (clarsimp)
apply (sep_cancel)+
apply (rule exI, sep_cancel)+
apply (clarsimp)
apply (clarsimp simp: previous_epochs_def)
using less_eq_Epoch_def
apply (clarsimp)
apply (sep_mp)
by (clarsimp simp: raw_epoch_simp)
abbreviation (input) "sep_wp pre post P \<equiv> (lift (pre \<and>* (post \<longrightarrow>* P)))"
schematic_goal is_in_activity_leak[wp]:
"hoare_triple (lift (pre ?x)) (c ?x) post \<Longrightarrow>
hoare_triple
(sep_wp (beacon_slots \<mapsto>\<^sub>l b_s \<and>* finalized_checkpoint \<mapsto>\<^sub>l c_f)
(beacon_slots \<mapsto>\<^sub>l b_s \<and>* finalized_checkpoint \<mapsto>\<^sub>l c_f)
(\<lambda>s. Checkpoint.epoch_f c_f \<in> previous_epochs b_s \<and> (Checkpoint.epoch_f c_f \<in> previous_epochs b_s \<longrightarrow> pre ?x s)))
(bindCont is_in_inactivity_leak c) post"
apply (unfold is_in_inactivity_leak_def, rule hoare_weaken_pre)
apply (wp)
apply (rule lift_mono')
apply (clarsimp)
apply (intro conjI impI)
apply (clarsimp simp: sep_conj_assoc)
defer
apply (clarsimp simp: sep_conj_assoc)
apply (sep_cancel)+
apply (sep_mp)
apply (clarsimp)
apply (sep_mp)
apply (clarsimp)
done
lemma epoch_always_bounded[simp]: "epoch_to_u64 (slot_to_epoch config v) \<le> epoch_to_u64 (slot_to_epoch config v) + 1"
apply (clarsimp simp: slot_to_epoch_def)
by (metis (no_types, opaque_lifting) SLOTS_PER_EPOCH_ATLEAST div_0 div_by_1 div_less_dividend_word
less_is_non_zero_p1 lt1_neq0 olen_add_eqv word_div_less zero_neq_one)
lemma subst_in_impl: "(x = y \<longrightarrow> f y) = (x = y \<longrightarrow> f x)"
by (safe)
schematic_goal new_state_context_wp[simplified subst_in_impl, wp]:
"hoare_triple (lift (pre ?x)) (c ?x) post \<Longrightarrow> hoare_triple (lift ?P) (bindCont new_state_context c) (post)"
apply (unfold new_state_context_def epoch_unsigned_add_def, rule hoare_weaken_pre)
apply (wp)
apply (erule hoare_eqI')
apply (clarsimp simp: subst_in_impl)
apply (sep_cancel)+
done
lemma new_slashings_context_wp[wp]:
"hoare_triple (lift (P x)) (c x) Q \<Longrightarrow> hoare_triple (lift (slashings \<mapsto>\<^sub>l ss \<and>*
(slashings \<mapsto>\<^sub>l ss \<longrightarrow>*
(\<lambda>s. safe_mul PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX (sum_list (vector_inner ss)) \<and>
(safe_mul PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX (sum_list (vector_inner ss)) \<longrightarrow>
raw_epoch (current_epoch_f st_ctxt) \<le> raw_epoch (current_epoch_f st_ctxt) + EPOCHS_PER_SLASHINGS_VECTOR config \<and>
(raw_epoch (current_epoch_f st_ctxt) \<le> raw_epoch (current_epoch_f st_ctxt) + EPOCHS_PER_SLASHINGS_VECTOR config \<longrightarrow>
SlashingsContext.fields (min (sum_list (vector_inner ss) * PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX) (total_active_balance_f pbc))
(Epoch ((raw_epoch (current_epoch_f st_ctxt) + EPOCHS_PER_SLASHINGS_VECTOR config) div 2)) =
x \<and>
(SlashingsContext.fields (min (sum_list (vector_inner ss) * PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX) (total_active_balance_f pbc))
(Epoch ((raw_epoch (current_epoch_f st_ctxt) + EPOCHS_PER_SLASHINGS_VECTOR config) div 2)) =
x \<longrightarrow>
P x s))))))) (bindCont (new_slashings_context st_ctxt pbc) c) ( Q)"
apply (clarsimp simp: new_slashings_context_def, rule hoare_weaken_pre , wp)
apply (erule hoare_eqI')
apply (clarsimp)
apply (rule exI)
apply (frule slashings_wf)
apply (erule sep_conj_impl, assumption)
apply (clarsimp)
apply (sep_cancel)+
apply (clarsimp)
apply (sep_mp)
apply (safe; clarsimp?)
by (case_tac ss; clarsimp simp: vector_inner_def)
schematic_goal new_activation_queue_wp[wp]:
"hoare_triple (lift (P x)) (c x) Q \<Longrightarrow>
hoare_triple (lift (beacon_slots \<mapsto>\<^sub>l b_s \<and>* validators \<mapsto>\<^sub>l vs \<and>*
(validators \<mapsto>\<^sub>l vs \<and>* beacon_slots \<mapsto>\<^sub>l b_s \<longrightarrow>*
(\<lambda>sc. fold (\<lambda>(i, v) q. add_if_could_be_eligible_for_activation q i v (Epoch (next_epoch b_s))) (local.enumerate (local.var_list_inner vs)) (ActivationQueue.fields []) = x \<and>
(fold (\<lambda>(i, v) q. add_if_could_be_eligible_for_activation q i v (Epoch (next_epoch b_s))) (local.enumerate (local.var_list_inner vs)) (ActivationQueue.fields []) = x \<longrightarrow> P x sc))) ))
(bindCont new_activation_queue c) Q"
apply (clarsimp simp: new_activation_queue_def epoch_unsigned_add_def, rule hoare_weaken_pre, wp)
apply (erule hoare_eqI')
apply (clarsimp)
apply (fold next_epoch_def)
apply (sep_cancel)+
apply (rule exI, sep_cancel+)
by (sep_mp, clarsimp)
abbreviation "map_varlist f xs \<equiv> map f (local.var_list_inner xs)"
definition "frequency_map xs = Some(0 := None) o of_nat o (count_list xs)"
lemma exit_cache_eq_iff: "(x :: ExitCache) = y \<longleftrightarrow> exit_epoch_counts_f x = exit_epoch_counts_f y"
by (case_tac x; case_tac y; clarsimp)
lemma new_exit_cache_wp[wp]: "
hoare_triple (lift (P x)) (c x) Q \<Longrightarrow>
hoare_triple (lift (validators \<mapsto>\<^sub>l vs \<and>*
(validators \<mapsto>\<^sub>l vs \<longrightarrow>*
(\<lambda>s. exit_epoch_counts_f x = frequency_map (map_varlist exit_epoch_f vs) \<and>
(exit_epoch_counts_f x = frequency_map (map_varlist exit_epoch_f vs) \<longrightarrow> P x s)))))
(bindCont new_exit_cache c) Q"
apply (clarsimp simp: new_exit_cache_def Let_unfold, rule hoare_weaken_pre, wp)
apply (erule hoare_eqI')
apply (clarsimp)
apply (rule exI)
apply (sep_cancel)+
apply (intro conjI impI)
apply (sep_mp)
apply (clarsimp)
apply (clarsimp simp: frequency_map_def exit_cache_eq_iff ExitCache.defs)
apply (intro ext, clarsimp)
apply (sep_mp, clarsimp)
done
lemma sqrt_eq_zero_iff[simp]: "sqrt' x = 0 \<longleftrightarrow> x = 0"
by (metis div_by_1 lt1_neq0 mult.right_neutral sqrt_le_eqI word_coorder.extremum zero_sqrt_zero)
schematic_goal get_base_reward_fast_wp[wp]:
"hoare_triple (lift (P x)) (c x) Q \<Longrightarrow> hoare_triple (lift (\<lambda>s. total_active_balance_f pbc < total_active_balance_f pbc + 1 \<and>
(total_active_balance_f pbc < total_active_balance_f pbc + 1 \<longrightarrow>
total_active_balance_f pbc \<noteq> 0 \<and>
(total_active_balance_f pbc \<noteq> 0 \<longrightarrow>
safe_mul (effective_balance div EFFECTIVE_BALANCE_INCREMENT config) (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) \<and>
(safe_mul (effective_balance div EFFECTIVE_BALANCE_INCREMENT config) (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) \<longrightarrow>
effective_balance div EFFECTIVE_BALANCE_INCREMENT config * (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) = x \<and>
(effective_balance div EFFECTIVE_BALANCE_INCREMENT config * (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) = x \<longrightarrow> P x s ))))))
(bindCont (get_base_reward_fast effective_balance pbc) c) Q"
apply (clarsimp simp: get_base_reward_fast_def, rule hoare_weaken_pre, wp)
apply (clarsimp simp: get_base_reward_per_increment_fast_def, wp)
apply (erule hoare_eqI')
apply (clarsimp)
apply (intro conjI impI; clarsimp?)
apply (metis brf_ebi_times_bounded mult.commute safe_mul_def)
using safe_mul_commute by blast
schematic_goal compute_base_rewards_wp[wp]:
"(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple
(lift (progressive_balances_cache \<mapsto>\<^sub>l pbc \<and>* (progressive_balances_cache \<mapsto>\<^sub>l pbc \<longrightarrow>*
(\<lambda>s. total_active_balance_f pbc < total_active_balance_f pbc + 1 \<and>
(total_active_balance_f pbc < total_active_balance_f pbc + 1 \<longrightarrow>
total_active_balance_f pbc \<noteq> 0 \<and>
(total_active_balance_f pbc \<noteq> 0 \<longrightarrow>
(\<forall>f\<in>list.set (local.range 0 (unat (MAX_EFFECTIVE_BALANCE + EFFECTIVE_BALANCE_INCREMENT config)) (unat (EFFECTIVE_BALANCE_INCREMENT config))).
safe_mul (word_of_nat f div EFFECTIVE_BALANCE_INCREMENT config) (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) \<and>
(safe_mul (word_of_nat f div EFFECTIVE_BALANCE_INCREMENT config) (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) \<longrightarrow>
P ((map (\<lambda>effective_balance.
word_of_nat effective_balance div EFFECTIVE_BALANCE_INCREMENT config * (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)))
(local.range 0 (unat (MAX_EFFECTIVE_BALANCE + EFFECTIVE_BALANCE_INCREMENT config)) (unat (EFFECTIVE_BALANCE_INCREMENT config))))) s))))) )))
(bindCont compute_base_rewards c) Q"
apply (clarsimp simp: compute_base_rewards_def, rule hoare_weaken_pre)
apply (simp only: bindCont_assoc[symmetric])
apply (rule read_beacon_wp)
apply (rule add_wp')
apply (rule mapM_wp'[where g="(\<lambda>effective_balance. of_nat effective_balance div EFFECTIVE_BALANCE_INCREMENT config * (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)))" for f])
apply (erule get_base_reward_fast_wp)
apply (intro conjI impI; clarsimp?)
apply (fastforce)
apply (clarsimp)
apply (erule sep_conj_impl, assumption)
apply (sep_cancel)+
apply (sep_mp)
apply (subgoal_tac "list.set (local.range 0 (unat (MAX_EFFECTIVE_BALANCE + EFFECTIVE_BALANCE_INCREMENT config)) (unat (EFFECTIVE_BALANCE_INCREMENT config))) \<noteq> {}")
apply (clarsimp simp: nonempty_ball_conj_lift nonempty_ball_imp_lift)
apply (erule_tac x=0 in ballE; clarsimp?)
apply (clarsimp simp: range_empty_iff)
by (metis EBI_ge_zero add_0 effective_balance_safe neq_0_no_wrap unat_0 unat_gt_0 unat_mono)
abbreviation "map_var f vs \<equiv> map f (var_list_inner vs)"
definition "base_rewards_from_cache pbc \<equiv>
map (\<lambda>effective_balance. word_of_nat effective_balance div EFFECTIVE_BALANCE_INCREMENT config *
(EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)))
(local.range 0 (unat (MAX_EFFECTIVE_BALANCE + EFFECTIVE_BALANCE_INCREMENT config)) (unat (EFFECTIVE_BALANCE_INCREMENT config)))"
schematic_goal new_base_rewards_cache_wp:
"(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple (lift (validators \<mapsto>\<^sub>l vs \<and>* progressive_balances_cache \<mapsto>\<^sub>l pbc \<and>*
(validators \<mapsto>\<^sub>l vs \<and>* progressive_balances_cache \<mapsto>\<^sub>l pbc \<longrightarrow>*
(\<lambda>s. total_active_balance_f pbc < total_active_balance_f pbc + 1 \<and>
(total_active_balance_f pbc < total_active_balance_f pbc + 1 \<longrightarrow>
total_active_balance_f pbc \<noteq> 0 \<and>
(total_active_balance_f pbc \<noteq> 0 \<longrightarrow>
(\<forall>f\<in>list.set (local.range 0 (unat (MAX_EFFECTIVE_BALANCE + EFFECTIVE_BALANCE_INCREMENT config)) (unat (EFFECTIVE_BALANCE_INCREMENT config))).
safe_mul (word_of_nat f div EFFECTIVE_BALANCE_INCREMENT config) (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) \<and>
(safe_mul (word_of_nat f div EFFECTIVE_BALANCE_INCREMENT config) (EFFECTIVE_BALANCE_INCREMENT config * BASE_REWARD_FACTOR config div sqrt' (total_active_balance_f pbc)) \<longrightarrow>
P \<lparr>effective_balances_f = map_var Validator.effective_balance_f vs,
base_rewards_f = base_rewards_from_cache pbc \<rparr> s))))))))
(bindCont new_base_rewards_cache c) Q"
apply (clarsimp simp: new_base_rewards_cache_def)
apply (rule hoare_weaken_pre, simp only: bindCont_assoc[symmetric])
apply (wp)
apply (clarsimp)
apply (rule exI)
apply (sep_cancel)
apply (sep_cancel)+
apply (sep_mp)
apply (clarsimp)
apply (clarsimp simp: base_rewards_from_cache_def)
done
lemma get_total_active_balance_wp[wp]:"(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple (lift (beacon_slots \<mapsto>\<^sub>l b_s \<and>* validators \<mapsto>\<^sub>l vs \<and>*
(beacon_slots \<mapsto>\<^sub>l b_s \<and>* validators \<mapsto>\<^sub>l vs \<longrightarrow>*
(\<lambda>s. (\<forall>x\<in>list.set (active_validator_indices (slot_to_epoch config b_s) vs). x < var_list_len vs) \<and>
((\<forall>x\<in>list.set (active_validator_indices (slot_to_epoch config b_s) vs). x < var_list_len vs) \<longrightarrow>
(\<forall>xs\<in>lists_of (list.set (active_validator_indices (slot_to_epoch config b_s) vs)).
P (max (EFFECTIVE_BALANCE_INCREMENT config)
(\<Sum>a\<leftarrow>xs. Validator.effective_balance_f (unsafe_var_list_index vs a))) s) )))))
(bindCont get_total_active_balance c) Q"
apply (clarsimp simp: get_total_active_balance_def, rule hoare_weaken_pre, wp, clarsimp)
apply (sep_cancel)+
apply (sep_mp, clarsimp)
done
abbreviation "current_epoch bs \<equiv> slot_to_epoch config bs"
definition "unslashed_participating_indices flag_index epoch epoch_participation vs \<equiv>
{x \<in> list.set (active_validator_indices epoch vs).
has_flag (unsafe_var_list_index epoch_participation x) flag_index \<and>
\<not> slashed_f (unsafe_var_list_index vs x)} "
lemma get_flag_attesting_balance_current_epoch_wp:
"(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple (lift (beacon_slots \<mapsto>\<^sub>l b_s \<and>* current_epoch_participation \<mapsto>\<^sub>l cep \<and>*
validators \<mapsto>\<^sub>l vs \<and>*
(beacon_slots \<mapsto>\<^sub>l b_s \<and>* current_epoch_participation \<mapsto>\<^sub>l cep \<and>*
validators \<mapsto>\<^sub>l vs \<longrightarrow>*
(\<lambda>s. epoch = current_epoch b_s \<and>
(\<forall>x\<in>(unslashed_participating_indices flag_index epoch cep vs ). x < var_list_len vs) \<and>
(epoch = current_epoch b_s \<longrightarrow>
(\<forall>x\<in>(unslashed_participating_indices flag_index epoch cep vs ). x < var_list_len vs) \<longrightarrow>
(\<forall>xs\<in>lists_of (unslashed_participating_indices flag_index epoch cep vs).
P (max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xs. Validator.effective_balance_f (unsafe_var_list_index vs a))) s))))))
(bindCont (get_flag_attesting_balance flag_index epoch) c) Q"
apply (clarsimp simp: get_flag_attesting_balance_def, rule hoare_weaken_pre)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule hoare_eqI'[where v=epoch], rule get_current_unslashed_participating_indices_wp, wp)
apply (rule lift_mono')
apply (clarsimp)
apply (intro conjI)
apply (sep_mp)
apply (blast)
apply (clarsimp)
apply (sep_cancel)+
apply (sep_mp)
apply (clarsimp simp: unslashed_participating_indices_def)
done
lemma get_flag_attesting_balance_previous_epoch_wp:
"(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow> current_epoch b_s \<noteq> GENESIS_EPOCH \<Longrightarrow>
hoare_triple (lift (beacon_slots \<mapsto>\<^sub>l b_s \<and>* previous_epoch_participation \<mapsto>\<^sub>l pep \<and>* current_epoch_participation \<mapsto>\<^sub>l cep \<and>*
validators \<mapsto>\<^sub>l vs \<and>*
(beacon_slots \<mapsto>\<^sub>l b_s \<and>* previous_epoch_participation \<mapsto>\<^sub>l pep \<and>* current_epoch_participation \<mapsto>\<^sub>l cep \<and>*
validators \<mapsto>\<^sub>l vs \<longrightarrow>*
(\<lambda>s. epoch = previous_epoch (slot_to_epoch config b_s) \<and>
(\<forall>x\<in>(unslashed_participating_indices flag_index epoch pep vs). x < var_list_len vs) \<and>
(epoch = previous_epoch (slot_to_epoch config b_s) \<longrightarrow>
(\<forall>x\<in>(unslashed_participating_indices flag_index epoch pep vs). x < var_list_len vs) \<longrightarrow>
(\<forall>xs\<in>lists_of (unslashed_participating_indices flag_index epoch pep vs).
P (max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xs. Validator.effective_balance_f (unsafe_var_list_index vs a))) s))))))
(bindCont (get_flag_attesting_balance flag_index epoch) c) Q"
apply (clarsimp simp: get_flag_attesting_balance_def, rule hoare_weaken_pre)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule hoare_eqI'[where v=epoch], rule get_previous_unslashed_participating_indices_wp, wp)
apply (rule lift_mono')
apply (clarsimp)
apply (intro conjI)
apply (sep_mp)
apply (blast)
apply (clarsimp)
apply (sep_cancel)+
apply (sep_mp)
apply (clarsimp simp: unslashed_participating_indices_def)
done
lemma [simp]: "(Invariants.var_list_inner vs) = (var_list_inner vs)"
by (case_tac vs; clarsimp)
lemma new_progressive_balances_wp: "(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple (lift (beacon_slots \<mapsto>\<^sub>l b_s \<and>* validators \<mapsto>\<^sub>l vs \<and>*
current_epoch_participation \<mapsto>\<^sub>l cep \<and>*
previous_epoch_participation \<mapsto>\<^sub>l pep \<and>*
(beacon_slots \<mapsto>\<^sub>l b_s \<and>* validators \<mapsto>\<^sub>l vs \<and>*
current_epoch_participation \<mapsto>\<^sub>l cep \<and>*
previous_epoch_participation \<mapsto>\<^sub>l pep \<longrightarrow>*
(\<lambda>s.(\<exists>ep. ep = (if (current_epoch b_s) = GENESIS_EPOCH then cep else pep) \<and>
(\<forall>xs \<in> lists_of (list.set (active_validator_indices (current_epoch b_s) vs)).
\<forall>xsa \<in> lists_of (unslashed_participating_indices TIMELY_SOURCE_FLAG_INDEX (previous_epoch (current_epoch b_s)) ep vs).
\<forall>xsb \<in> lists_of (unslashed_participating_indices TIMELY_TARGET_FLAG_INDEX (previous_epoch (current_epoch b_s)) ep vs).
\<forall>xsc \<in> lists_of (unslashed_participating_indices TIMELY_HEAD_FLAG_INDEX (previous_epoch (current_epoch b_s)) ep vs).
\<forall>xsd \<in> lists_of (unslashed_participating_indices TIMELY_SOURCE_FLAG_INDEX (current_epoch b_s) cep vs).
\<forall>xse \<in> lists_of (unslashed_participating_indices TIMELY_TARGET_FLAG_INDEX (current_epoch b_s) cep vs).
\<forall>xsf \<in> lists_of (unslashed_participating_indices TIMELY_HEAD_FLAG_INDEX (current_epoch b_s) cep vs).
P (ProgressiveBalancesCache.fields (max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xs. Validator.effective_balance_f (unsafe_var_list_index vs a)))
[max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xsa. Validator.effective_balance_f (unsafe_var_list_index vs a)),
max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xsb. Validator.effective_balance_f (unsafe_var_list_index vs a)),
max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xsc. Validator.effective_balance_f (unsafe_var_list_index vs a))]
[max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xsd. Validator.effective_balance_f (unsafe_var_list_index vs a)),
max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xse. Validator.effective_balance_f (unsafe_var_list_index vs a)),
max (EFFECTIVE_BALANCE_INCREMENT config) (\<Sum>a\<leftarrow>xsf. Validator.effective_balance_f (unsafe_var_list_index vs a))]) s))))))
(bindCont new_progressive_balances c) Q"
apply (case_tac "current_epoch b_s = GENESIS_EPOCH")
defer
apply (clarsimp simp: new_progressive_balances_def, rule hoare_weaken_pre)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule get_total_active_balance_wp[where b_s=b_s])
apply (rule get_previous_epoch_wp[where v=b_s])
apply (rule get_current_epoch_wp[where v=b_s])
apply (rule get_flag_attesting_balance_previous_epoch_wp[where b_s=b_s])
apply (rule get_flag_attesting_balance_previous_epoch_wp[where b_s=b_s])
apply (rule get_flag_attesting_balance_previous_epoch_wp[where b_s=b_s])
apply (rule get_flag_attesting_balance_current_epoch_wp[where b_s=b_s])+
apply (fastforce)
apply (clarsimp)
prefer 3
apply (clarsimp)
apply (sep_cancel)+
apply (safe; clarsimp?)
apply (erule active_validator_indices_are_bound)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_drule (direct) val_length_wf)
apply (clarsimp)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_cancel)+
apply (intro conjI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (erule active_validator_indices_are_bound)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_drule (direct) val_length_wf)
apply (clarsimp)
apply (intro conjI impI ballI)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (erule active_validator_indices_are_bound)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_drule (direct) val_length_wf)
apply (clarsimp)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (erule active_validator_indices_are_bound)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_drule (direct) val_length_wf)
apply (clarsimp)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (sep_cancel)+
apply (intro conjI impI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (intro conjI impI ballI)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_mp)
apply (erule_tac x=xs in ballE)
apply (erule_tac x=xsa in ballE)
apply (erule_tac x=xsb in ballE)
apply (erule_tac x=xsc in ballE)
apply (erule_tac x=xsd in ballE)
apply (erule_tac x=xse in ballE)
apply (erule_tac x=xsf in ballE)
apply (assumption)
apply (clarsimp)+
apply (clarsimp simp: new_progressive_balances_def, rule hoare_weaken_pre)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule get_total_active_balance_wp[where b_s=b_s])
apply (rule get_previous_epoch_wp[where v=b_s])
apply (rule get_current_epoch_wp[where v=b_s])
apply (rule get_flag_attesting_balance_current_epoch_wp[where b_s=b_s])+
apply (fastforce)
apply (clarsimp)
apply (sep_cancel)+
apply (safe; clarsimp?)
apply (erule active_validator_indices_are_bound)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_drule (direct) val_length_wf)
apply (clarsimp)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (sep_cancel)+
apply (intro conjI impI ballI)
apply (clarsimp simp: unslashed_participating_indices_def)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_mp)
apply (clarsimp)
done
lemma new_rewards_and_penalties_context_wp[wp]:"(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple
(lift (progressive_balances_cache \<mapsto>\<^sub>l pbc \<and>*
(\<lambda>s. (\<forall>x\<in>list.set (local.range 0 (unat NUM_FLAG_INDICES) (Suc 0)). x < length (previous_epoch_flag_attesting_balances_f pbc)) \<and>
((\<forall>x\<in>list.set (local.range 0 (unat NUM_FLAG_INDICES) (Suc 0)). x < length (previous_epoch_flag_attesting_balances_f pbc)) \<longrightarrow>
(progressive_balances_cache \<mapsto>\<^sub>l pbc \<longrightarrow>*
P (RewardsAndPenaltiesContext.fields (map (\<lambda>a. previous_epoch_flag_attesting_balances_f pbc ! a div EFFECTIVE_BALANCE_INCREMENT config) (local.range 0 (unat NUM_FLAG_INDICES) (Suc 0)))
(total_active_balance_f pbc div EFFECTIVE_BALANCE_INCREMENT config)))s
))))
(bindCont (new_rewards_and_penalties_context pbc) c) Q"
apply (unfold new_rewards_and_penalties_context_def)
apply (rule hoare_weaken_pre)
apply (simp only: bindCont_assoc[symmetric])
apply (rule mapM_wp_foldr')
apply (clarsimp simp: unslashed_participating_increment_def liftM_def comp_def)
apply (simp only: bindCont_assoc[symmetric])
apply (rule read_beacon_wp[where v=pbc])
apply (wp)
apply (clarsimp)
apply (rule factor_foldr_sep)
prefer 2
apply (clarsimp simp: mono_def)
apply blast
defer
apply (intro ext iffI; clarsimp)
apply (sep_cancel)
apply (rule factor_foldr_pure)
apply (clarsimp)
by (clarsimp)
lemma safe_mul_one[simp]: "safe_mul 1 (x :: u64)"
apply (clarsimp simp: safe_mul_def)
using div_word_self by blast
lemma new_effective_balances_ctxt_wp[wp]:
"(\<And>x. hoare_triple (lift (P x)) (c x) Q) \<Longrightarrow>
hoare_triple
(lift (P \<lparr> downward_threshold_f =
(EFFECTIVE_BALANCE_INCREMENT config div HYSTERESIS_QUOTIENT),
upward_threshold_f =
(EFFECTIVE_BALANCE_INCREMENT config div HYSTERESIS_QUOTIENT * HYSTERESIS_UPWARD_MULTIPLIER)\<rparr>))