-
Notifications
You must be signed in to change notification settings - Fork 108
/
CSpaceInv_AI.thy
2101 lines (1749 loc) · 80.5 KB
/
CSpaceInv_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
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(*
CSpace invariants
*)
theory CSpaceInv_AI
imports ArchCSpaceInvPre_AI
begin
arch_requalify_consts
cap_master_arch_cap
replaceable_final_arch_cap
replaceable_non_final_arch_cap
unique_table_refs
arch_requalify_facts
aobj_ref_acap_rights_update
arch_obj_size_acap_rights_update
valid_arch_cap_acap_rights_update
cap_master_arch_inv
unique_table_refs_def
valid_ipc_buffer_cap_def
acap_rights_update_idem
valid_acap_rights_update_id
cap_master_arch_cap_rights
is_nondevice_page_cap_simps
set_cap_hyp_refs_of
state_hyp_refs_of_revokable
set_cap_hyp_refs_of
is_valid_vtable_root_is_arch_cap
lemma is_valid_vtable_root_simps[simp]:
"\<not> is_valid_vtable_root (UntypedCap a b c d)"
"\<not> is_valid_vtable_root (ThreadCap tcb_ref)"
"\<not> is_valid_vtable_root (CNodeCap cnode_ref sz guard)"
"\<not> is_valid_vtable_root (EndpointCap ep_ref badge R)"
"\<not> is_valid_vtable_root (NotificationCap ep_ref badge R)"
"\<not> is_valid_vtable_root (ReplyCap tcb_ref master R)"
"\<not> is_valid_vtable_root (Zombie e f g)"
"\<not> is_valid_vtable_root (NullCap)"
"\<not> is_valid_vtable_root (DomainCap)"
by (fastforce dest: is_valid_vtable_root_is_arch_cap simp: is_cap_simps)+
lemmas [simp] = aobj_ref_acap_rights_update arch_obj_size_acap_rights_update
valid_validate_vm_rights cap_master_arch_inv acap_rights_update_idem
cap_master_arch_cap_rights valid_acap_rights_update_id state_hyp_refs_of_revokable
lemmas [intro] = valid_arch_cap_acap_rights_update
lemmas [intro!] = valid_acap_rights_update_id
lemmas [wp] = set_cap_hyp_refs_of
lemma remove_rights_cap_valid[simp]:
"s \<turnstile> c \<Longrightarrow> s \<turnstile> remove_rights S c"
using valid_validate_vm_rights
apply (cases c; simp add: remove_rights_def cap_rights_update_def
valid_cap_def cap_aligned_def
split: bool.splits)
by fastforce
lemma get_thread_state_inv [simp]:
"\<lbrace> P \<rbrace> get_thread_state t \<lbrace> \<lambda>r. P \<rbrace>"
apply (simp add: get_thread_state_def thread_get_def gets_the_def)
apply wp
apply simp
done
lemma get_bound_notification_inv[simp]:
"\<lbrace>P\<rbrace> get_bound_notification t \<lbrace>\<lambda>r. P\<rbrace>"
apply (simp add: get_bound_notification_def thread_get_def gets_the_def)
apply (wp, simp)
done
lemma gets_the_sp:
"\<lbrace> Q \<rbrace> gets_the f \<lbrace>\<lambda>rv s. f s = Some rv \<and> Q s\<rbrace>"
by wpsimp
lemma gets_the_get_tcb_sp:
"\<lbrace> Q \<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. Q and ko_at (TCB t) thread\<rbrace>"
by wpsimp
lemma assert_get_tcb_sp:
assumes "\<And>s. Q s \<Longrightarrow> valid_objs s"
shows "\<lbrace> Q \<rbrace> gets_the (get_tcb thread)
\<lbrace>\<lambda>t. Q and ko_at (TCB t) thread and valid_tcb thread t \<rbrace>"
apply (rule hoare_strengthen_post[OF gets_the_get_tcb_sp])
apply (clarsimp simp: obj_at_def)
apply (erule (1) valid_objsE[where x=thread, OF assms])
apply (clarsimp simp: valid_obj_def)
done
crunch get_cap
for inv[wp]: "P"
(simp: crunch_simps)
lemma rab_inv[wp]:
"\<lbrace>P\<rbrace> resolve_address_bits slot \<lbrace>\<lambda>rv. P\<rbrace>"
unfolding resolve_address_bits_def
proof (induct slot rule: resolve_address_bits'.induct)
case (1 z cap cref)
show ?case
apply (clarsimp simp add: valid_def)
apply (subst (asm) resolve_address_bits'.simps)
apply (cases cap)
apply (auto simp: in_monad)[5]
defer
apply (auto simp: in_monad)[6]
apply (rename_tac obj_ref nat list)
apply (simp only: cap.simps)
apply (case_tac "nat + length list = 0")
apply (simp add: fail_def)
apply (simp only: if_False)
apply (case_tac a)
apply (simp only: K_bind_def)
apply (drule in_bindE_L, elim disjE conjE exE)+
apply (simp only: split: if_split_asm)
apply (simp add: returnOk_def return_def)
apply (drule in_bindE_L, elim disjE conjE exE)+
apply (simp only: split: if_split_asm)
prefer 2
apply (clarsimp simp: in_monad)
apply (drule (8) 1)
apply (clarsimp simp: in_monad)
apply (drule in_inv_by_hoareD [OF get_cap_inv])
apply (auto simp: in_monad valid_def)[1]
apply (clarsimp simp: in_monad)
apply (clarsimp simp: in_monad)
apply (clarsimp simp: in_monad)
apply (clarsimp simp: in_monad)
apply (clarsimp simp: in_monad)
apply (simp only: K_bind_def in_bindE_R)
apply (elim conjE exE)
apply (simp only: split: if_split_asm)
apply (simp add: in_monad split: if_split_asm)
apply (simp only: K_bind_def in_bindE_R)
apply (elim conjE exE)
apply (simp only: split: if_split_asm)
prefer 2
apply (clarsimp simp: in_monad)
apply (drule in_inv_by_hoareD [OF get_cap_inv])
apply simp
apply (drule (8) "1")
apply (clarsimp simp: in_monad valid_def)
apply (drule in_inv_by_hoareD [OF get_cap_inv])
apply (auto simp: in_monad)
done
qed
crunch lookup_slot_for_thread
for inv[wp]: P
crunch lookup_cap
for inv[wp]: P
lemma cte_at_tcb_update:
"tcb_at t s \<Longrightarrow> cte_at slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = cte_at slot s"
by (clarsimp simp add: cte_at_cases obj_at_def is_tcb)
lemma valid_cap_tcb_update [simp]:
"tcb_at t s \<Longrightarrow> (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) \<turnstile> cap = s \<turnstile> cap"
apply (clarsimp simp: is_tcb elim!: obj_atE)
apply (subgoal_tac "a_type (TCB tcba) = a_type (TCB tcb)")
apply (rule iffI)
apply (drule(1) valid_cap_same_type[where p=t])
apply simp
apply (simp add: fun_upd_idem)
apply (erule(2) valid_cap_same_type[OF _ sym])
apply (simp add: a_type_def)
done
lemma obj_at_tcb_update:
"\<lbrakk> tcb_at t s; \<And>x y. P (TCB x) = P (TCB y)\<rbrakk> \<Longrightarrow>
obj_at P t' (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = obj_at P t' s"
apply (simp add: obj_at_def is_tcb_def)
apply clarsimp
apply (case_tac ko)
apply simp_all
done
lemma valid_thread_state_tcb_update:
"\<lbrakk> tcb_at t s \<rbrakk> \<Longrightarrow>
valid_tcb_state ts (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = valid_tcb_state ts s"
apply (unfold valid_tcb_state_def)
apply (case_tac ts)
apply (simp_all add: obj_at_tcb_update is_ep_def is_tcb_def is_ntfn_def)
done
lemma valid_objs_tcb_update:
"\<lbrakk>tcb_at t s; valid_tcb t tcb s; valid_objs s \<rbrakk>
\<Longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)"
apply (clarsimp simp: valid_objs_def dom_def
elim!: obj_atE)
apply (intro conjI impI)
apply (rule valid_obj_same_type)
apply (simp add: valid_obj_def)+
apply (clarsimp simp: a_type_def is_tcb)
apply clarsimp
apply (rule valid_obj_same_type)
apply (drule_tac x=ptr in spec, simp)
apply (simp add: valid_obj_def)
apply assumption
apply (clarsimp simp add: a_type_def is_tcb)
done
lemma obj_at_update:
"obj_at P t' (s \<lparr>kheap := (kheap s)(t \<mapsto> v)\<rparr>) =
(if t = t' then P v else obj_at P t' s)"
by (simp add: obj_at_def)
lemma iflive_tcb_update:
"\<lbrakk> if_live_then_nonz_cap s; live (TCB tcb) \<longrightarrow> ex_nonz_cap_to t s;
obj_at (same_caps (TCB tcb)) t s \<rbrakk>
\<Longrightarrow> if_live_then_nonz_cap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)"
unfolding fun_upd_def
apply (simp add: if_live_then_nonz_cap_def, erule allEI)
apply safe
apply (clarsimp simp add: obj_at_def elim!: ex_cap_to_after_update
split: if_split_asm | (erule notE, erule ex_cap_to_after_update))+
done
lemma ifunsafe_tcb_update:
"\<lbrakk> if_unsafe_then_cap s; obj_at (same_caps (TCB tcb)) t s \<rbrakk>
\<Longrightarrow> if_unsafe_then_cap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)"
apply (simp add: if_unsafe_then_cap_def, elim allEI)
apply (clarsimp dest!: caps_of_state_cteD
simp: cte_wp_at_after_update fun_upd_def)
apply (clarsimp simp: cte_wp_at_caps_of_state
ex_cte_cap_to_after_update)
done
lemma zombies_tcb_update:
"\<lbrakk> zombies_final s; obj_at (same_caps (TCB tcb)) t s \<rbrakk>
\<Longrightarrow> zombies_final (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)"
apply (simp add: zombies_final_def is_final_cap'_def2, elim allEI)
apply (clarsimp simp: cte_wp_at_after_update fun_upd_def)
done
lemma valid_idle_tcb_update:
"\<lbrakk>valid_idle s; ko_at (TCB t) p s;
tcb_state t = tcb_state t'; tcb_bound_notification t = tcb_bound_notification t';
tcb_iarch t = tcb_iarch t';
valid_tcb p t' s \<rbrakk>
\<Longrightarrow> valid_idle (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)"
by (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
lemma valid_reply_caps_tcb_update:
"\<lbrakk>valid_reply_caps s; ko_at (TCB t) p s; tcb_state t = tcb_state t';
same_caps (TCB t) (TCB t') \<rbrakk>
\<Longrightarrow> valid_reply_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)"
apply (frule_tac P'="same_caps (TCB t')" in obj_at_weakenE, simp)
apply (fastforce simp: valid_reply_caps_def has_reply_cap_def
pred_tcb_at_def obj_at_def fun_upd_def
cte_wp_at_after_update caps_of_state_after_update)
done
lemma valid_reply_masters_tcb_update:
"\<lbrakk>valid_reply_masters s; ko_at (TCB t) p s; tcb_state t = tcb_state t';
same_caps (TCB t) (TCB t') \<rbrakk>
\<Longrightarrow> valid_reply_masters (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)"
by (clarsimp simp: valid_reply_masters_def fun_upd_def is_tcb
cte_wp_at_after_update obj_at_def)
lemma tcb_state_same_cte_wp_at:
"\<lbrakk> ko_at (TCB t) p s; \<forall>(getF, v) \<in> ran tcb_cap_cases. getF t = getF t' \<rbrakk>
\<Longrightarrow> \<forall>P p'. cte_wp_at P p' (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)
= cte_wp_at P p' s"
apply (clarsimp simp add: cte_wp_at_cases obj_at_def)
apply (case_tac "tcb_cap_cases b")
apply simp
apply (drule bspec, erule ranI)
apply clarsimp
done
lemma valid_tcb_state_update:
"\<lbrakk> valid_tcb p t s; valid_tcb_state st s;
case st of
Structures_A.Inactive \<Rightarrow> True
| Structures_A.BlockedOnReceive e data \<Rightarrow>
tcb_caller t = cap.NullCap
\<and> is_master_reply_cap (tcb_reply t)
\<and> obj_ref_of (tcb_reply t) = p
\<and> AllowGrant \<in> cap_rights (tcb_reply t)
| _ \<Rightarrow> is_master_reply_cap (tcb_reply t)
\<and> obj_ref_of (tcb_reply t) = p
\<and> AllowGrant \<in> cap_rights (tcb_reply t) \<rbrakk> \<Longrightarrow>
valid_tcb p (t\<lparr>tcb_state := st\<rparr>) s"
by (simp add: valid_tcb_def valid_tcb_state_def ran_tcb_cap_cases
split: Structures_A.thread_state.splits)
lemma valid_tcb_if_valid_state:
assumes vs: "valid_state s"
assumes somet: "get_tcb thread s = Some y"
shows "valid_tcb thread y s"
proof -
from somet have inran: "kheap s thread = Some (TCB y)"
by (clarsimp simp: get_tcb_def
split: option.splits Structures_A.kernel_object.splits)
from vs have "(\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s)"
by (simp add: valid_state_def valid_pspace_def valid_objs_def)
with inran have "valid_obj thread (TCB y) s" by (fastforce simp: dom_def)
thus ?thesis by (simp add: valid_tcb_def valid_obj_def)
qed
lemma assert_get_tcb_ko:
shows "\<lbrace> P \<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. ko_at (TCB t) thread \<rbrace>"
by (clarsimp simp: valid_def in_monad gets_the_def get_tcb_def
obj_at_def
split: option.splits Structures_A.kernel_object.splits)
lemma gts_st_tcb_at: "\<lbrace>st_tcb_at P t\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: get_thread_state_def thread_get_def)
apply wp
apply (clarsimp simp: pred_tcb_at_def obj_at_def get_tcb_def is_tcb)
done
lemma gts_st_tcb:
"\<lbrace>\<top>\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. rv = st) t\<rbrace>"
apply (simp add: get_thread_state_def thread_get_def)
apply wp
apply (clarsimp simp: pred_tcb_at_def)
done
lemma gbn_bound_tcb:
"\<lbrace>\<top>\<rbrace> get_bound_notification t \<lbrace>\<lambda>rv. bound_tcb_at (\<lambda>ntfn. rv = ntfn) t\<rbrace>"
apply (simp add: get_bound_notification_def thread_get_def)
apply wp
apply (clarsimp simp: pred_tcb_at_def)
done
lemma allActiveTCBs_valid_state:
"\<lbrace>valid_state\<rbrace> allActiveTCBs \<lbrace>\<lambda>R s. valid_state s \<and> (\<forall>t \<in> R. st_tcb_at runnable t s) \<rbrace>"
apply (simp add: allActiveTCBs_def, wp)
apply (simp add: getActiveTCB_def pred_tcb_at_def obj_at_def get_tcb_def
split: option.splits if_split_asm Structures_A.kernel_object.splits)
done
definition
cap_master_cap :: "cap \<Rightarrow> cap"
where
"cap_master_cap cap \<equiv> case cap of
cap.EndpointCap ref bdg rghts \<Rightarrow> cap.EndpointCap ref 0 UNIV
| cap.NotificationCap ref bdg rghts \<Rightarrow> cap.NotificationCap ref 0 UNIV
| cap.CNodeCap ref bits gd \<Rightarrow> cap.CNodeCap ref bits []
| cap.ThreadCap ref \<Rightarrow> cap.ThreadCap ref
| cap.DomainCap \<Rightarrow> cap.DomainCap
| cap.ReplyCap ref master rghts \<Rightarrow> cap.ReplyCap ref True UNIV
| cap.UntypedCap dev ref n f \<Rightarrow> cap.UntypedCap dev ref n 0
| cap.ArchObjectCap acap \<Rightarrow> cap.ArchObjectCap (cap_master_arch_cap acap)
| _ \<Rightarrow> cap"
lemma cap_master_cap_eqDs1:
"cap_master_cap cap = cap.EndpointCap ref bdg rghts
\<Longrightarrow> bdg = 0 \<and> rghts = UNIV
\<and> (\<exists>bdg rghts. cap = cap.EndpointCap ref bdg rghts)"
"cap_master_cap cap = cap.NotificationCap ref bdg rghts
\<Longrightarrow> bdg = 0 \<and> rghts = UNIV
\<and> (\<exists>bdg rghts. cap = cap.NotificationCap ref bdg rghts)"
"cap_master_cap cap = cap.CNodeCap ref bits gd
\<Longrightarrow> gd = [] \<and> (\<exists>gd. cap = cap.CNodeCap ref bits gd)"
"cap_master_cap cap = cap.ThreadCap ref
\<Longrightarrow> cap = cap.ThreadCap ref"
"cap_master_cap cap = cap.DomainCap
\<Longrightarrow> cap = cap.DomainCap"
"cap_master_cap cap = cap.NullCap
\<Longrightarrow> cap = cap.NullCap"
"cap_master_cap cap = cap.IRQControlCap
\<Longrightarrow> cap = cap.IRQControlCap"
"cap_master_cap cap = cap.IRQHandlerCap irq
\<Longrightarrow> cap = cap.IRQHandlerCap irq"
"cap_master_cap cap = cap.Zombie ref tp n
\<Longrightarrow> cap = cap.Zombie ref tp n"
"cap_master_cap cap = cap.UntypedCap dev ref bits 0
\<Longrightarrow> \<exists>f. cap = cap.UntypedCap dev ref bits f"
"cap_master_cap cap = cap.ReplyCap ref master rghts
\<Longrightarrow> master = True \<and> rghts = UNIV
\<and> (\<exists>master rghts. cap = cap.ReplyCap ref master rghts)"
by (clarsimp simp: cap_master_cap_def
split: cap.split_asm)+
lemma cap_master_cap_arch_eqD:
"cap_master_cap cap = ArchObjectCap acap
\<Longrightarrow> \<exists>ac. cap = ArchObjectCap ac \<and> acap = cap_master_arch_cap ac"
by (clarsimp simp: cap_master_cap_def
split: cap.split_asm)+
lemmas cap_master_cap_eqDs =
cap_master_cap_eqDs1 cap_master_cap_arch_eqD
cap_master_cap_eqDs1 [OF sym] cap_master_cap_arch_eqD [OF sym]
definition
cap_badge :: "cap \<rightharpoonup> badge"
where
"cap_badge cap \<equiv> case cap of
cap.EndpointCap r badge rights \<Rightarrow> Some badge
| cap.NotificationCap r badge rights \<Rightarrow> Some badge
| _ \<Rightarrow> None"
lemma cap_badge_simps [simp]:
"cap_badge (cap.EndpointCap r badge rights) = Some badge"
"cap_badge (cap.NotificationCap r badge rights) = Some badge"
"cap_badge (cap.UntypedCap dev p n f) = None"
"cap_badge (cap.NullCap) = None"
"cap_badge (cap.DomainCap) = None"
"cap_badge (cap.CNodeCap r bits guard) = None"
"cap_badge (cap.ThreadCap r) = None"
"cap_badge (cap.DomainCap) = None"
"cap_badge (cap.ReplyCap r master rights) = None"
"cap_badge (cap.IRQControlCap) = None"
"cap_badge (cap.IRQHandlerCap irq) = None"
"cap_badge (cap.Zombie r b n) = None"
"cap_badge (cap.ArchObjectCap cap) = None"
by (auto simp: cap_badge_def)
lemma cdt_parent_of_def:
"m \<turnstile> p cdt_parent_of c \<equiv> m c = Some p"
by (simp add: cdt_parent_rel_def is_cdt_parent_def)
lemmas cdt_parent_defs = cdt_parent_of_def is_cdt_parent_def cdt_parent_rel_def
lemma valid_mdb_no_null:
"\<lbrakk> valid_mdb s; caps_of_state s p = Some cap.NullCap \<rbrakk> \<Longrightarrow>
\<not> cdt s \<Turnstile> p \<rightarrow> p' \<and> \<not> cdt s \<Turnstile> p' \<rightarrow> p"
apply (simp add: valid_mdb_def mdb_cte_at_def cte_wp_at_caps_of_state)
apply (cases p, cases p')
apply (rule conjI)
apply (fastforce dest!: tranclD simp: cdt_parent_defs)
apply (fastforce dest!: tranclD2 simp: cdt_parent_defs)
done
lemma x_sym: "(s = t) = r \<Longrightarrow> (t = s) = r" by auto
lemma set_inter_not_emptyD1: "\<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> A"
by blast
lemma set_inter_not_emptyD2: "\<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> A \<subseteq> B"
by blast
lemma set_inter_not_emptyD3: "\<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> A \<noteq> B"
by blast
lemma untyped_range_in_cap_range: "untyped_range x \<subseteq> cap_range x"
by(simp add: cap_range_def)
lemma set_object_cte_wp_at:
"\<lbrace>\<lambda>s. cte_wp_at P p (kheap_update (\<lambda>ps. (kheap s)(ptr \<mapsto> ko)) s)\<rbrace>
set_object ptr ko
\<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>"
by (wpsimp wp: set_object_wp_strong)
lemma set_cap_cte_wp_at:
"\<lbrace>(\<lambda>s. if p = ptr then P cap else cte_wp_at P p s) and cte_at ptr\<rbrace>
set_cap cap ptr
\<lbrace>\<lambda>uu s. cte_wp_at P p s\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply (wp set_cap_caps_of_state)
apply clarsimp
done
lemma set_cap_cte_wp_at':
"\<lbrace>\<lambda>s. if p = ptr then (P cap \<and> cte_at ptr s) else cte_wp_at P p s\<rbrace>
set_cap cap ptr
\<lbrace>\<lambda>uu s. cte_wp_at P p s\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply (wp set_cap_caps_of_state)
apply clarsimp
done
lemma set_cap_typ_at:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace>
set_cap cap p'
\<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
by (wpsimp wp: set_object_typ_at get_object_wp simp: set_cap_def)
lemma set_cap_a_type_inv:
"((), t) \<in> fst (set_cap cap slot s) \<Longrightarrow> typ_at T p t = typ_at T p s"
apply (subgoal_tac "EX x. typ_at T p s = x")
apply (elim exE)
apply (cut_tac P="(=) x" in set_cap_typ_at[of _ T p cap slot])
apply (fastforce simp: valid_def)
apply fastforce
done
lemma set_cap_tcb:
"\<lbrace>tcb_at p'\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. tcb_at p'\<rbrace>"
by (clarsimp simp: tcb_at_typ intro!: set_cap_typ_at)
lemma set_cap_sets:
"\<lbrace>\<top>\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. c = cap) p s\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply (wp set_cap_caps_of_state)
apply clarsimp
done
lemma set_cap_valid_cap:
"\<lbrace>valid_cap c\<rbrace> set_cap x p \<lbrace>\<lambda>_. valid_cap c\<rbrace>"
by (simp add: valid_cap_typ set_cap_typ_at)
lemma set_cap_cte_at:
"\<lbrace>cte_at p'\<rbrace> set_cap x p \<lbrace>\<lambda>_. cte_at p'\<rbrace>"
by (simp add: valid_cte_at_typ set_cap_typ_at [where P="\<lambda>x. x"])
lemma set_cap_valid_objs:
"\<lbrace>(valid_objs::'state_ext::state_ext state \<Rightarrow> bool) and valid_cap x
and tcb_cap_valid x p\<rbrace>
set_cap x p \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: set_cap_def split_def)
apply (rule bind_wp [OF _ get_object_sp])
apply (case_tac obj, simp_all split del: if_split)
apply clarsimp
apply (wp set_object_valid_objs)
apply (clarsimp simp: obj_at_def a_type_def wf_cs_upd)
apply (erule(1) valid_objsE)
apply (clarsimp simp: valid_obj_def valid_cs_def
valid_cs_size_def wf_cs_upd)
apply (clarsimp simp: ran_def split: if_split_asm)
apply blast
apply (rule hoare_pre, wp set_object_valid_objs)
apply (clarsimp simp: obj_at_def a_type_def tcb_cap_valid_def
is_tcb_def)
apply (erule(1) valid_objsE)
apply (clarsimp simp: valid_obj_def valid_tcb_def
ran_tcb_cap_cases)
apply (intro conjI impI, simp_all add: pred_tcb_at_def obj_at_def)
done
lemma set_cap_aligned [wp]:
"\<lbrace>pspace_aligned\<rbrace>
set_cap c p
\<lbrace>\<lambda>rv. pspace_aligned\<rbrace>"
apply (simp add: set_cap_def split_def)
apply (wp set_object_aligned get_object_wp | wpc)+
apply (auto simp: a_type_def obj_at_def wf_cs_upd fun_upd_def[symmetric])
done
lemma set_cap_refs_of [wp]:
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
set_cap cp p
\<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>"
apply (simp add: set_cap_def set_object_def split_def)
apply (wp get_object_wp | wpc)+
apply (auto elim!: rsubst[where P=P]
simp: state_refs_of_def obj_at_def
intro!: ext
split: if_split_asm)
done
lemma set_cap_distinct [wp]:
"\<lbrace>pspace_distinct\<rbrace> set_cap c p \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>"
apply (simp add: set_cap_def split_def)
apply (wp set_object_distinct get_object_wp | wpc)+
apply (auto simp: a_type_def obj_at_def wf_cs_upd fun_upd_def[symmetric])
done
lemma set_cap_cur [wp]:
"\<lbrace>cur_tcb\<rbrace> set_cap c p \<lbrace>\<lambda>rv. cur_tcb\<rbrace>"
apply (simp add: set_cap_def set_object_def split_def)
apply (wp get_object_wp | wpc)+
apply (clarsimp simp: cur_tcb_def obj_at_def is_tcb)
done
lemma set_cap_pred_tcb [wp]:
"\<lbrace>pred_tcb_at proj P t\<rbrace> set_cap c p \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>"
apply (simp add: set_cap_def set_object_def split_def)
apply (wp get_object_wp | wpc)+
apply (auto simp: pred_tcb_at_def obj_at_def tcb_to_itcb_def)
done
lemma set_cap_live[wp]:
"\<lbrace>\<lambda>s. P (obj_at live p' s)\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. P (obj_at live p' s)\<rbrace>"
apply (simp add: set_cap_def split_def set_object_def)
apply (wp get_object_wp | wpc)+
by (fastforce simp: obj_at_def live_def)
lemma set_cap_cap_to:
"\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. p'\<notin>(zobj_refs cap' - zobj_refs cap)) p s
\<and> ex_nonz_cap_to p' s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. ex_nonz_cap_to p'\<rbrace>"
apply (simp add: ex_nonz_cap_to_def cte_wp_at_caps_of_state)
apply wp
apply simp
apply (elim conjE exE)
apply (case_tac "(a, b) = p")
apply fastforce
apply fastforce
done
crunch set_cap
for irq_node[wp]: "\<lambda>s. P (interrupt_irq_node s)"
(simp: crunch_simps)
lemma set_cap_cte_cap_wp_to:
"\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> P cap'
\<longrightarrow> p' \<in> cte_refs cap (interrupt_irq_node s) \<and> P cap) p s
\<and> ex_cte_cap_wp_to P p' s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p'\<rbrace>"
apply (simp add: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state del: split_paired_Ex)
apply (wp hoare_vcg_ex_lift)
apply clarify
by (metis fun_upd_other fun_upd_same option.sel)
lemma set_cap_iflive:
"\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>p'\<in>(zobj_refs cap' - zobj_refs cap). obj_at (Not \<circ> live) p' s) p s
\<and> if_live_then_nonz_cap s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>"
apply (simp add: if_live_then_nonz_cap_def)
apply (simp only: imp_conv_disj)
apply (rule hoare_pre, wp hoare_vcg_all_lift hoare_vcg_disj_lift set_cap_cap_to)
apply (clarsimp simp: cte_wp_at_def)
apply (rule ccontr)
apply (drule bspec)
apply simp
apply (clarsimp simp: obj_at_def)
done
lemma update_cap_iflive:
"\<lbrace>cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs cap) p
and if_live_then_nonz_cap\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>"
apply (wp set_cap_iflive)
apply (clarsimp elim!: cte_wp_at_weakenE)
done
lemma set_cap_ifunsafe:
"\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>p'. p' \<in> cte_refs cap' (interrupt_irq_node s)
\<and> (p' \<notin> cte_refs cap (interrupt_irq_node s)
\<or> (\<exists>cp. appropriate_cte_cap cp cap'
\<and> \<not> appropriate_cte_cap cp cap))
\<longrightarrow>
(p' \<noteq> p \<longrightarrow> cte_wp_at ((=) cap.NullCap) p' s)
\<and> (p' = p \<longrightarrow> cap = cap.NullCap)) p s
\<and> if_unsafe_then_cap s
\<and> (cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>"
apply (simp add: if_unsafe_then_cap_def)
apply (wp set_cap_cte_cap_wp_to hoare_vcg_all_lift hoare_vcg_imp_lift)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (rule ccontr, clarsimp)
apply (drule spec, drule spec, drule(1) mp [OF _ conjI])
apply auto[2]
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (fastforce simp: Ball_def)
done
lemma update_cap_ifunsafe:
"\<lbrace>cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs cap
\<and> (\<forall>cp. appropriate_cte_cap cp cap'
= appropriate_cte_cap cp cap)) p
and if_unsafe_then_cap
and (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>"
apply (wp set_cap_ifunsafe)
apply (clarsimp elim!: cte_wp_at_weakenE)
done
crunch set_cap
for it[wp]: "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps simp: crunch_simps)
lemma set_cap_refs [wp]:
"\<lbrace>\<lambda>x. P (global_refs x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (global_refs x)\<rbrace>"
by (rule global_refs_lift) wp+
lemma set_cap_globals [wp]:
"\<lbrace>valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range cap = {})\<rbrace>
set_cap cap p
\<lbrace>\<lambda>_. valid_global_refs\<rbrace>"
apply (simp add: valid_global_refs_def valid_refs_def2 Ball_def)
apply (wp set_cap_caps_of_state hoare_vcg_all_lift hoare_vcg_imp_lift)
apply (clarsimp simp: ran_def)
apply blast
done
lemma set_cap_pspace:
assumes x: "\<And>s f'. f (kheap_update f' s) = f s"
shows "\<lbrace>\<lambda>s. P (f s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. P (f s)\<rbrace>"
apply (simp add: set_cap_def split_def)
apply (rule bind_wp [OF _ get_object_sp])
apply (case_tac obj, simp_all split del: if_split cong: if_cong)
apply (wpsimp wp: set_object_wp simp: x)+
done
lemma set_cap_rvk_cdt_ct_ms[wp]:
"\<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. P (is_original_cap s)\<rbrace>"
"\<lbrace>\<lambda>s. Q (cur_thread s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. Q (cur_thread s)\<rbrace>"
"\<lbrace>\<lambda>s. R (machine_state s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. R (machine_state s)\<rbrace>"
"\<lbrace>\<lambda>s. S (cdt s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. S (cdt s)\<rbrace>"
"\<lbrace>\<lambda>s. T (idle_thread s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. T (idle_thread s)\<rbrace>"
"\<lbrace>\<lambda>s. U (arch_state s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. U (arch_state s)\<rbrace>"
by (rule set_cap_pspace | simp)+
lemma obvious:
"\<lbrakk> S = {a}; x \<noteq> y; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> P"
by blast
lemma obvious2:
"\<lbrakk> x \<in> S; \<And>y. y \<noteq> x \<Longrightarrow> y \<notin> S \<rbrakk> \<Longrightarrow> \<exists>x. S = {x}"
by blast
lemma is_final_cap'_def3:
"is_final_cap' cap = (\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref s
\<and> (\<forall>cref'. (cte_at cref' s \<and> cref' \<noteq> cref)
\<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c = {}) cref' s))"
apply (clarsimp simp: is_final_cap'_def2
intro!: ext arg_cong[where f=Ex])
apply (subst iff_conv_conj_imp)
apply (clarsimp simp: all_conj_distrib conj_comms)
apply (rule rev_conj_cong[OF _ refl])
apply (rule arg_cong[where f=All] ext)+
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply fastforce
done
lemma final_cap_at_eq:
"cte_wp_at (\<lambda>c. is_final_cap' c s) p s =
(\<exists>cp. cte_wp_at (\<lambda>c. c = cp) p s \<and> (gen_obj_refs cp \<noteq> {})
\<and> (\<forall>p'. (cte_at p' s \<and> p' \<noteq> p) \<longrightarrow>
cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s))"
apply (clarsimp simp: is_final_cap'_def3 cte_wp_at_caps_of_state
simp del: split_paired_Ex split_paired_All)
apply (rule iffI)
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (rule conjI)
apply clarsimp
apply (subgoal_tac "(a, b) = p")
apply (erule allEI)
apply clarsimp
apply (erule_tac x=p in allE)
apply fastforce
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (rule_tac x=p in exI)
apply (clarsimp simp del: split_paired_Ex split_paired_All)
done
lemma zombie_has_refs:
"is_zombie cap \<Longrightarrow> gen_obj_refs cap \<noteq> {}"
by (clarsimp simp: is_cap_simps cap_irqs_def cap_irq_opt_def
gen_obj_refs_def
split: sum.split_asm)
lemma zombie_cap_irqs:
"is_zombie cap \<Longrightarrow> cap_irqs cap = {}"
by (clarsimp simp: is_cap_simps)
lemma zombie_cap_arch_gen_obj_refs:
"is_zombie cap \<Longrightarrow> arch_gen_refs cap = {}"
by (clarsimp simp: is_cap_simps)
lemma zombies_final_def2:
"zombies_final = (\<lambda>s. \<forall>p p' cap cap'. (cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s
\<and> (obj_refs cap \<inter> obj_refs cap' \<noteq> {}) \<and> p \<noteq> p')
\<longrightarrow> (\<not> is_zombie cap \<and> \<not> is_zombie cap'))"
unfolding zombies_final_def
apply (rule ext)
apply (rule iffI)
apply (intro allI impI conjI notI)
apply (elim conjE)
apply (simp only: simp_thms conj_commute final_cap_at_eq cte_wp_at_def)
apply (elim allE, drule mp, rule exI, erule(1) conjI)
apply (elim exE conjE)
apply (drule spec, drule mp, rule conjI, erule not_sym)
apply simp
apply (clarsimp simp: gen_obj_refs_Int)
apply (elim conjE)
apply (simp only: simp_thms conj_commute final_cap_at_eq cte_wp_at_def)
apply (elim allE, drule mp, rule exI, erule(1) conjI)
apply (elim exE conjE)
apply (drule spec, drule mp, erule conjI)
apply simp
apply (clarsimp simp: Int_commute gen_obj_refs_Int)
apply (clarsimp simp: final_cap_at_eq cte_wp_at_def
zombie_has_refs gen_obj_refs_Int
zombie_cap_irqs
simp del: split_paired_Ex)
apply (rule ccontr)
apply (elim allE, erule impE, (erule conjI)+)
apply (clarsimp simp: is_cap_simps)
apply clarsimp
done
lemma zombies_finalD2:
"\<lbrakk> fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)};
p \<noteq> p'; zombies_final s; obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<rbrakk>
\<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'"
by (simp only: zombies_final_def2 cte_wp_at_def simp_thms conj_comms)
lemma zombies_finalD3:
"\<lbrakk> cte_wp_at P p s; cte_wp_at P' p' s; p \<noteq> p'; zombies_final s;
\<And>cap cap'. \<lbrakk> P cap; P' cap' \<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<rbrakk>
\<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) p s \<and> cte_wp_at (Not \<circ> is_zombie) p' s"
apply (clarsimp simp: cte_wp_at_def)
apply (erule(3) zombies_finalD2)
apply simp
done
lemma set_cap_final_cap_at:
"\<lbrace>\<lambda>s. is_final_cap' cap' s \<and>
cte_wp_at (\<lambda>cap''. (gen_obj_refs cap'' \<inter> gen_obj_refs cap' \<noteq> {})
= (gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {})) p s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace>"
apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state)
apply wp
apply (elim conjE exEI allEI)
apply (clarsimp simp: Int_commute)
done
lemma set_cap_zombies':
"\<lbrace>\<lambda>s. zombies_final s
\<and> cte_wp_at (\<lambda>cap'. \<forall>p' cap''. (cte_wp_at ((=) cap'') p' s \<and> p \<noteq> p'
\<and> (obj_refs cap \<inter> obj_refs cap'' \<noteq> {})
\<longrightarrow> (\<not> is_zombie cap \<and> \<not> is_zombie cap''))) p s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. zombies_final\<rbrace>"
apply (simp add: zombies_final_def2 cte_wp_at_caps_of_state)
apply (rule hoare_pre, wp)
apply clarsimp
apply (metis Int_commute prod.inject)
done
fun ex_zombie_refs :: "(cap \<times> cap) \<Rightarrow> obj_ref set"
where
"ex_zombie_refs (c1, c2) =
(case c1 of
cap.Zombie p b n \<Rightarrow>
(case c2 of
cap.Zombie p' b' n' \<Rightarrow>
(obj_refs (cap.Zombie p b n) - obj_refs (cap.Zombie p' b' n'))
| _ \<Rightarrow>
obj_refs (cap.Zombie p b n))
| _ \<Rightarrow> obj_refs c1 - obj_refs c2)"
declare ex_zombie_refs.simps [simp del]
lemmas ex_zombie_refs_simps [simp]
= ex_zombie_refs.simps[split_simps cap.split, simplified]
lemma ex_zombie_refs_def2:
"ex_zombie_refs (cap, cap') =
(if is_zombie cap
then if is_zombie cap'
then obj_refs cap - obj_refs cap'
else obj_refs cap
else obj_refs cap - obj_refs cap')"
by (simp add: is_zombie_def split: cap.splits split del: if_split)
lemma set_cap_zombies:
"\<lbrace>\<lambda>s. zombies_final s
\<and> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'.
(p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s)
\<longrightarrow> (cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap)) p s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. zombies_final\<rbrace>"
apply (wp set_cap_zombies')
apply (clarsimp simp: cte_wp_at_def elim!: nonemptyE)
apply (subgoal_tac "x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa")
prefer 2
apply (rule impI)
apply (drule(3) zombies_finalD2)
apply clarsimp
apply blast
apply simp
apply (simp only: ex_zombie_refs_def2 split: if_split_asm)
apply simp
apply (drule bspec, simp)
apply (elim allE, erule disjE, erule(1) notE)
apply simp
apply simp
apply (drule(1) bspec, elim allE, erule disjE, erule(1) notE)
apply simp
apply simp
apply (erule impCE)
apply (drule bspec, simp)
apply (elim allE, erule impE, erule conjI)
apply simp
apply simp
apply simp
done
lemma set_cap_obj_at_other:
"\<lbrace>\<lambda>s. P (obj_at P' p s) \<and> p \<noteq> fst p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>"
apply (simp add: set_cap_def split_def)
apply (rule bind_wp [OF _ get_object_inv])
apply (case_tac obj, simp_all split del: if_split)
apply (wpsimp wp: set_object_wp simp: obj_at_def)+
done
lemma new_cap_iflive:
"\<lbrace>cte_wp_at ((=) cap.NullCap) p
and if_live_then_nonz_cap\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>"
by (wp set_cap_iflive, clarsimp elim!: cte_wp_at_weakenE)
lemma new_cap_ifunsafe:
"\<lbrace>cte_wp_at ((=) cap.NullCap) p
and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) p\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>"
by (wp set_cap_ifunsafe, clarsimp elim!: cte_wp_at_weakenE)
lemma ex_zombie_refs_Null[simp]:
"ex_zombie_refs (c, cap.NullCap) = obj_refs c"
by (simp add: ex_zombie_refs_def2)
lemma new_cap_zombies:
"\<lbrace>\<lambda>s. cte_wp_at ((=) cap.NullCap) p s \<and>
(\<forall>r\<in>obj_refs cap. \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s
\<longrightarrow> (cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap))
\<and> zombies_final s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. zombies_final\<rbrace>"
apply (wp set_cap_zombies)
apply (clarsimp elim!: cte_wp_at_weakenE)
done
lemma new_cap_valid_pspace:
"\<lbrace>cte_wp_at ((=) cap.NullCap) p and valid_cap cap