-
Notifications
You must be signed in to change notification settings - Fork 1
/
Process_Epoch_O_Specs.thy
2058 lines (1752 loc) · 104 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
begin
locale extended_hl_pre = extended_vc + hoare_logic
begin
declare [[show_sorts=false]]
declare [[show_types=false]]
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 (erule lift_mono, clarsimp, 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 sub_wp[wp]: "hoare_triple (lift (P (n - m))) (c (n - m)) Q \<Longrightarrow>
hoare_triple (lift (\<lambda>s. n \<ge> m \<and> (n \<ge> m \<longrightarrow> P (n - m) s)))
(do {x <- (n .- m); c x}) Q"
apply (rule hoare_weaken_pre)
apply (clarsimp simp: word_unsigned_sub_def )
apply (simp only: Let_unfold)
apply (wp, clarsimp simp: bindCont_return')
apply (safe)
by (simp add: word_sub_le_iff)
apply (erule notE)
apply (clarsimp simp: lift_def)
using word_sub_le_iff by blast
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 if_wp[wp]:
"(B \<Longrightarrow> hoare_triple ( lift S) ( bindCont P c) R) \<Longrightarrow> (\<not>B \<Longrightarrow> hoare_triple ( lift S') (bindCont Q c) R) \<Longrightarrow>
hoare_triple ( lift (if B then S else S')) (do {x <- (if B then P else Q); c x}) R"
apply (clarsimp split: if_splits)
done
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
definition "previous_epoch epoch \<equiv>
if epoch = GENESIS_EPOCH then GENESIS_EPOCH else Epoch (epoch_to_u64 epoch - 1)"
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)
declare lift_mono[elim!]
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 (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 add_zero_simp:"(bindCont ((a :: u64) .+ (0 :: u64)) f) = f a" sorry
lemma unsigned_add_commute[intro]:" word_unsigned_add b a = a .+ b "
apply (rule ext; clarsimp simp: Let_unfold word_unsigned_add_def)
apply (safe; clarsimp simp: add.commute)
using olen_add_eqv apply auto[1]
using olen_add_eqv apply auto[1]
done
lemma unsigned_word_add_shuffle:" bindCont (word_unsigned_add a n) (\<lambda>y. bindCont (b .+ y) f) = bindCont (b .+ n) (\<lambda>y. bindCont ( a .+ y) f) "
apply (clarsimp simp: word_unsigned_add_def Let_unfold, safe; (clarsimp simp: bindCont_return' bindCont_return split: if_splits)?)
apply (simp add: add.left_commute)
using olen_add_eqv word_random apply blast
using olen_add_eqv word_random apply blast
apply (metis add.left_commute le_no_overflow)
by (simp add: add.left_commute le_no_overflow)
lemma foldrM_elems_cons: "foldrM word_unsigned_add ([a,b]) n = foldrM word_unsigned_add ([b,a]) n"
apply (clarsimp simp: foldrM_cons)
using unsigned_word_add_shuffle
by (metis bindCont_assoc bindCont_return)
lemma word_unsigned_add_shuffle2: "bindCont (word_unsigned_add x y) (\<lambda>x. x .+ z) = bindCont (x .+ z) (\<lambda>x. x .+ y)"
apply (clarsimp simp: word_unsigned_add_def Let_unfold, safe; (clarsimp simp: bindCont_return' bindCont_return split: if_splits)?)
apply (simp add: add.commute add.left_commute)
apply (smt (verit, ccfv_threshold) no_olen_add word_le_def)
apply (metis (no_types, lifting) add.commute olen_add_eqv word_random)
apply (metis add.assoc add.commute olen_add_eqv word_plus_mono_right)
by (metis (no_types, opaque_lifting) add.commute group_cancel.add2 nle_le olen_add_eqv word_add_increasing word_plus_mcs_4')
lemma foldrM_shift: "foldrM word_unsigned_add (a#xs) n = (do {x <- foldrM word_unsigned_add (xs) n; word_unsigned_add x a}) "
apply (induct xs arbitrary: n a; clarsimp?)
apply (clarsimp simp: foldrM_def bindCont_return' k_comp_def bindCont_return)
apply (rule unsigned_add_commute)
apply (clarsimp simp: foldrM_cons)
apply (clarsimp simp: bindCont_assoc)
apply (subst bindCont_assoc[symmetric])
apply (subst bindCont_assoc[symmetric])
apply (rule bindCont_right_eqI)
apply (rule word_unsigned_add_shuffle2)
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
definition "lists_of S \<equiv> {xs. distinct xs \<and> list.set xs = S}"
lemma maps_to_is_valid:"(maps_to l v \<and>* R) s \<Longrightarrow> valid (l) (Some v)"
apply (clarsimp simp: sep_conj_def maps_to_def )
sorry
lemma valid_validator_some_simp[simp]:
"valid validators (Some xs) = (let ys = Invariants.var_list_inner xs in sum_list (map (unat o Validator.effective_balance_f) ys) < 2^(64) \<and> distinct ys \<and> length ys < 2^64 )"
apply (clarsimp simp: validators_def)
sorry
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[where x=a]) 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)
find_theorems select
lemma select_wp_lift[wp]: "(\<And>x. x \<in> P \<Longrightarrow> hoare_triple (lift (pre x)) (f x) Q) \<Longrightarrow> hoare_triple (lift (\<lambda>s. \<forall>x\<in>P. pre x s)) (do {x <- select P; f x}) Q"
apply (clarsimp simp: select_def bindCont_def hoare_triple_def run_def)
apply (subst Sup_le_iff)
apply (clarsimp)
apply (atomize, erule allE, drule mp, assumption)
apply (erule order_trans)
apply (rule seq_mono_left)
by (subst assert_iso[symmetric], clarsimp)
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=aa in allE)
apply (erule_tac x=a in allE)
apply (fastforce)
apply (clarsimp)
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 lift_option_wp[wp]: "(\<And>x. v = Some x \<Longrightarrow> hoare_triple (lift (P x)) (f x) Q) \<Longrightarrow>
hoare_triple (lift (\<lambda>s. v \<noteq> None \<and> (v \<noteq> None \<longrightarrow> P (the v) s))) (do {b <- lift_option v; f b}) Q"
apply (unfold lift_option_def)
apply (rule hoare_assert_stateI, clarsimp)
apply (intro conjI impI)
apply (clarsimp simp: lift_def)
apply (clarsimp simp: lift_def)
apply (rule hoare_weaken_pre, assumption)
apply (clarsimp)
apply (clarsimp simp: lift_def)
apply (blast)
done
lemma getState_wp_spec[wp]: " (\<And>s. hoare_triple (P s) (c s) Q) \<Longrightarrow>
hoare_triple (\<lambda>x. P x x) (bindCont getState c) Q"
apply (clarsimp simp: getState_def hoare_triple_def bindCont_def run_def Sup_le_iff assert_galois_test test_restricts_Nondet)
apply (atomize)
apply (erule_tac x=a in allE)
apply (erule_tac x=b in allE)
apply (erule order_trans[rotated])
using seq_mono_left test.hom_mono by force
lemma getState_wp_alt: "(\<And>s. P s \<Longrightarrow> hoare_triple ((=) s) (c s) Q) \<Longrightarrow>
hoare_triple P (bindCont getState c) Q "
by (clarsimp simp: getState_def hoare_triple_def bindCont_def run_def Sup_le_iff assert_galois_test test_restricts_Nondet)
lemma hoare_subgoalI: "(\<And>s. P \<Longrightarrow> hoare_triple P' f Q) \<Longrightarrow> hoare_triple (\<lambda>s. P \<and> (P \<longrightarrow> P' s)) f Q"
apply (rule hoare_assert_stateI)
apply (rule hoare_weaken_pre)
apply (clarsimp)
apply (assumption)
apply (clarsimp)
done
lemma [simp]: "((\<lambda>a. the (u64_of a)) \<circ> u64) = id "
by (intro ext; clarsimp)
text \<open>lemma translate_ProgressiveBalancesCacheI:"(extended_vc.maps_to current_epoch_flag_attesting_balances (list (map u64 (current_epoch_flag_attesting_balances_f pbc))) \<and>*
extended_vc.maps_to previous_epoch_flag_attesting_balances (list (map u64 (previous_epoch_flag_attesting_balances_f pbc))) \<and>*
extended_vc.maps_to total_active_balance (u64 (total_active_balance_f pbc)) \<and>*
extended_vc.maps_to progressive_balances_cache (list [ptr total_active_balance, ptr previous_epoch_flag_attesting_balances, ptr current_epoch_flag_attesting_balances])) s \<Longrightarrow> translate_ProgressiveBalancesCache progressive_balances_cache pbc s"
apply (clarsimp simp: translate_ProgressiveBalancesCache_def)
apply (intro exI)
apply (sep_solve)
done
\<close>
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)
text \<open>lemma read_ProgressiveBalancesCache_wp[wp]:"hoare_triple (P pbc) (f pbc) Q \<Longrightarrow>
hoare_triple (translate_ProgressiveBalancesCache progressive_balances_cache pbc \<and>* (translate_ProgressiveBalancesCache progressive_balances_cache pbc \<longrightarrow>* P (pbc)))
(do {b <- read_ProgressiveBalancesCache progressive_balances_cache; f b}) Q"
apply (rule hoare_assert_stateI)
apply (subst (asm) translate_ProgressiveBalancesCache_def)
apply (clarsimp simp: sep_conj_exists1)
find_theorems "((\<lambda>s. \<exists>x. ?f x s) \<and>* ?R)"
apply (rule hoare_weaken_pre, unfold read_ProgressiveBalancesCache_def, wp)
apply (rule_tac v=xb and x="(map u64 (previous_epoch_flag_attesting_balances_f pbc))" in hoare_eqI)
apply (simp)
apply (wp)
apply (rule mapM_wp[where g="the o u64_of"])
apply (simp only: comp_def)
apply (rule_tac v="(u64_of xc)" in lift_option_wp)
apply (clarsimp)
apply (assumption)
apply (clarsimp)
apply (erule hoare_eqI)
apply (wp)
apply (rule_tac v=xc and x="(map u64 (current_epoch_flag_attesting_balances_f pbc))" in hoare_eqI)
apply (rule mapM_wp[where g="the o u64_of"])
apply (simp only: comp_def)
apply (rule_tac v="(u64_of xd)" in lift_option_wp)
apply (clarsimp)
apply (assumption)
apply (clarsimp)
apply (clarsimp)
apply (erule hoare_eqI)
apply (clarsimp)
apply (safe)
apply (sep_cancel)+
apply (clarsimp)
apply (sep_cancel)+
apply (clarsimp)
apply (intro conjI impI; clarsimp?)
apply (sep_cancel)+
apply clarsimp
apply (intro conjI impI)
apply (sep_drule translate_ProgressiveBalancesCacheI, assumption)
apply (sep_drule translate_ProgressiveBalancesCacheI, assumption)
apply (sep_cancel)+
apply (intro conjI impI)
apply (sep_drule translate_ProgressiveBalancesCacheI, assumption)
apply (sep_drule translate_ProgressiveBalancesCacheI, assumption)
apply (clarsimp)
done
\<close>
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)
apply (wp)
apply (safe)
apply (sep_cancel)+
apply (clarsimp)
apply (sep_cancel)+
done
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 [simp]: "Epoch x \<le> Epoch y \<longleftrightarrow> x \<le> y"
by (safe; clarsimp simp: less_eq_Epoch_def)
lemma [simp]: "epoch_to_u64 GENESIS_EPOCH = 0"
by (clarsimp simp: GENESIS_EPOCH_def)
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 div_wp_lift: "hoare_triple (lift (P (n div m))) (c (n div m)) Q \<Longrightarrow>
hoare_triple (lift (\<lambda>s. m \<noteq> 0 \<and> (m \<noteq> 0 \<longrightarrow> (P ( n div m)) s)))
(do {x <- (word_unsigned_div n m); c x}) Q"
apply (rule hoare_weaken_pre)
apply (unfold word_unsigned_div_def, wp)
apply (clarsimp simp: bindCont_return')
apply (clarsimp simp: lift_def)
done
find_theorems name:div_wp
lemma [simp]: "CHURN_LIMIT_QUOTIENT config \<noteq> 0" sorry
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 (rule div_wp_lift)
apply (rule return_wp)
apply (clarsimp)
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)
apply (rule div_wp_lift)
apply (fastforce)
apply (clarsimp)
apply (sep_cancel)+
done
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 (rule div_wp_lift)
apply (rule return_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 (rule div_wp_lift)
apply (assumption)
apply (clarsimp)
apply (sep_cancel)+
apply (sep_mp)
apply (sep_cancel)+
done
lemma [simp]: "\<lless>\<lambda>s. P\<then> = (\<lambda>s. P)"
apply (intro ext, clarsimp simp: lift_def)
apply (safe)
apply (rule_tac x="id_p" in exI)
by simp
lemma add_wp[wp]: "hoare_triple (lift (P (n + m))) (c (n + m)) Q \<Longrightarrow>
hoare_triple (lift (\<lambda>s. n \<le> n + m \<and> (n \<le> n + m \<longrightarrow> P (n + m) s)))
(do {x <- (word_unsigned_add n m); c x}) Q"
apply (rule hoare_weaken_pre)
apply (clarsimp simp: word_unsigned_add_def )
apply (simp only: Let_unfold)
apply (wp, clarsimp simp: bindCont_return')
done
lemma mod_wp[wp]: "hoare_triple (lift (P (n mod m))) (c (n mod m)) Q \<Longrightarrow>
hoare_triple (lift (\<lambda>s. m \<noteq> 0 \<and> (m \<noteq> 0 \<longrightarrow> P (n mod m) s)))
(do {x <- (n .% m); c x}) Q"
apply (rule hoare_weaken_pre)
apply (unfold word_unsigned_mod_def)
apply wp
apply fastforce
done
find_theorems name:if_wp
thm wp
lemma when_wp[wp]:
"(B \<Longrightarrow> hoare_triple ( lift S) ( bindCont P c) R) \<Longrightarrow> (\<not>B \<Longrightarrow> hoare_triple ( lift S') (c ()) R) \<Longrightarrow>
hoare_triple ( lift (if B then S else S')) (do {x <- (when B P); c x}) R"
apply (clarsimp split: if_splits)
done
definition "next_epoch b_slots \<equiv> epoch_to_u64 (slot_to_epoch config b_slots) + 1"
lemma SLOTS_PER_EPOCH_ATLEAST[simp]: "1 < SLOTS_PER_EPOCH config" sorry
lemma EPOCHS_PER_ETH1_VOTING_PERIOD_ATLEAST[simp]: "EPOCHS_PER_ETH1_VOTING_PERIOD config \<noteq> 0" sorry
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 bits_div_0 div_less_dividend_word less_is_non_zero_p1 lt1_neq0 olen_add_eqv word_less_1 zero_neq_one)
apply (clarsimp)
apply (clarsimp)
apply (clarsimp simp: next_epoch_def)
by (sep_cancel)+
thm get_previous_epoch_wp
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 (intro conjI impI)
apply (clarsimp)
apply (clarsimp simp: previous_epochs_def)
using less_eq_Epoch_def apply blast
apply (clarsimp)
apply (sep_mp)
apply (clarsimp simp: raw_epoch_simp)
apply (clarsimp simp: raw_epoch_simp)
done
abbreviation (input) "sep_wp pre post P \<equiv> (lift (pre \<and>* (post \<longrightarrow>* P)))"
lemma lift_pure_conj[simp]: "lift (\<lambda>s. P \<and> Q s) s = (P \<and> lift Q s)"
by (clarsimp simp: lift_def)
lemma lift_pure_imp[simp]: "lift (\<lambda>s. P \<longrightarrow> Q s) s = (P \<longrightarrow> lift Q s)"
apply (clarsimp simp: lift_def)
apply (safe, blast)
apply (rule_tac x=id_p in exI)
apply (clarsimp)
apply (blast)
done
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 add.commute
bits_div_0 div_less_dividend_word inc_i le_no_overflow lt1_neq0
verit_comp_simplify1(2) word_le_not_less)
lemma subst_in_impl: "(x = y \<longrightarrow> f y) = (x = y \<longrightarrow> f x)"
by (safe)
lemma hoare_eqI': "hoare_triple (lift (P x)) (f x) Q \<Longrightarrow> hoare_triple (lift (\<lambda>s. v = x \<and> (v = x \<longrightarrow> P v s))) (f v) Q"
apply (rule hoare_assert_stateI)
apply (clarsimp)
apply (clarsimp simp: lift_def)
apply (erule hoare_weaken_pre)
apply (clarsimp simp: lift_def)
apply (blast)
done
lemma hoare_eqI'': "hoare_triple (lift (P x v)) (f x) Q \<Longrightarrow> hoare_triple (lift (\<lambda>s. v = x \<and> (v = x \<longrightarrow> P x v s))) (f v) Q"
apply (rule hoare_assert_stateI)
apply (clarsimp)
apply (clarsimp simp: lift_def)
apply (erule hoare_weaken_pre)
apply (clarsimp simp: lift_def)
apply (blast)
done
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
definition "safe_mul m n \<equiv> if (m = 0 \<or> n = 0) then True else (m * n div n = m)"
lemma fail_wp[wp]: "\<lblot>lift \<bottom>\<rblot> bindCont fail c \<lblot>Q\<rblot>"
apply (rule hoare_weaken_pre, wp)
apply (clarsimp simp: lift_def)
done
thm mul_wp
lemma mul_wp[wp]: "hoare_triple (lift (P (n * m))) (c (n * m)) Q \<Longrightarrow>
hoare_triple (lift (\<lambda>s. safe_mul m n \<and> (safe_mul m n \<longrightarrow> P (n * m) s)))
(do {x <- (word_unsigned_mul n m); c x}) Q"
apply (rule hoare_weaken_pre)
apply (unfold word_unsigned_mul_def )
apply (simp only: Let_unfold)
apply (rule if_wp, simp)
apply (fastforce)
apply (rule if_wp, simp)
apply (wp)
apply (clarsimp simp: safe_mul_def)
apply (intro conjI impI; clarsimp?)
by (simp add: mult.commute)
lemma div_wp[wp]: "hoare_triple (lift (P (n div m))) (c (n div m)) Q \<Longrightarrow>
hoare_triple (lift (\<lambda>s. m \<noteq> 0 \<and> (m \<noteq> 0 \<longrightarrow> P ( n div m) s)))
(do {x <- (word_unsigned_div n m); c x}) Q"
apply (rule hoare_weaken_pre)
apply (unfold word_unsigned_div_def, wp)
apply (clarsimp simp: bindCont_return')
done
lemma slashings_wf: "(slashings \<mapsto>\<^sub>l ss \<and>* R) s \<Longrightarrow>
sum_list (map unat (local.vector_inner ss)) \<le> 2 ^ 64 - 1 \<and>
PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX = sum_list (local.vector_inner ss) *
PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX div sum_list (local.vector_inner ss)"
sorry
schematic_goal new_slashings_context_wp[wp]:
"hoare_triple (lift (P x)) (c x) Q \<Longrightarrow> hoare_triple (lift (slashings \<mapsto>\<^sub>l ss \<and>* ?R)) (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 (frule slashings_wf)
apply (erule sep_conj_impl, assumption)
apply (clarsimp)
apply (assumption)
done
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 (sep_mp, clarsimp)
done
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 (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 mapM_wp'':
assumes c_wp: "\<And>(f :: 'e \<Rightarrow> ('f, 'a) cont) x P Q. (\<And>xs. hoare_triple (lift (P (g x))) (f (g x)) ( Q)) \<Longrightarrow> hoare_triple (lift (pre x)) (do { b <- c x; f b}) Q"
shows " (\<And>x y. hoare_triple (lift (P x)) (f y) Q) \<Longrightarrow> hoare_triple (lift (\<lambda>s. (\<forall>x\<in>list.set xs. pre x s) \<and> ((\<forall>x\<in>list.set xs. pre x s) \<longrightarrow> P (map g xs) s))) (do {vs <- mapM c (xs :: 'd list) ; (f :: 'e list \<Rightarrow> ('f, 'a) cont) (vs )}) Q"
apply (induct xs arbitrary: f)
apply (simp)
apply (clarsimp)
apply (rule hoare_weaken_pre)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule c_wp)
defer
apply (clarsimp)
defer
apply (atomize)
apply (erule_tac x="(\<lambda>aa. f (g a # aa))" in allE)
apply (drule mp)
apply (clarsimp)
apply (fastforce)
done
thm mapM_wp
term "foldr (\<lambda>x R. pre' R x) xs"
lemma mapM_wp_foldr:
assumes c_wp: "\<And>(f :: 'e \<Rightarrow> ('f, 'a) cont) x P Q. (\<And>x. hoare_triple (lift (P)) (f x) (Q)) \<Longrightarrow> hoare_triple (lift (pre P x)) (do { b <- c x; f b}) Q"
shows " (\<And>x. hoare_triple (lift (P)) (f x) Q) \<Longrightarrow> hoare_triple (lift (foldr (\<lambda>x R. pre R x) xs P )) (do {vs <- mapM c (xs :: 'd list) ; (f :: 'e list \<Rightarrow> ('f, 'a) cont) (vs )}) Q"
apply (induct xs arbitrary: f; clarsimp)
by (metis (no_types, lifting) bindCont_assoc c_wp return_triple')
lemma mapM_wp':
assumes c_wp: "\<And>(f :: 'e \<Rightarrow> ('f, 'a) cont) x P Q. hoare_triple (lift P) (f (g x)) ( Q) \<Longrightarrow> hoare_triple (lift (pre P x)) (do { b <- c x; f b}) Q"
assumes pre_mono: "(\<And>x P Q s . (P s \<Longrightarrow> Q s) \<Longrightarrow> (pre P x) s \<Longrightarrow> (pre Q x) s )"
shows " hoare_triple (lift P) (f (map g xs)) Q \<Longrightarrow> hoare_triple (lift (\<lambda>s. (\<Sqinter>x\<in>(list.set xs). pre P x) s \<and> ((\<Sqinter>x\<in>(list.set xs). pre P x) s \<longrightarrow> P s))) (do {vs <- mapM c (xs :: 'd list) ; (f :: 'e list \<Rightarrow> ('f, 'a) cont) (vs )}) Q"
apply (induct xs arbitrary: f; clarsimp)
apply (atomize)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule hoare_weaken_pre)
apply (rule c_wp)
apply (erule allE)
apply (erule impE)
defer
apply (assumption)
apply (clarsimp)
apply (rule pre_mono[rotated], assumption)
apply (clarsimp)
apply (clarsimp)
done
lemma ebi_not_zero[intro]: "EFFECTIVE_BALANCE_INCREMENT config \<noteq> 0" sorry
lemma brf_ebi_times_bounded[simp]:
"EFFECTIVE_BALANCE_INCREMENT config *
BASE_REWARD_FACTOR config div EFFECTIVE_BALANCE_INCREMENT config =
BASE_REWARD_FACTOR config" sorry
lemma sqrt_eq_zero_iff[simp]: "sqrt' x = 0 \<longleftrightarrow> x = 0"
by (metis (no_types, opaque_lifting) add_0 bits_div_by_1
comm_monoid_mult_class.mult_1 linorder_not_le lt1_neq0
sqrt_induct sqrt_le sub_wrap word_not_simps(1))
definition "mul_bound x y \<equiv> y = x * y div x"
lemma safe_mul_commute: "safe_mul (x :: u64) y = safe_mul y x"
apply (clarsimp simp: safe_mul_def)
apply (safe)
apply (unat_arith, simp)
apply (metis (no_types, lifting) bot_nat_0.not_eq_extremum div_mult_le mult.commute
nonzero_mult_div_cancel_left order_le_less_trans unat_mult_lem unsigned_less)
apply (unat_arith, simp)
apply (metis (no_types, lifting) bot_nat_0.not_eq_extremum div_mult_le mult.commute
nonzero_mult_div_cancel_left order_le_less_trans unat_mult_lem unsigned_less)
done
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?)
using ebi_not_zero apply force
apply (metis brf_ebi_times_bounded mult.commute safe_mul_def)
using safe_mul_commute by blast
lemma nonempty_ball_conj_lift: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. P \<and> Q x) = (P \<and> (\<forall>x\<in>S. Q x))"
by (safe; clarsimp?)