-
Notifications
You must be signed in to change notification settings - Fork 0
/
Ipc_AI.thy
3382 lines (2634 loc) · 126 KB
/
Ipc_AI.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
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
theory Ipc_AI
imports Finalise_AI
begin
declare if_cong[cong del]
lemmas lookup_slot_wrapper_defs[simp] =
lookup_source_slot_def lookup_target_slot_def lookup_pivot_slot_def
lemma get_mi_inv[wp]: "\<lbrace>I\<rbrace> get_message_info a \<lbrace>\<lambda>x. I\<rbrace>"
by (simp add: get_message_info_def user_getreg_inv | wp)+
lemma set_mi_tcb [wp]:
"\<lbrace> tcb_at t \<rbrace> set_message_info receiver msg \<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
by (simp add: set_message_info_def) wp
lemma mask_mask:
"mask_cap R (mask_cap R' c) = mask_cap (R \<inter> R') c"
by (auto simp: mask_cap_def cap_rights_update_def acap_rights_update_def
validate_vm_rights_inter Int_assoc Int_commute[of R']
split: cap.splits arch_cap.splits)
lemma lsfco_real_cte_at:
"\<lbrace>valid_objs and valid_cap cn\<rbrace>
lookup_slot_for_cnode_op f cn idx depth
\<lbrace>\<lambda>rv. real_cte_at rv\<rbrace>,-"
apply (simp add: lookup_slot_for_cnode_op_def split_def)
apply (rule conjI)
prefer 2
apply clarsimp
apply (rule hoare_pre)
apply wp
apply (clarsimp simp: unlessE_def whenE_def split del: split_if)
apply (rule hoare_pre)
apply (wp resolve_address_bits_real_cte_at | wpcw)+
apply simp
done
lemma lsfco_cte_at:
"\<lbrace>valid_objs and valid_cap cn\<rbrace>
lookup_slot_for_cnode_op f cn idx depth
\<lbrace>\<lambda>rv. cte_at rv\<rbrace>,-"
by (rule hoare_post_imp_R, rule lsfco_real_cte_at, simp add: real_cte_at_cte)
declare do_machine_op_tcb[wp]
lemma load_ct_inv[wp]:
"\<lbrace>P\<rbrace> load_cap_transfer buf \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: load_cap_transfer_def)
apply (wp dmo_inv mapM_wp' loadWord_inv)
done
lemma get_recv_slot_inv[wp]:
"\<lbrace> P \<rbrace> get_receive_slots receiver buf \<lbrace>\<lambda>rv. P \<rbrace>"
apply (case_tac buf)
apply simp
apply (simp add: split_def whenE_def)
apply (wp | simp)+
done
lemma cte_wp_at_eq_simp:
"cte_wp_at (op = cap) = cte_wp_at (\<lambda>c. c = cap)"
apply (rule arg_cong [where f=cte_wp_at])
apply (safe intro!: ext)
done
lemma get_rs_cte_at[wp]:
"\<lbrace>\<top>\<rbrace>
get_receive_slots receiver recv_buf
\<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. cte_wp_at (\<lambda>c. c = cap.NullCap) x s\<rbrace>"
apply (cases recv_buf)
apply (simp,wp,simp)
apply (clarsimp simp add: split_def whenE_def)
apply (wp | simp add: cte_wp_at_eq_simp | rule get_cap_wp)+
done
lemma get_rs_cte_at2[wp]:
"\<lbrace>\<top>\<rbrace>
get_receive_slots receiver recv_buf
\<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. cte_wp_at (op = cap.NullCap) x s\<rbrace>"
apply (rule hoare_strengthen_post, rule get_rs_cte_at)
apply (clarsimp simp: cte_wp_at_caps_of_state)
done
lemma get_rs_real_cte_at[wp]:
"\<lbrace>valid_objs\<rbrace>
get_receive_slots receiver recv_buf
\<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. real_cte_at x s\<rbrace>"
apply (cases recv_buf)
apply (simp,wp,simp)
apply (clarsimp simp add: split_def whenE_def)
apply (wp hoare_drop_imps lsfco_real_cte_at lookup_cap_valid | simp | rule get_cap_wp)+
done
declare returnOKE_R_wp [wp]
lemma cap_derive_not_null_helper:
"\<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>Q\<rbrace>,- \<Longrightarrow>
\<lbrace>\<lambda>s. cap \<noteq> cap.NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> cap.IRQControlCap \<longrightarrow> P s\<rbrace>
derive_cap slot
cap
\<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> Q rv s\<rbrace>,-"
apply (case_tac cap,
simp_all add: is_zombie_def,
safe elim!: hoare_post_imp_R)
apply (wp | simp add: derive_cap_def is_zombie_def)+
done
lemma mask_cap_Null [simp]:
"(mask_cap R c = cap.NullCap) = (c = cap.NullCap)"
by (cases c) (auto simp: mask_cap_def cap_rights_update_def)
lemma update_cap_data_closedform:
"update_cap_data pres w cap =
(case cap of
cap.EndpointCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (cap.EndpointCap r (w && mask 28) rights) else cap.NullCap
| cap.AsyncEndpointCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (cap.AsyncEndpointCap r (w && mask 28) rights) else cap.NullCap
| cap.CNodeCap r bits guard \<Rightarrow>
if word_bits < unat ((w >> 3) && mask 5) + bits
then cap.NullCap
else cap.CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> 3) && mask 5)) (to_bl g'')) ((w >> 8) && mask 18))
| cap.ThreadCap r \<Rightarrow> cap.ThreadCap r
| cap.DomainCap \<Rightarrow> cap.DomainCap
| cap.UntypedCap p n idx \<Rightarrow> cap.UntypedCap p n idx
| cap.NullCap \<Rightarrow> cap.NullCap
| cap.ReplyCap t m \<Rightarrow> cap.ReplyCap t m
| cap.IRQControlCap \<Rightarrow> cap.IRQControlCap
| cap.IRQHandlerCap irq \<Rightarrow> cap.IRQHandlerCap irq
| cap.Zombie r b n \<Rightarrow> cap.Zombie r b n
| cap.ArchObjectCap cap \<Rightarrow> cap.ArchObjectCap (arch_update_cap_data w cap))"
apply (cases cap,
simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
is_aep_cap.simps is_cnode_cap.simps is_arch_cap_def word_size
cap_ep_badge.simps badge_update_def o_def cap_rights_update_def
simp_thms cap_rights.simps Let_def split_def
the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def
cong: if_cong)
apply auto
done
lemma update_cap_Null:
"update_cap_data p D c \<noteq> cap.NullCap \<Longrightarrow> c \<noteq> cap.NullCap"
by (auto simp: update_cap_data_closedform is_cap_defs)
lemma ensure_no_children_wp:
"\<lbrace>\<lambda>s. descendants_of p (cdt s) = {} \<longrightarrow> P s\<rbrace> ensure_no_children p \<lbrace>\<lambda>_. P\<rbrace>, -"
apply (simp add: ensure_no_children_descendants valid_def validE_R_def validE_def)
apply (auto simp: in_monad)
done
lemma cap_asid_PageCap_None [simp]:
"cap_asid (cap.ArchObjectCap (arch_cap.PageCap r R pgsz None)) = None"
by (simp add: cap_asid_def)
lemma arch_derive_cap_is_derived:
"\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap . cap_master_cap cap =
cap_master_cap (cap.ArchObjectCap c') \<and>
cap_aligned cap \<and>
cap_asid cap = cap_asid (cap.ArchObjectCap c') \<and>
vs_cap_ref cap = vs_cap_ref (cap.ArchObjectCap c')) p s\<rbrace>
arch_derive_cap c'
\<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p (cap.ArchObjectCap rv)) p s\<rbrace>, -"
unfolding arch_derive_cap_def
apply(cases c', simp_all add: is_cap_simps cap_master_cap_def)
apply((wp throwError_validE_R
| clarsimp simp: is_derived_def is_cap_simps cap_master_cap_def
cap_aligned_def is_aligned_no_overflow is_pt_cap_def
cap_asid_def vs_cap_ref_def
| erule cte_wp_at_weakenE
| rule conjI
| simp split: arch_cap.split_asm cap.split_asm option.splits)+)
done
lemma derive_cap_is_derived:
"\<lbrace>\<lambda>s. c'\<noteq> cap.NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap c'
\<and> (cap_badge cap, cap_badge c') \<in> capBadge_ordering False
\<and> cap_asid cap = cap_asid c'
\<and> vs_cap_ref cap = vs_cap_ref c') slot s
\<and> valid_objs s\<rbrace>
derive_cap slot c'
\<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow>
cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -"
unfolding derive_cap_def
apply (cases c', simp_all add: is_cap_simps)
apply ((wp ensure_no_children_wp
| clarsimp simp: is_derived_def is_cap_simps
cap_master_cap_def bits_of_def
same_object_as_def is_pt_cap_def
cap_asid_def
| fold validE_R_def
| erule cte_wp_at_weakenE
| simp split: cap.split_asm)+)[11]
apply(wp, simp add: o_def)
apply(rule hoare_pre, wp hoare_drop_imps arch_derive_cap_is_derived)
apply(clarify, drule cte_wp_at_eqD, clarify)
apply(frule(1) cte_wp_at_valid_objs_valid_cap)
apply(erule cte_wp_at_weakenE)
apply(clarsimp simp: valid_cap_def)
done
lemma arch_derive_cap_cte:
"\<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap \<and> is_derived (cdt s) p (cap.ArchObjectCap c') c) p s\<rbrace>
arch_derive_cap c'
\<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap \<and> is_derived (cdt s) p (cap.ArchObjectCap rv) c) p s\<rbrace>, -"
unfolding arch_derive_cap_def
apply(cases c', simp_all add: is_cap_simps)
apply(rule hoare_pre, wp ensure_no_children_wp, clarsimp)+
apply(erule cte_wp_at_weakenE)
apply(case_tac c, (clarsimp simp: is_derived_def cap_master_cap_def is_cap_simps
cap_asid_def is_pt_cap_def vs_cap_ref_def
split: cap.splits arch_cap.splits)+)
apply(rule hoare_pre, wpc, wp, clarsimp)+
done
lemma derive_cap_cte:
"\<lbrace>\<lambda>s. c' \<noteq> cap.NullCap \<and> \<not>is_zombie c' \<and> c' \<noteq> cap.IRQControlCap \<longrightarrow>
(is_untyped_cap c' \<longrightarrow> descendants_of p (cdt s) = {}) \<longrightarrow>
cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap \<and> is_derived (cdt s) p c' c) p s\<rbrace>
derive_cap p c'
\<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow>
cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap \<and> is_derived (cdt s) p rv c) p s\<rbrace>, -"
unfolding derive_cap_def
apply (cases c', simp_all add: is_cap_simps)
apply ((rule hoare_pre, wp ensure_no_children_wp, simp)+)[11]
apply clarsimp
apply (rule hoare_pre, wp)
apply (simp add: o_def)
apply (wp arch_derive_cap_cte)
apply assumption
done
lemma is_derived_cap_rights [simp]:
"is_derived m p (cap_rights_update R c) = is_derived m p c"
apply (rule ext)
apply (simp add: cap_rights_update_def is_derived_def is_cap_simps)
apply (case_tac x, simp_all)
apply (simp add: cap_master_cap_def bits_of_def is_cap_simps
vs_cap_ref_def
split: cap.split)+
apply (simp add: is_cap_simps is_page_cap_def
cong: arch_cap.case_cong)
apply (simp split: arch_cap.split cap.split
add: is_cap_simps acap_rights_update_def is_pt_cap_def)
done
lemma is_derived_mask [simp]:
"is_derived m p (mask_cap R c) = is_derived m p c"
by (simp add: mask_cap_def)
lemma is_derived_cap_data:
"\<lbrakk> update_cap_data pres D c \<noteq> cap.NullCap; is_derived (cdt s) p c c' \<rbrakk> \<Longrightarrow>
is_derived (cdt s) p (update_cap_data pres D c) c'"
apply (case_tac c)
apply (simp_all add: is_derived_def cap_master_cap_simps split del: split_if
split: split_if_asm)
apply (clarsimp dest!:cap_master_cap_eqDs
simp:update_cap_data_closedform cap_master_cap_simps
is_cap_simps vs_cap_ref_def arch_update_cap_data_def
split:if_splits)+
apply (case_tac c')
apply (clarsimp dest!:cap_master_cap_eqDs
simp:cap_master_cap_simps cap_asid_def split:arch_cap.splits option.splits)+
done
lemma is_derived_remove_rights [simp]:
"is_derived m p (remove_rights R c) = is_derived m p c"
by (simp add: remove_rights_def)
definition
"valid_message_info mi \<equiv>
mi_length mi \<le> of_nat msg_max_length \<and>
mi_extra_caps mi \<le> of_nat msg_max_extra_caps"
lemma data_to_message_info_valid:
"valid_message_info (data_to_message_info w)"
apply (simp add: valid_message_info_def data_to_message_info_def)
apply (rule conjI)
apply (simp add: word_and_le1 msg_max_length_def msg_max_extra_caps_def Let_def not_less)+
done
lemma get_mi_valid[wp]:
"\<lbrace>valid_mdb\<rbrace> get_message_info a \<lbrace>\<lambda>rv s. valid_message_info rv\<rbrace>"
apply (simp add: get_message_info_def)
apply (wp | simp add: data_to_message_info_valid)+
done
crunch inv[wp]: get_extra_cptr P (wp: dmo_inv loadWord_inv)
lemma get_extra_cptrs_inv[wp]:
"\<lbrace>P\<rbrace> get_extra_cptrs buf mi \<lbrace>\<lambda>rv. P\<rbrace>"
apply (cases buf, simp_all del: upt.simps)
apply (wp mapM_wp' dmo_inv loadWord_inv
| simp add: load_word_offs_def del: upt.simps)+
done
lemma mapM_length[wp]:
"\<lbrace>\<lambda>s. P (length xs)\<rbrace> mapM f xs \<lbrace>\<lambda>rv s. P (length rv)\<rbrace>"
apply (induct xs arbitrary: P)
apply (simp add: mapM_def sequence_def)
apply wp
apply simp
apply (simp add: mapM_Cons)
apply wp
apply simp
apply assumption
apply wp
done
lemma get_extra_cptrs_length[wp]:
"\<lbrace>\<lambda>s . valid_message_info mi\<rbrace>
get_extra_cptrs buf mi
\<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace>"
apply (cases buf)
apply (simp, wp, simp)
apply (simp add: msg_max_length_def)
apply (subst hoare_liftM_subst, simp add: o_def)
apply (rule hoare_pre)
apply (rule mapM_length, simp)
apply (clarsimp simp: valid_message_info_def msg_max_extra_caps_def
word_le_nat_alt
intro: length_upt)
done
lemma cap_insert_ep_at[wp]:
"\<lbrace>ep_at ep\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. ep_at ep\<rbrace>"
by (simp add: ep_at_typ, wp)
lemma cap_master_cap_remove_rights[simp]:
"cap_master_cap (cap_rights_update rights cap) = cap_master_cap cap"
apply (simp add: cap_rights_update_def
acap_rights_update_def
split: cap.split arch_cap.split)
apply (simp add: cap_master_cap_def)
done
lemma cap_badge_rights_update[simp]:
"cap_badge (cap_rights_update rights cap) = cap_badge cap"
by (simp add: cap_rights_update_def split: cap.split)
lemma cap_asid_rights_update [simp]:
"cap_asid (cap_rights_update R c) = cap_asid c"
apply (simp add: cap_rights_update_def acap_rights_update_def split: cap.splits arch_cap.splits)
apply (clarsimp simp: cap_asid_def)
done
lemma get_cap_cte_wp_at_rv:
"\<lbrace>cte_wp_at (\<lambda>cap. P cap cap) p\<rbrace> get_cap p \<lbrace>\<lambda>rv. cte_wp_at (P rv) p\<rbrace>"
apply (wp get_cap_wp)
apply (clarsimp simp: cte_wp_at_caps_of_state)
done
lemma lsfco_cte_wp_at_univ:
"\<lbrace>valid_objs and valid_cap root and K (\<forall>cap rv. P cap rv)\<rbrace>
lookup_slot_for_cnode_op f root idx depth
\<lbrace>\<lambda>rv. cte_wp_at (P rv) rv\<rbrace>, -"
apply (rule hoare_gen_asmE)
apply (rule hoare_post_imp_R)
apply (rule lsfco_cte_at)
apply (clarsimp simp: cte_wp_at_def)
done
lemma bits_low_high_eq:
assumes low: "x && mask bits = y && mask bits"
and high: "x >> bits = y >> bits"
shows "x = y"
apply (rule word_eqI)
apply (case_tac "n < bits")
apply (cut_tac x=n in word_eqD[OF low])
apply (simp add: word_size)
apply (cut_tac x="n - bits" in word_eqD[OF high])
apply (simp add: nth_shiftr)
done
lemma cap_rights_update_vs_cap_ref[simp]:
"vs_cap_ref (cap_rights_update rs cap) = vs_cap_ref cap"
by (simp add: vs_cap_ref_def cap_rights_update_def
acap_rights_update_def
split: cap.split arch_cap.split)
lemma mask_cap_vs_cap_ref[simp]:
"vs_cap_ref (mask_cap msk cap) = vs_cap_ref cap"
by (simp add: mask_cap_def)
lemma set_extra_badge_typ_at[wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>"
by (simp add: set_extra_badge_def store_word_offs_def | wp)+
lemmas set_extra_badge_typ_ats[wp] = abs_typ_at_lifts[OF set_extra_badge_typ_at]
crunch valid_objs [wp]: set_extra_badge valid_objs
crunch aligned [wp]: set_extra_badge pspace_aligned
crunch dist [wp]: set_extra_badge pspace_distinct
crunch valid_mdb [wp]: set_extra_badge valid_mdb
crunch cte_wp_at [wp]: set_extra_badge "cte_wp_at P p"
crunch inv[wp]: get_extra_cptr P (wp: dmo_inv loadWord_inv)
lemma impEM:
"\<lbrakk>P \<longrightarrow> Q; P; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by auto
lemma derive_cap_is_derived_foo:
"\<lbrace>\<lambda>s. \<forall>cap'. (cte_wp_at (\<lambda>capa.
cap_master_cap capa = cap_master_cap cap \<and>
(cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and>
cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap)
slot s \<and> valid_objs s \<and> cap' \<noteq> cap.NullCap
\<longrightarrow> cte_at slot s )
\<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap')
\<and> (cap' \<noteq> cap.NullCap \<longrightarrow> cap \<noteq> cap.NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> cap.IRQControlCap)
\<longrightarrow> Q cap' s \<rbrace>
derive_cap slot cap \<lbrace>Q\<rbrace>,-"
apply (clarsimp simp add: validE_R_def validE_def valid_def
split: sum.splits)
apply (frule in_inv_by_hoareD[OF derive_cap_inv], clarsimp)
apply (erule allE)
apply (erule impEM)
apply (frule use_validE_R[OF _ cap_derive_not_null_helper, OF _ _ imp_refl])
apply (wp derive_cap_inv)
apply (intro conjI)
apply (clarsimp simp:cte_wp_at_caps_of_state)+
apply (erule(1) use_validE_R[OF _ derive_cap_valid_cap])
apply simp
apply simp
done
lemma cap_rights_update_NullCap[simp]:
"(cap_rights_update rs cap = cap.NullCap) = (cap = cap.NullCap)"
by (simp add: cap_rights_update_def split: cap.split)
crunch in_user_frame[wp]: set_extra_badge "in_user_frame buffer"
lemma cap_insert_cte_wp_at:
"\<lbrace>\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s \<and> valid_mdb s \<and> valid_objs s
\<and> (if p = dest then P cap else cte_wp_at (\<lambda>c. P (masked_as_full c cap)) p s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>"
apply (rule hoare_name_pre_state)
apply (clarsimp split:split_if_asm)
apply (clarsimp simp:cap_insert_def)
apply (wp set_cap_cte_wp_at | simp split del: split_if)+
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_splits)
apply (wp get_cap_wp)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (clarsimp simp:cap_insert_def)
apply (wp set_cap_cte_wp_at | simp split del: split_if)+
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_splits)
apply (wp set_cap_cte_wp_at get_cap_wp)
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (frule(1) caps_of_state_valid)
apply (intro conjI impI)
apply (clarsimp simp:masked_as_full_def split:if_splits)+
apply (clarsimp simp:valid_mdb_def is_derived_def)
apply (drule(4) untyped_incD)
apply (clarsimp simp:is_cap_simps cap_aligned_def
dest!:valid_cap_aligned split:split_if_asm)
apply (drule_tac y = "of_nat fa" in word_plus_mono_right[OF _ is_aligned_no_overflow',rotated])
apply (simp add:word_of_nat_less unat_power_lower32)
apply (clarsimp simp:p_assoc_help)
apply (drule(1) caps_of_state_valid)+
apply (clarsimp simp:valid_cap_def valid_untyped_def max_free_index_def)
apply (clarsimp simp:masked_as_full_def split:if_splits)
apply (erule impEM)
apply (clarsimp simp: is_derived_def split:if_splits)
apply (clarsimp simp:is_cap_simps vs_cap_ref_def cap_master_cap_simps)
apply (clarsimp simp:is_cap_simps cap_master_cap_simps dest!:cap_master_cap_eqDs)
apply (erule impEM)
apply (clarsimp simp: is_derived_def split:if_splits)
apply (clarsimp simp:is_cap_simps vs_cap_ref_def cap_master_cap_simps)
apply (clarsimp simp:is_cap_simps cap_master_cap_simps dest!:cap_master_cap_eqDs)
apply (clarsimp simp:is_derived_def is_cap_simps cap_master_cap_simps)
done
lemma set_cap_in_user_frame[wp]:
"\<lbrace>in_user_frame buffer\<rbrace> set_cap cap ref \<lbrace>\<lambda>_. in_user_frame buffer\<rbrace>"
by (simp add: in_user_frame_def) (wp hoare_vcg_ex_lift set_cap_typ_at)
lemma cap_insert_weak_cte_wp_at2:
assumes imp: "\<And>c. P c \<Longrightarrow> \<not>is_untyped_cap c"
shows
"\<lbrace>\<lambda>s. if p = dest then P cap else cte_wp_at P p s\<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>"
unfolding cap_insert_def
by (wp set_cap_cte_wp_at get_cap_wp static_imp_wp
| simp add: cap_insert_def
| unfold set_untyped_cap_as_full_def
| auto simp: cte_wp_at_def dest!:imp)+
crunch in_user_frame[wp]: cap_insert "in_user_frame buffer"
(wp: crunch_wps ignore: get_cap)
crunch cdt [wp]: set_extra_badge "\<lambda>s. P (cdt s)"
lemma descendants_insert_update:
"\<lbrakk>m dest = None; p \<in> descendants_of a m\<rbrakk>
\<Longrightarrow> p \<in> descendants_of a (\<lambda>x. if x = dest then y else m x)"
apply (clarsimp simp:descendants_of_empty descendants_of_def)
apply (simp add:cdt_parent_rel_def)
apply (erule trancl_mono)
apply (clarsimp simp:is_cdt_parent_def)
done
(* FIXME: name conflicts with WordLemmaBucket.in_emptyE. *)
lemma in_emptyE: "\<lbrakk>A={}; \<exists>x. x\<in> A\<rbrakk> \<Longrightarrow> P" by clarsimp
lemma caps_of_state_orth_original:
"caps_of_state(s\<lparr>is_original_cap := M \<rparr>) = caps_of_state s"
by (rule Invariants_AI.revokable_update.caps_of_state_update)
lemma is_derived_cap_rights2[simp]:
"is_derived m p c (cap_rights_update R c') = is_derived m p c c'"
apply (case_tac c')
apply (simp_all add:cap_rights_update_def)
apply (clarsimp simp:is_derived_def is_cap_simps cap_master_cap_def
vs_cap_ref_def split:cap.splits )+
apply (case_tac arch_cap)
apply (simp_all add:acap_rights_update_def)
done
lemma weak_derived_update_rights:
"valid_cap cap s \<Longrightarrow> weak_derived cap (cap_rights_update R cap)"
apply (case_tac cap)
apply (clarsimp simp:weak_derived_def same_object_as_def
is_cap_simps cap_rights_update_def acap_rights_update_def copy_of_def)+
apply (case_tac arch_cap)
apply (simp_all add: cap_asid_def cap_vptr_def)
apply (clarsimp simp:valid_cap_def cap_aligned_def)
apply (erule is_aligned_no_overflow)
done
lemma masked_as_full_null_cap[simp]:
"(masked_as_full x x = cap.NullCap) = (x = cap.NullCap)"
"(cap.NullCap = masked_as_full x x) = (x = cap.NullCap)"
by (case_tac x,simp_all add:masked_as_full_def)+
lemma transfer_caps_loop_mi_label[wp]:
"\<lbrace>\<lambda>s. P (mi_label mi)\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>mi' s. P (mi_label mi')\<rbrace>"
apply (induct caps arbitrary: n slots mi)
apply simp
apply wp
apply simp
apply (clarsimp split del: split_if)
apply (rule hoare_pre)
apply (wp const_on_failure_wp hoare_drop_imps | assumption)+
apply simp
done
lemma cap_insert_real_cte_at[wp]:
"\<lbrace>real_cte_at p\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. real_cte_at p\<rbrace>"
by (simp add: cap_table_at_typ, wp)
lemma valid_remove_rights_If[simp]:
"valid_cap cap s \<Longrightarrow> valid_cap (if P then remove_rights rs cap else cap) s"
by simp
declare const_on_failure_wp [wp]
crunch ex_cte_cap_wp_to [wp]: set_extra_badge "ex_cte_cap_wp_to P p"
(lift: ex_cte_cap_to_pres)
lemma return_value_any_R:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
by (erule hoare_post_imp_R, simp)
lemma cap_insert_assume_null:
"\<lbrace>P\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace> \<Longrightarrow>
\<lbrace>\<lambda>s. cte_wp_at (op = cap.NullCap) dest s \<longrightarrow> P s\<rbrace> cap_insert cap src dest \<lbrace>Q\<rbrace>"
apply (rule hoare_name_pre_state)
apply (erule impCE)
apply (simp add: cap_insert_def)
apply (rule hoare_seq_ext[OF _ get_cap_sp])+
apply (clarsimp simp: valid_def cte_wp_at_caps_of_state in_monad
split del: split_if)
apply (erule hoare_pre(1))
apply simp
done
lemma transfer_caps_loop_presM:
assumes x: "\<And>cap src dest.
\<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s
\<and> real_cte_at src s
\<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> cap.NullCap)
\<and> (em \<longrightarrow> cte_wp_at (op = cap.NullCap) dest s)
\<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace>
cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>"
assumes eb: "\<And>b n. \<lbrace>P\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. P\<rbrace>"
shows "\<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and>
(\<forall>x \<in> set slots. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s \<and> real_cte_at x s) \<and>
(\<forall>x \<in> set caps. valid_cap (fst x) s \<and>
cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s
\<and> real_cte_at (snd x) s))
\<and> (ex \<longrightarrow> (\<forall>x \<in> set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. P\<rbrace>"
apply (induct caps arbitrary: slots n mi)
apply (simp, wp, simp)
apply (clarsimp simp add: Let_def split_def whenE_def
cong: if_cong list.case_cong split del: split_if)
apply (rule hoare_pre)
apply (wp eb hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift static_imp_wp
| assumption | simp split del: split_if)+
apply (rule cap_insert_assume_null)
apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at static_imp_wp)
apply (rule hoare_vcg_conj_liftE_R)
apply (rule derive_cap_is_derived_foo)
apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> cap.NullCap \<longrightarrow>
cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s)
\<and> (cap'\<noteq> cap.NullCap \<longrightarrow> ?QM s cap')"
in hoare_post_imp_R)
prefer 2
apply clarsimp
apply assumption
apply (rule hoare_vcg_conj_liftE_R)
apply (rule hoare_vcg_const_imp_lift_R)
apply (rule derive_cap_is_derived)
apply (wp derive_cap_is_derived_foo)
apply (clarsimp simp: cte_wp_at_caps_of_state
ex_cte_cap_to_cnode_always_appropriate_strg
real_cte_tcb_valid caps_of_state_valid
split del: split_if)
apply (clarsimp simp: remove_rights_def caps_of_state_valid
neq_Nil_conv cte_wp_at_caps_of_state
imp_conjR[symmetric] conj_ac
split del: if_splits)
apply (intro conjI)
apply clarsimp
apply (case_tac "cap = a",clarsimp)
apply (clarsimp simp:masked_as_full_def is_cap_simps)
apply (clarsimp simp: cap_master_cap_simps split:if_splits)
apply (clarsimp split del:if_splits)
apply (intro conjI)
apply (clarsimp split:if_splits)
apply (clarsimp)
apply (rule ballI)
apply (drule(1) bspec)
apply clarsimp
apply (intro conjI)
apply (case_tac "capa = ac",clarsimp+)
apply (case_tac "capa = ac")
apply (clarsimp simp:masked_as_full_def is_cap_simps split:if_splits)+
done
abbreviation (input)
"transfer_caps_srcs caps s \<equiv>
(\<forall>x \<in> set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s
\<and> real_cte_at (snd x) s)"
lemmas transfer_caps_loop_pres =
transfer_caps_loop_presM[where vo=False and ex=False and em=False, simplified]
lemma transfer_caps_loop_typ_at[wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
by (wp transfer_caps_loop_pres)
lemma transfer_loop_aligned[wp]:
"\<lbrace>pspace_aligned\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. pspace_aligned\<rbrace>"
by (wp transfer_caps_loop_pres)
lemma transfer_loop_distinct[wp]:
"\<lbrace>pspace_distinct\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. pspace_distinct\<rbrace>"
by (wp transfer_caps_loop_pres)
lemma invs_valid_objs2:
"invs s \<longrightarrow> valid_objs s"
by clarsimp
lemma transfer_caps_loop_valid_objs[wp]:
"\<lbrace>valid_objs and valid_mdb and (\<lambda>s. \<forall>slot \<in> set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) slot s)
and transfer_caps_srcs caps and K (distinct slots)\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_objs\<rbrace>"
apply (rule hoare_pre)
apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False])
apply (wp|clarsimp)+
apply (drule(1) bspec)
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (drule(1) caps_of_state_valid)
apply (case_tac "a = cap.NullCap")
apply clarsimp+
done
lemma transfer_caps_loop_valid_mdb[wp]:
"\<lbrace>\<lambda>s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s
\<and> (\<forall>slot \<in> set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) slot s)
\<and> transfer_caps_srcs caps s \<and> distinct slots\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_mdb\<rbrace>"
apply (rule hoare_pre)
apply (rule transfer_caps_loop_presM[where vo=True and em=True and ex=False])
apply wp
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (wp set_extra_badge_valid_mdb)
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (drule(1) bspec)+
apply clarsimp
apply (drule(1) caps_of_state_valid)
apply (case_tac "a = cap.NullCap")
apply clarsimp+
done
crunch state_refs_of [wp]: set_extra_badge "\<lambda>s. P (state_refs_of s)"
lemma tcl_state_refs_of[wp]:
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>"
by (wp transfer_caps_loop_pres)
crunch if_live [wp]: set_extra_badge if_live_then_nonz_cap
lemma tcl_iflive[wp]:
"\<lbrace>if_live_then_nonz_cap\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>"
by (wp transfer_caps_loop_pres cap_insert_iflive)
crunch if_unsafe [wp]: set_extra_badge if_unsafe_then_cap
lemma tcl_ifunsafe[wp]:
"\<lbrace>\<lambda>s. if_unsafe_then_cap s \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>"
by (wp transfer_caps_loop_presM[where vo=False and em=False and ex=True, simplified]
cap_insert_ifunsafe | simp)+
lemma get_cap_global_refs[wp]:
"\<lbrace>valid_global_refs\<rbrace> get_cap p \<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace>"
apply (rule hoare_pre)
apply (rule get_cap_wp)
apply (clarsimp simp: valid_refs_def2 valid_global_refs_def cte_wp_at_caps_of_state)
apply (blast intro: ranI)
done
lemma cap_range_update [simp]:
"cap_range (cap_rights_update R cap) = cap_range cap"
by (simp add: cap_range_def cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
lemma derive_cap_idle[wp]:
"\<lbrace>\<lambda>s. global_refs s \<inter> cap_range cap = {}\<rbrace>
derive_cap slot cap
\<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace>, -"
apply (simp add: derive_cap_def)
apply (rule hoare_pre)
apply (wpc| wp | simp add: arch_derive_cap_def)+
apply (case_tac cap, simp_all add: cap_range_def)
apply (case_tac arch_cap, simp_all)
done
crunch st_tcb_at [wp]: set_extra_badge "\<lambda>s. st_tcb_at P p s"
crunch idle [wp]: set_extra_badge "\<lambda>s. P (idle_thread s)"
lemma tcl_idle[wp]:
"\<lbrace>valid_idle\<rbrace> transfer_caps_loop ep diminish buffer n caps slots mi \<lbrace>\<lambda>_. valid_idle\<rbrace>"
by (wp transfer_caps_loop_pres cap_insert_idle valid_idle_lift)
crunch cur_tcb [wp]: set_extra_badge cur_tcb
lemma tcl_ct[wp]:
"\<lbrace>cur_tcb\<rbrace> transfer_caps_loop ep diminish buffer n caps slots mi \<lbrace>\<lambda>rv. cur_tcb\<rbrace>"
by (wp transfer_caps_loop_pres)
crunch it[wp]: cap_insert "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps simp: crunch_simps)
lemma tcl_it[wp]:
"\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>"
by (wp transfer_caps_loop_pres)
lemma arch_derive_cap_objrefs_iszombie:
"\<lbrace>\<lambda>s . P (Option.set (aobj_ref cap)) False s\<rbrace>
arch_derive_cap cap
\<lbrace>\<lambda>rv s. P (Option.set (aobj_ref rv)) False s\<rbrace>,-"
apply(cases cap, simp_all add: is_zombie_def arch_derive_cap_def)
apply(rule hoare_pre, wpc?, wp, simp)+
done
lemma derive_cap_objrefs_iszombie:
"\<lbrace>\<lambda>s. \<not> is_zombie cap \<longrightarrow> P (obj_refs cap) False s\<rbrace>
derive_cap slot cap
\<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> P (obj_refs rv) (is_zombie rv) s\<rbrace>,-"
apply (cases cap, simp_all add: derive_cap_def is_zombie_def)
apply (rule hoare_pre,
(wp | simp add: o_def arch_derive_cap_objrefs_iszombie)+)+
done
lemma obj_refs_remove_rights[simp]:
"obj_refs (remove_rights rs cap) = obj_refs cap"
by (simp add: remove_rights_def cap_rights_update_def
acap_rights_update_def
split: cap.splits arch_cap.splits)
lemma is_zombie_rights[simp]:
"is_zombie (remove_rights rs cap) = is_zombie cap"
by (simp add: is_zombie_def remove_rights_def cap_rights_update_def
split: cap.splits)
crunch caps_of_state [wp]: set_extra_badge "\<lambda>s. P (caps_of_state s)"
lemma set_extra_badge_zombies_final[wp]:
"\<lbrace>zombies_final\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. zombies_final\<rbrace>"
apply (simp add: zombies_final_def cte_wp_at_caps_of_state is_final_cap'_def2)
apply (wp hoare_vcg_all_lift final_cap_lift)
done
lemma tcl_zombies[wp]:
"\<lbrace>zombies_final and valid_objs and valid_mdb and K (distinct slots)
and (\<lambda>s. \<forall>slot \<in> set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) slot s )
and transfer_caps_srcs caps\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. zombies_final\<rbrace>"
apply (rule hoare_pre)
apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False])
apply (wp cap_insert_zombies)
apply clarsimp
apply (case_tac "(a, b) = (ab, bb)")
apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def)
apply (simp split: split_if_asm)
apply (clarsimp simp: is_cap_simps cap_master_cap_def
split: cap.split_asm)+
apply fastforce
apply (frule(3) zombies_finalD3)
apply (clarsimp simp: is_derived_def is_cap_simps cap_master_cap_simps
vs_cap_ref_def split: split_if_asm dest!:cap_master_cap_eqDs)
apply (drule_tac a=r in equals0D)
apply (drule master_cap_obj_refs, simp)
apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def
is_cap_simps cap_master_cap_def
split: split_if_asm cap.split_asm)
apply fastforce
apply wp
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (drule(1) bspec,clarsimp)
apply (fastforce dest!:caps_of_state_valid)
done
lemma derive_cap_valid_globals [wp]:
"\<lbrace>valid_global_refs\<rbrace> derive_cap r cap \<lbrace>\<lambda>rv. valid_global_refs\<rbrace>"
by (rule valid_global_refs_cte_lift) wp
crunch arch [wp]: set_extra_badge "\<lambda>s. P (arch_state s)"
crunch irq [wp]: set_extra_badge "\<lambda>s. P (interrupt_irq_node s)"
lemma transfer_caps_loop_valid_globals [wp]:
"\<lbrace>valid_global_refs and valid_objs and valid_mdb and K (distinct slots)
and (\<lambda>s. \<forall>slot \<in> set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) slot s)
and transfer_caps_srcs caps\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_global_refs\<rbrace>"
apply (rule hoare_pre)
apply (rule transfer_caps_loop_presM[where em=False and ex=False and vo=True])
apply (wp | simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_cap_range)
apply (wp valid_global_refs_cte_lift|simp|intro conjI ballI)+
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (drule(1) bspec,clarsimp)
apply (frule(1) caps_of_state_valid)
apply (fastforce simp:valid_cap_def)
apply clarsimp
apply (drule(1) bspec)
apply (clarsimp simp:cte_wp_at_caps_of_state)
done
lemma transfer_caps_loop_arch[wp]:
"\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> transfer_caps_loop ep diminish buffer n caps slots mi \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>"
by (rule transfer_caps_loop_pres) wp
lemma transfer_caps_loop_valid_arch[wp]:
"\<lbrace>valid_arch_state\<rbrace> transfer_caps_loop ep diminish buffer n caps slots mi \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
by (rule valid_arch_state_lift) wp
lemma derive_cap_not_reply:
"\<lbrace>\<top>\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. \<not> is_reply_cap rv\<rbrace>, -"
apply (rule hoare_pre)
apply (wpc | wp
| clarsimp simp: derive_cap_def arch_derive_cap_def is_reply_cap_def)+
done
lemma tcl_reply':
"\<lbrace>valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K(distinct slots)
and (\<lambda>s. \<forall>x \<in> set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s)
and transfer_caps_srcs caps\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_reply_caps and valid_reply_masters\<rbrace>"
apply (rule hoare_pre)
apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False])
apply wp
apply (clarsimp simp: real_cte_at_cte)
apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def)
apply (clarsimp simp: real_cte_at_cte)
apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def is_cap_simps)
apply (frule(1) valid_reply_mastersD[OF caps_of_state_cteD])
apply (frule(1) tcb_cap_valid_caps_of_stateD)
apply (frule(1) caps_of_state_valid)
apply (clarsimp simp: tcb_cap_valid_def valid_cap_def is_cap_simps)
apply (clarsimp simp: obj_at_def is_tcb is_cap_table cap_master_cap_def)
apply (wp valid_reply_caps_st_cte_lift valid_reply_masters_cte_lift|simp)+