-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCSpace_R.thy
14048 lines (12996 loc) · 541 KB
/
CSpace_R.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)
*)
(*
CSpace refinement
*)
theory CSpace_R
imports
CSpace_I
"../invariant-abstract/DetSchedSchedule_AI"
begin
lemma isMDBParentOf_CTE1:
"isMDBParentOf (CTE cap node) cte =
(\<exists>cap' node'. cte = CTE cap' node' \<and> sameRegionAs cap cap'
\<and> mdbRevocable node
\<and> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> 0 \<longrightarrow>
capEPBadge cap = capEPBadge cap' \<and> \<not> mdbFirstBadged node')
\<and> (isAsyncEndpointCap cap \<longrightarrow> capAEPBadge cap \<noteq> 0 \<longrightarrow>
capAEPBadge cap = capAEPBadge cap' \<and> \<not> mdbFirstBadged node'))"
apply (simp add: isMDBParentOf_def Let_def split: cte.splits split del: split_if)
apply (clarsimp simp: Let_def)
apply (fastforce simp: isCap_simps)
done
lemma isMDBParentOf_CTE:
"isMDBParentOf (CTE cap node) cte =
(\<exists>cap' node'. cte = CTE cap' node' \<and> sameRegionAs cap cap'
\<and> mdbRevocable node
\<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'))"
apply (simp add: isMDBParentOf_CTE1)
apply (intro arg_cong[where f=Ex] ext conj_cong refl)
apply (cases cap, simp_all add: isCap_simps)
apply (auto elim!: sameRegionAsE simp: isCap_simps)
done
lemma isMDBParentOf_trans:
"\<lbrakk> isMDBParentOf a b; isMDBParentOf b c \<rbrakk> \<Longrightarrow> isMDBParentOf a c"
apply (cases a)
apply (clarsimp simp: isMDBParentOf_CTE)
apply (frule(1) sameRegionAs_trans, simp)
apply (erule(1) capBadge_ordering_trans)
done
lemma parentOf_trans:
"\<lbrakk> s \<turnstile> a parentOf b; s \<turnstile> b parentOf c \<rbrakk> \<Longrightarrow> s \<turnstile> a parentOf c"
by (auto simp: parentOf_def elim: isMDBParentOf_trans)
lemma subtree_parent:
"s \<turnstile> a \<rightarrow> b \<Longrightarrow> s \<turnstile> a parentOf b"
by (erule subtree.induct) auto
lemma leadsto_is_prev:
"\<lbrakk> m \<turnstile> p \<leadsto> c; m c = Some (CTE cap node);
valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow>
p = mdbPrev node"
by (fastforce simp add: next_unfold' valid_dlist_def Let_def no_0_def)
lemma subtree_target_Some:
"m \<turnstile> a \<rightarrow> b \<Longrightarrow> m b \<noteq> None"
by (erule subtree.cases) (auto simp: parentOf_def)
lemma subtree_prev_loop:
"\<lbrakk> m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow>
m \<turnstile> p \<rightarrow> mdbPrev node = False"
apply clarsimp
apply (frule subtree_target_Some)
apply (drule subtree_mdb_next)
apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ p")
apply (simp add: no_loops_def)
apply (erule trancl_into_trancl)
apply (clarsimp simp: mdb_next_unfold)
apply (fastforce simp: next_unfold' valid_dlist_def no_0_def Let_def)
done
lemma subtree_trans_lemma:
assumes "s \<turnstile> b \<rightarrow> c"
shows "s \<turnstile> a \<rightarrow> b \<Longrightarrow> s \<turnstile> a \<rightarrow> c"
using assms
proof induct
case direct_parent
thus ?case
by (blast intro: trans_parent parentOf_trans subtree_parent)
next
case (trans_parent y z)
have IH: "s \<turnstile> a \<rightarrow> b \<Longrightarrow> s \<turnstile> a \<rightarrow> y" by fact+
have step: "s \<turnstile> y \<leadsto> z" "z \<noteq> 0" "s \<turnstile> b parentOf z" by fact+
have "s \<turnstile> a \<rightarrow> b" by fact+
hence "s \<turnstile> a \<rightarrow> y" and "s \<turnstile> a parentOf b" by (auto intro: IH subtree_parent)
moreover
with step
have "s \<turnstile> a parentOf z" by - (rule parentOf_trans)
ultimately
show ?case using step by - (rule subtree.trans_parent)
qed
lemma subtree_trans: "\<lbrakk> s \<turnstile> a \<rightarrow> b; s \<turnstile> b \<rightarrow> c \<rbrakk> \<Longrightarrow> s \<turnstile> a \<rightarrow> c"
by (rule subtree_trans_lemma)
lemma same_arch_region_as_relation:
"\<lbrakk>acap_relation c d; acap_relation c' d'\<rbrakk> \<Longrightarrow>
arch_same_region_as c c' =
sameRegionAs (ArchObjectCap d) (ArchObjectCap d')"
apply (cases c)
apply ((cases c', auto simp: ArchRetype_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)[1])+
done
lemma is_phyiscal_relation:
"cap_relation c c' \<Longrightarrow> is_physical c = isPhysicalCap c'"
by (auto simp: is_physical_def arch_is_physical_def
split: cap.splits arch_cap.splits)
lemma obj_ref_of_relation:
"\<lbrakk> cap_relation c c'; capClass c' = PhysicalClass \<rbrakk> \<Longrightarrow>
obj_ref_of c = capUntypedPtr c'"
by (cases c, simp_all) (case_tac arch_cap, auto)
lemma obj_size_relation:
"\<lbrakk> cap_relation c c'; capClass c' = PhysicalClass \<rbrakk> \<Longrightarrow>
obj_size c = capUntypedSize c'"
apply (cases c, simp_all add: objBits_def objBitsKO_def zbits_map_def
cte_level_bits_def
split: option.splits sum.splits)
apply (case_tac arch_cap,
simp_all add: objBits_def ArchRetype_H.capUntypedSize_def asid_low_bits_def
pageBits_def)
done
lemma same_region_as_relation:
"\<lbrakk> cap_relation c d; cap_relation c' d' \<rbrakk> \<Longrightarrow>
same_region_as c c' = sameRegionAs d d'"
apply (cases c)
apply clarsimp
apply (clarsimp simp: sameRegionAs_def isCap_simps Let_def is_phyiscal_relation)
apply (auto simp: obj_ref_of_relation obj_size_relation cong: conj_cong)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def bits_of_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1]
apply simp
apply (cases c')
apply (clarsimp simp: same_arch_region_as_relation|
clarsimp simp: sameRegionAs_def isCap_simps Let_def)+
done
lemma can_be_is:
"\<lbrakk> cap_relation c (cteCap cte); cap_relation c' (cteCap cte');
mdbRevocable (cteMDBNode cte) = r;
mdbFirstBadged (cteMDBNode cte') = r' \<rbrakk> \<Longrightarrow>
should_be_parent_of c r c' r' = isMDBParentOf cte cte'"
unfolding should_be_parent_of_def isMDBParentOf_def
apply (cases cte)
apply (cases cte')
apply (clarsimp split del: split_if)
apply (case_tac "mdbRevocable mdbnode")
prefer 2
apply simp
apply (clarsimp split del: split_if)
apply (case_tac "RetypeDecls_H.sameRegionAs capability capabilitya")
prefer 2
apply (simp add: same_region_as_relation)
apply (simp add: same_region_as_relation split del: split_if)
apply (cases c, simp_all add: isCap_simps)
apply (cases c', auto simp: sameRegionAs_def Let_def isCap_simps)[1]
apply (cases c', auto simp: sameRegionAs_def isCap_simps is_cap_simps)[1]
apply (auto simp: Let_def)[1]
done
lemma no_fail_getCTE [wp]:
"no_fail (cte_at' p) (getCTE p)"
apply (simp add: getCTE_def getObject_def split_def
loadObject_cte alignCheck_def unless_def
alignError_def is_aligned_mask[symmetric]
cong: kernel_object.case_cong)
apply (rule no_fail_pre, (wp | wpc)+)
apply (clarsimp simp: cte_wp_at'_def getObject_def
loadObject_cte split_def in_monad
dest!: in_singleton
split del: split_if)
apply (clarsimp simp: in_monad typeError_def objBits_simps
magnitudeCheck_def
split: kernel_object.split_asm split_if_asm option.split_asm
split del: split_if)
apply simp+
done
lemma tcb_cases_related:
"tcb_cap_cases ref = Some (getF, setF, restr) \<Longrightarrow>
\<exists>getF' setF'. (\<forall>x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF'))
\<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')))"
by (simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1
cte_map_def tcb_relation_def
split: split_if_asm)
lemma pspace_relation_cte_wp_at:
"\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
cte_wp_at (op = c) (cref, oref) s; pspace_aligned' s';
pspace_distinct' s' \<rbrakk>
\<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'"
apply (simp add: cte_wp_at_cases)
apply (erule disjE)
apply clarsimp
apply (drule(1) pspace_relation_absD)
apply (simp add: unpleasant_helper)
apply (drule spec, drule mp, erule domI)
apply (clarsimp simp: cte_relation_def)
apply (drule(2) aligned_distinct_obj_atI'[where 'a=cte])
apply simp
apply (drule ko_at_imp_cte_wp_at')
apply (clarsimp elim!: cte_wp_at_weakenE')
apply clarsimp
apply (drule(1) pspace_relation_absD)
apply (clarsimp simp: other_obj_relation_def)
apply (simp split: kernel_object.split_asm)
apply (drule(2) aligned_distinct_obj_atI'[where 'a=tcb])
apply simp
apply (drule tcb_cases_related)
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps)
apply (erule(2) cte_wp_at_tcbI')
apply fastforce
apply simp
done
lemma pspace_relation_ctes_ofI:
"\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
cte_wp_at (op = c) slot s; pspace_aligned' s';
pspace_distinct' s' \<rbrakk>
\<Longrightarrow> \<exists>cte. ctes_of s' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)"
apply (cases slot, clarsimp)
apply (drule(3) pspace_relation_cte_wp_at)
apply (simp add: cte_wp_at_ctes_of)
done
lemma get_cap_corres_P:
"corres (\<lambda>x y. cap_relation x (cteCap y) \<and> P x)
(cte_wp_at P cslot_ptr)
(pspace_aligned' and pspace_distinct')
(get_cap cslot_ptr) (getCTE (cte_map cslot_ptr))"
apply (rule corres_stronger_no_failI)
apply (rule no_fail_pre, wp)
apply clarsimp
apply (drule cte_wp_at_norm)
apply (clarsimp simp: state_relation_def)
apply (drule (3) pspace_relation_ctes_ofI)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (cases cslot_ptr)
apply (rename_tac oref cref)
apply (clarsimp simp: cte_wp_at_def)
apply (frule in_inv_by_hoareD[OF getCTE_inv])
apply (drule use_valid [where P="\<top>", OF _ getCTE_sp TrueI])
apply (clarsimp simp: state_relation_def)
apply (drule pspace_relation_ctes_ofI)
apply (simp add: cte_wp_at_def)
apply assumption+
apply (clarsimp simp: cte_wp_at_ctes_of)
done
lemmas get_cap_corres = get_cap_corres_P[where P="\<top>", simplified]
lemma cap_relation_masks:
"cap_relation c c' \<Longrightarrow> cap_relation
(cap_rights_update (cap_rights c \<inter> rmask) c)
(RetypeDecls_H.maskCapRights (rights_mask_map rmask) c')"
apply (case_tac c, simp_all add: isCap_defs maskCapRights_def Let_def
rights_mask_map_def maskVMRights_def
AllowSend_def AllowRecv_def
cap_rights_update_def
split del: split_if)
apply (clarsimp simp add: isCap_defs)
by (rule ArchAcc_R.arch_cap_rights_update
[simplified, simplified rights_mask_map_def])
lemma getCTE_wp:
"\<lbrace>\<lambda>s. cte_at' p s \<longrightarrow> (\<exists>cte. cte_wp_at' (op = cte) p s \<and> Q cte s)\<rbrace> getCTE p \<lbrace>Q\<rbrace>"
apply (clarsimp simp add: getCTE_def valid_def cte_wp_at'_def)
apply (drule getObject_cte_det)
apply clarsimp
done
lemma getCTE_ctes_of:
"\<lbrace>\<lambda>s. ctes_of s p \<noteq> None \<longrightarrow> P (the (ctes_of s p)) (ctes_of s)\<rbrace> getCTE p \<lbrace>\<lambda>rv s. P rv (ctes_of s)\<rbrace>"
apply (wp getCTE_wp)
apply (clarsimp simp: cte_wp_at_ctes_of)
done
lemma getCTE_ctes_of_weakened:
"\<lbrace>\<lambda>s. P (the (ctes_of s p)) (ctes_of s)\<rbrace> getCTE p \<lbrace>\<lambda>rv s. P rv (ctes_of s)\<rbrace>"
by (wp getCTE_ctes_of, simp)
lemma getCTE_wp':
"\<lbrace>\<lambda>s. \<forall>cte. cte_wp_at' (op = cte) p s \<longrightarrow> Q cte s\<rbrace> getCTE p \<lbrace>Q\<rbrace>"
apply (clarsimp simp add: getCTE_def valid_def cte_wp_at'_def)
apply (drule getObject_cte_det)
apply clarsimp
done
lemma getSlotCap_corres:
"cte_ptr' = cte_map cte_ptr \<Longrightarrow>
corres cap_relation
(cte_at cte_ptr)
(pspace_distinct' and pspace_aligned')
(get_cap cte_ptr)
(getSlotCap cte_ptr')"
apply (simp add: getSlotCap_def)
apply (subst bind_return [symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ get_cap_corres])
apply (rule corres_trivial, simp)
apply (wp | simp)+
done
lemma maskCapRights [simp]:
"cap_relation c c' \<Longrightarrow>
cap_relation (mask_cap msk c) (maskCapRights (rights_mask_map msk) c')"
by (simp add: mask_cap_def cap_relation_masks)
lemma maskCap_valid [simp]:
"s \<turnstile>' RetypeDecls_H.maskCapRights R cap = s \<turnstile>' cap"
by (simp add: valid_cap'_def maskCapRights_def isCap_simps
capAligned_def ArchRetype_H.maskCapRights_def
split: capability.split arch_capability.split
split del: split_if)
lemma getSlotCap_valid_cap:
"\<lbrace>valid_objs'\<rbrace> getSlotCap t \<lbrace>\<lambda>r. valid_cap' r and cte_at' t\<rbrace>"
apply (simp add: getSlotCap_def)
apply (wp getCTE_valid_cap | simp)+
done
lemmas getSlotCap_valid_cap1 [wp] = getSlotCap_valid_cap [THEN hoare_conjD1]
lemmas getSlotCap_valid_cap2 [wp] = getSlotCap_valid_cap [THEN hoare_conjD2]
lemma resolveAddressBits_real_cte_at':
"\<lbrace> valid_objs' and valid_cap' cap \<rbrace>
resolveAddressBits cap addr depth
\<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -"
proof (induct rule: resolveAddressBits.induct)
case (1 cap addr depth)
show ?case
apply (clarsimp simp: validE_def validE_R_def valid_def split: sum.split)
apply (subst (asm) resolveAddressBits.simps)
apply (simp only: Let_def split: split_if_asm)
prefer 2
apply (simp add: in_monad)
apply (simp only: in_bindE_R K_bind_def)
apply (elim exE conjE)
apply (simp only: split: split_if_asm)
apply (clarsimp simp: in_monad locateSlot_def)
apply (cases cap)
apply (simp_all add: isCap_defs)[12]
apply (clarsimp simp add: valid_cap'_def objBits_simps)
apply (simp only: in_bindE_R K_bind_def)
apply (elim exE conjE)
apply (simp only: cap_case_CNodeCap split: split_if_asm)
apply (drule_tac cap=nextCap in isCapDs(4), elim exE)
apply (simp only: in_bindE_R K_bind_def)
apply (frule (12) 1 [OF refl], (assumption | rule refl)+)
apply (clarsimp simp: in_monad locateSlot_def objBits_simps)
apply (cases cap)
apply (simp_all add: isCap_defs)[12]
apply (frule in_inv_by_hoareD [OF getSlotCap_inv])
apply simp
apply (frule (1) post_by_hoare [OF getSlotCap_valid_cap])
apply (simp add: valid_def validE_def validE_R_def)
apply (erule allE, erule impE, blast)
apply (drule (1) bspec)
apply simp
apply (clarsimp simp: in_monad locateSlot_def objBits_simps)
apply (cases cap)
apply (simp_all add: isCap_defs)[12]
apply (frule in_inv_by_hoareD [OF getSlotCap_inv])
apply (clarsimp simp: valid_cap'_def)
done
qed
lemma resolveAddressBits_cte_at':
"\<lbrace> valid_objs' and valid_cap' cap \<rbrace>
resolveAddressBits cap addr depth
\<lbrace>\<lambda>rv. cte_at' (fst rv)\<rbrace>, \<lbrace>\<lambda>rv s. True\<rbrace>"
apply (fold validE_R_def)
apply (rule hoare_post_imp_R)
apply (rule resolveAddressBits_real_cte_at')
apply (erule real_cte_at')
done
declare AllowSend_def[simp]
declare AllowRecv_def[simp]
lemma cap_map_update_data:
assumes "cap_relation c c'"
shows "cap_relation (update_cap_data p x c) (updateCapData p x c')"
proof -
note simps = update_cap_data_def updateCapData_def word_size
isCap_defs is_cap_defs Let_def
cap_rights_update_def badge_update_def
{ fix x :: word32
def y \<equiv> "(x >> 8) && mask 18"
def z \<equiv> "unat ((x >> 3) && mask 5)"
have "of_bl (to_bl (y && mask z)) = (of_bl (replicate (32-z) False @ drop (32-z) (to_bl y))::word32)"
by (simp add: bl_and_mask)
then
have "y && mask z = of_bl (drop (32 - z) (to_bl y))"
apply simp
apply (subst test_bit_eq_iff [symmetric])
apply (rule ext)
apply (clarsimp simp: test_bit_of_bl nth_append)
done
} note x = this
from assms
show ?thesis
apply (cases c)
apply (simp_all add: simps)[5]
defer
apply (simp_all add: simps)[4]
apply (clarsimp simp: simps the_arch_cap_def)
apply (case_tac arch_cap)
apply (simp_all add: simps arch_update_cap_data_def
ArchRetype_H.updateCapData_def)[5]
-- CNodeCap
apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
rightsFromWord_def data_to_rights_def nth_ucast)
apply (insert x)
apply (subgoal_tac "unat ((x >> 3) && mask 5) < unat (2^5::word32)")
prefer 2
apply (fold word_less_nat_alt)[1]
apply (rule and_mask_less_size)
apply (simp add: word_size)
apply (simp add: word_bw_assocs)
done
qed
lemma cte_map_shift:
assumes bl: "to_bl cref' = zs @ cref"
assumes pre: "guard \<le> cref"
assumes len: "cbits + length guard \<le> length cref"
assumes aligned: "is_aligned ptr (4 + cbits)"
assumes cbits: "cbits \<le> word_bits - cte_level_bits"
shows
"ptr + 16 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) =
cte_map (ptr, take cbits (drop (length guard) cref))"
proof -
let ?l = "length cref - (cbits + length guard)"
from pre obtain xs where
xs: "cref = guard @ xs" by (auto simp: prefixeq_def less_eq_list_def)
hence len_c: "length cref = length guard + length xs" by simp
with len have len_x: "cbits \<le> length xs" by simp
from bl xs
have cref': "to_bl cref' = zs @ guard @ xs" by simp
hence "length (to_bl cref') = length \<dots>" by simp
hence 32: "32 = length zs + length guard + length xs" by simp
have len_conv [simp]: "size ptr = word_bits"
by (simp add: word_size word_bits_def)
have "to_bl ((cref' >> ?l) && mask cbits) = (replicate (32 - cbits) False) @
drop (32 - cbits) (to_bl (cref' >> ?l))"
by (simp add: bl_shiftl word_size bl_and_mask
cte_level_bits_def word_bits_def)
also
from len_c len_x cref' 32
have "\<dots> = (replicate (32 - cbits) False) @ take cbits xs"
by (simp add: bl_shiftr word_size add_ac)
also
from len_x len_c 32
have "\<dots> = to_bl (of_bl (take cbits (drop (length guard) cref)) :: word32)"
by (simp add: xs word_rev_tf takefill_alt rev_take rev_drop)
finally
show ?thesis
by (simp add: cte_map_def)
qed
lemma cte_map_shift':
"\<lbrakk> to_bl cref' = zs @ cref; guard \<le> cref; length cref = cbits + length guard;
is_aligned ptr (4 + cbits); cbits \<le> word_bits - cte_level_bits \<rbrakk> \<Longrightarrow>
ptr + 16 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)"
by (auto dest: cte_map_shift)
lemma cap_relation_Null2 [simp]:
"cap_relation c NullCap = (c = cap.NullCap)"
by (cases c) auto
lemma cnode_cap_case_if:
"(case c of CNodeCap _ _ _ _ \<Rightarrow> f | _ \<Rightarrow> g) = (if isCNodeCap c then f else g)"
by (auto simp: isCap_simps split: capability.splits)
declare resolve_address_bits'.simps[simp del]
lemma rab_corres':
"\<lbrakk> cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a;
bits = length (snd a) \<rbrakk> \<Longrightarrow>
corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
cte' = cte_map cte \<and> length bits = bits'))
(valid_objs and pspace_aligned and valid_cap (fst a))
(valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c')
(resolve_address_bits a)
(resolveAddressBits c' cref' bits)"
unfolding resolve_address_bits_def
proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
case (1 z cap cref)
show ?case
proof (cases "isCNodeCap c'")
case True
with "1.prems"
obtain ptr guard' guard cbits where caps:
"cap = cap.CNodeCap ptr cbits guard"
"c' = CNodeCap ptr cbits (of_bl guard) (length guard)"
apply (cases cap, simp_all add: isCap_defs)
apply auto
done
with "1.prems"
have IH: "\<And>vd vc c' f' cref' bits.
\<lbrakk> cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref;
vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap;
cap_relation vd c'; bits = length vc; is_cnode_cap vd;
drop (32 - bits) (to_bl cref') = vc \<rbrakk>
\<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
cte' = cte_map cte \<and> length bits = bits'))
(valid_objs and pspace_aligned and (\<lambda>s. s \<turnstile> fst (vd,vc)))
(valid_objs' and pspace_distinct' and pspace_aligned' and (\<lambda>s. s \<turnstile>' c'))
(resolve_address_bits' z (vd, vc))
(CSpace_H.resolveAddressBits c' cref' bits)"
apply -
apply (rule "1.hyps" [of _ cbits guard, OF caps(1)])
prefer 7
apply (clarsimp simp: in_monad)
apply (rule get_cap_success)
apply (auto simp: in_monad intro!: get_cap_success) (* takes time *)
done
note split_if [split del]
{ assume "cbits + length guard = 0 \<or> cbits = 0 \<and> guard = []"
hence ?thesis
apply (simp add: caps isCap_defs
resolveAddressBits.simps resolve_address_bits'.simps)
apply (rule corres_fail)
apply (clarsimp simp: valid_cap_def)
done
}
moreover
{ assume "cbits + length guard \<noteq> 0 \<and> \<not>(cbits = 0 \<and> guard = [])"
hence [simp]: "((cbits + length guard = 0) = False) \<and>
((cbits = 0 \<and> guard = []) = False) \<and>
(0 < cbits \<or> guard \<noteq> []) " by simp
note split_if [split del]
from "1.prems"
have ?thesis
apply -
apply (rule corres_assume_pre)
apply (subgoal_tac "is_aligned ptr (4 + cbits) \<and> cbits \<le> word_bits - cte_level_bits")
prefer 2
apply (clarsimp simp: caps)
apply (erule valid_CNodeCapE)
apply fastforce
apply fastforce
apply fastforce
apply (thin_tac "?t \<in> state_relation")
apply (erule conjE)
apply (subst resolveAddressBits.simps)
apply (subst resolve_address_bits'.simps)
apply (simp add: caps isCap_defs Let_def)
apply (simp add: linorder_not_less drop_postfix_eq)
apply (erule exE)
apply (cases "guard \<le> cref")
prefer 2
apply (clarsimp simp: guard_mask_shift lookup_failure_map_def unlessE_whenE)
apply (clarsimp simp: guard_mask_shift unlessE_whenE)
apply (cases "length cref < cbits + length guard")
apply (clarsimp simp: lookup_failure_map_def)
apply (simp add: guard_mask_shift locateSlot_def returnOk_liftE [symmetric])
apply (cases "length cref = cbits + length guard")
apply clarsimp
apply (rule corres_noopE)
prefer 2
apply (rule no_fail_pre, wp)[1]
apply wp
apply (clarsimp simp: objBits_simps)
apply (erule (2) valid_CNodeCapE)
apply (erule (3) cte_map_shift')
apply simp
apply simp
apply (subgoal_tac "cbits + length guard < length cref")
prefer 2
apply simp
apply simp
apply (rule corres_initial_splitE)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule getSlotCap_corres)
apply (simp add: objBits_simps)
apply (erule (1) cte_map_shift)
apply simp
apply assumption
apply assumption
apply clarsimp
apply (clarsimp simp: valid_cap_def)
apply (erule cap_table_at_cte_at)
apply simp
apply clarsimp
apply (case_tac "is_cnode_cap rv")
prefer 2
apply (simp add: cnode_cap_case_if)
apply (rule corres_noopE)
prefer 2
apply (rule no_fail_pre, rule no_fail_returnOK)
apply (rule TrueI)
prefer 2
apply (simp add: unlessE_whenE cnode_cap_case_if)
apply (rule IH, (simp_all)[9])
apply clarsimp
apply (drule postfix_dropD)
apply clarsimp
apply (subgoal_tac "32 + (cbits + length guard) - length cref = (cbits + length guard) + (32 - length cref)")
prefer 2
apply (drule len_drop_lemma)
apply simp
apply arith
apply simp
apply (subst drop_drop [symmetric])
apply simp
apply wp
apply (clarsimp simp: objBits_simps)
apply (erule (1) cte_map_shift)
apply simp
apply assumption
apply assumption
apply wp
apply clarsimp
apply (rule hoare_chain)
apply (rule hoare_conj [OF get_cap_inv [of "valid_objs and pspace_aligned"] get_cap_valid])
apply clarsimp
apply clarsimp
apply clarsimp
apply wp
apply simp
apply simp
done
}
ultimately
show ?thesis by fast
next
case False
with "1.prems"
show ?thesis
by (cases cap)
(auto simp: resolve_address_bits'.simps resolveAddressBits.simps
isCap_defs lookup_failure_map_def)
qed
qed
lemma rab_corres:
"\<lbrakk> cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a;
bits = length (snd a) \<rbrakk> \<Longrightarrow>
corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
cte' = cte_map cte \<and> length bits = bits'))
(invs and valid_cap (fst a)) (invs' and valid_cap' c')
(resolve_address_bits a)
(resolveAddressBits c' cref' bits)"
using rab_corres' by (rule corres_guard_imp) auto
lemma getThreadCSpaceRoot:
"getThreadCSpaceRoot t = return t"
by (simp add: getThreadCSpaceRoot_def locateSlot_def
tcbCTableSlot_def)
lemma getThreadVSpaceRoot:
"getThreadVSpaceRoot t = return (t+16)"
by (simp add: getThreadVSpaceRoot_def locateSlot_def objBits_simps
tcbVTableSlot_def shiftl_t2n)
lemma getSlotCap_tcb_corres:
"corres (\<lambda>t c. cap_relation (tcb_ctable t) c)
(tcb_at t and valid_objs and pspace_aligned)
(pspace_distinct' and pspace_aligned')
(gets_the (get_tcb t))
(getSlotCap t)"
(is "corres ?r ?P ?Q ?f ?g")
using get_cap_corres [where cslot_ptr = "(t, tcb_cnode_index 0)"]
apply (simp add: getSlotCap_def liftM_def[symmetric])
apply (drule corres_guard_imp [where P="?P" and P'="?Q"])
apply (clarsimp simp: cte_at_cases tcb_at_def
dest!: get_tcb_SomeD)
apply simp
apply (subst(asm) corres_cong [OF refl refl gets_the_tcb_get_cap[symmetric] refl refl])
apply simp
apply (simp add: o_def cte_map_def tcb_cnode_index_def)
done
lemma lookup_slot_corres:
"corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref))
(valid_objs and pspace_aligned and tcb_at t)
(valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t)
(lookup_slot_for_thread t (to_bl cptr))
(lookupSlotForThread t cptr)"
apply (unfold lookup_slot_for_thread_def lookupSlotForThread_def)
apply (simp add: returnOk_bindE const_def)
apply (simp add: getThreadCSpaceRoot)
apply (fold returnOk_liftE)
apply (simp add: returnOk_bindE)
apply (rule corres_initial_splitE)
apply (subst corres_liftE_rel_sum)
apply (rule corres_guard_imp)
apply (rule getSlotCap_tcb_corres)
apply simp
apply simp
apply (subst bindE_returnOk[symmetric])
apply (rule corres_initial_splitE)
apply (rule rab_corres')
apply simp
apply (simp add: word_size)
apply simp
apply (clarsimp simp: word_size)
prefer 4
apply wp
apply clarsimp
apply (erule (1) objs_valid_tcb_ctable)
prefer 4
apply wp
apply clarsimp
apply simp
prefer 2
apply (rule hoare_vcg_precond_impE)
apply (rule resolve_address_bits_cte_at [unfolded validE_R_def])
apply clarsimp
prefer 2
apply (rule hoare_vcg_precond_impE)
apply (rule resolveAddressBits_cte_at')
apply (simp add: invs'_def valid_state'_def valid_pspace'_def)
apply (simp add: returnOk_def split_def)
done
lemmas rab_cte_at' [wp] = resolveAddressBits_cte_at' [folded validE_R_def]
lemma lookupSlot_cte_at_wp[wp]:
"\<lbrace>valid_objs'\<rbrace> lookupSlotForThread t addr \<lbrace>\<lambda>rv. cte_at' rv\<rbrace>, \<lbrace>\<lambda>r. \<top>\<rbrace>"
apply (simp add: lookupSlotForThread_def)
apply (simp add: getThreadCSpaceRoot_def locateSlot_def tcbCTableSlot_def)
apply (wp | simp add: split_def)+
done
lemma lookupSlot_inv[wp]:
"\<lbrace>P\<rbrace> lookupSlotForThread t addr \<lbrace>\<lambda>_. P\<rbrace>"
apply (simp add: lookupSlotForThread_def)
apply (simp add: getThreadCSpaceRoot_def locateSlot_def tcbCTableSlot_def)
apply (wp | simp add: split_def)+
done
lemma lc_corres:
"corres (lfr \<oplus> cap_relation)
(valid_objs and pspace_aligned and tcb_at t)
(valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t)
(lookup_cap t (to_bl ref)) (lookupCap t ref)"
apply (simp add: lookup_cap_def lookupCap_def bindE_assoc
lookupCapAndSlot_def liftME_def split_def)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF _ lookup_slot_corres])
apply (simp add: split_def getSlotCap_def liftM_def[symmetric] o_def)
apply (rule get_cap_corres)
apply (rule hoare_pre, wp lookup_slot_cte_at_wp|simp)+
done
lemma setObject_cte_obj_at_tcb':
assumes x: "\<And>tcb f. P (tcbCTable_update f tcb) = P tcb"
"\<And>tcb f. P (tcbVTable_update f tcb) = P tcb"
"\<And>tcb f. P (tcbReply_update f tcb) = P tcb"
"\<And>tcb f. P (tcbCaller_update f tcb) = P tcb"
"\<And>tcb f. P (tcbIPCBufferFrame_update f tcb) = P tcb"
shows
"\<lbrace>\<lambda>s. P' (obj_at' (P :: tcb \<Rightarrow> bool) p s)\<rbrace>
setObject c (cte::cte)
\<lbrace>\<lambda>_ s. P' (obj_at' P p s)\<rbrace>"
apply (clarsimp simp: setObject_def in_monad split_def
valid_def lookupAround2_char1
obj_at'_def ps_clear_upd' projectKOs
split del: split_if)
apply (clarsimp elim!: rsubst[where P=P'])
apply (clarsimp simp: updateObject_cte in_monad objBits_simps
tcbCTableSlot_def tcbVTableSlot_def x
typeError_def
split: split_if_asm
Structures_H.kernel_object.split_asm)
done
lemma setCTE_typ_at':
"\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setCTE c cte \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>"
by (clarsimp simp add: setCTE_def) (wp setObject_typ_at')
lemmas setObject_typ_at [wp] = setObject_typ_at' [where P=id, simplified]
lemma setCTE_typ_at [wp]:
"\<lbrace>typ_at' T p\<rbrace> setCTE c cte \<lbrace>\<lambda>_. typ_at' T p\<rbrace>"
by (clarsimp simp add: setCTE_def) wp
lemmas setCTE_typ_ats [wp] = typ_at_lifts [OF setCTE_typ_at']
lemma setCTE_st_tcb_at':
"\<lbrace>st_tcb_at' P t\<rbrace>
setCTE c cte
\<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>"
unfolding st_tcb_at'_def setCTE_def
apply (rule setObject_cte_obj_at_tcb')
apply simp+
done
lemma setObject_cte_ksCurDomain[wp]:
"\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject ptr (cte::cte) \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>"
apply (simp add: setObject_def split_def)
apply (wp updateObject_cte_inv | simp)+
done
lemma setCTE_tcb_in_cur_domain':
"\<lbrace>tcb_in_cur_domain' t\<rbrace>
setCTE c cte
\<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>"
unfolding tcb_in_cur_domain'_def setCTE_def
apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf)
apply (wp setObject_cte_obj_at_tcb' | simp)+
done
lemma tcbCTable_upd_simp [simp]:
"tcbCTable (tcbCTable_update (\<lambda>_. x) tcb) = x"
by (cases tcb) simp
lemma tcbVTable_upd_simp [simp]:
"tcbVTable (tcbVTable_update (\<lambda>_. x) tcb) = x"
by (cases tcb) simp
lemma setCTE_ctes_of_wp [wp]:
"\<lbrace>\<lambda>s. P (ctes_of s (p \<mapsto> cte))\<rbrace>
setCTE p cte
\<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>"
by (simp add: setCTE_def ctes_of_setObject_cte)
lemma setCTE_weak_cte_wp_at:
"\<lbrace>\<lambda>s. (if p = ptr then P (cteCap cte) else cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace>
setCTE ptr cte
\<lbrace>\<lambda>uu s. cte_wp_at'(\<lambda>c. P (cteCap c)) p s\<rbrace>"
apply (simp add: cte_wp_at_ctes_of)
apply wp
apply clarsimp
done
lemma updateMDB_weak_cte_wp_at:
"\<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
updateMDB m f
\<lbrace>\<lambda>uu. cte_wp_at'(\<lambda>c. P (cteCap c)) p\<rbrace>"
unfolding updateMDB_def
apply simp
apply safe
apply (wp setCTE_weak_cte_wp_at)
apply (rule hoare_post_imp [OF _ getCTE_sp])
apply (clarsimp simp: cte_wp_at'_def)
done
lemma cte_wp_at_extract':
"\<lbrakk> cte_wp_at' (\<lambda>c. c = x) p s; cte_wp_at' P p s \<rbrakk> \<Longrightarrow> P x"
by (clarsimp simp: cte_wp_at_ctes_of)
lemma cteCap_update_id [simp]:
"cteCap (cteCap_update (\<lambda>_. cap) c) = cap"
by (cases c) simp
lemmas setCTE_valid_objs = setCTE_valid_objs'
lemma updateMDB_objs [wp]:
"\<lbrace>valid_objs'\<rbrace>
updateMDB p f
\<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
apply (simp add: updateMDB_def)
apply clarsimp
apply (wp setCTE_valid_objs | simp)+
done
lemma capFreeIndex_update_valid_cap':
"\<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (of_nat fb :: word32) 4;
s \<turnstile>' capability.UntypedCap v bits fa\<rbrakk>
\<Longrightarrow> s \<turnstile>' capability.UntypedCap v bits fb"
apply (clarsimp simp:valid_cap'_def capAligned_def valid_untyped'_def ko_wp_at'_def)
apply (intro conjI impI allI)
apply (elim allE)
apply (erule(1) impE)+
apply (erule disjE)
apply simp_all
apply (rule disjI1)
apply clarsimp
apply (erule disjoint_subset2[rotated])
apply (clarsimp)
apply (rule word_plus_mono_right)
apply (rule of_nat_mono_maybe_le[THEN iffD1])
apply (subst word_bits_def[symmetric])
apply (erule less_le_trans[OF _ power_increasing])
apply simp
apply simp
apply (subst word_bits_def[symmetric])
apply (erule le_less_trans)
apply (erule less_le_trans[OF _ power_increasing])
apply simp+
apply (erule is_aligned_no_wrap')
apply (rule word_of_nat_less)
apply simp
apply (erule allE)+
apply (erule(1) impE)+
apply simp
done
lemma maxFreeIndex_update_valid_cap'[simp]:
"s \<turnstile>' capability.UntypedCap v0a v1a fa \<Longrightarrow>
s \<turnstile>' capability.UntypedCap v0a v1a (maxFreeIndex v1a)"
apply (rule capFreeIndex_update_valid_cap'[rotated -1])
apply assumption
apply (clarsimp simp:valid_cap'_def capAligned_def
valid_untyped'_def ko_wp_at'_def maxFreeIndex_def shiftL_nat)+
apply (erule is_aligned_weaken[OF is_aligned_triv])
done
lemma cap_insert_objs' [wp]:
"\<lbrace>valid_objs'
and valid_cap' cap\<rbrace>
cteInsert cap src dest \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: split_if)
apply (wp setCTE_valid_objs)
apply simp
apply wp
apply (clarsimp simp: updateCap_def)
apply (wp|simp)+
apply (rule hoare_drop_imp)+
apply wp
apply (rule hoare_strengthen_post[OF getCTE_sp])
apply (clarsimp simp:isCap_simps)
done
lemma cteInsert_weak_cte_wp_at:
"\<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and>
cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>
cteInsert cap src dest
\<lbrace>\<lambda>uu. cte_wp_at'(\<lambda>c. P (cteCap c)) p\<rbrace>"
unfolding cteInsert_def error_def updateCap_def setUntypedCapAsFull_def
apply (simp add: bind_assoc split del: split_if)
apply (wp setCTE_weak_cte_wp_at updateMDB_weak_cte_wp_at static_imp_wp | simp)+
apply (wp getCTE_ctes_wp)
apply (clarsimp simp: isCap_simps split:split_if_asm| rule conjI)+
done
lemma setCTE_valid_cap:
"\<lbrace>valid_cap' c\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r. valid_cap' c\<rbrace>"
by (rule typ_at_lifts, rule setCTE_typ_at')
lemma setCTE_weak_cte_at:
"\<lbrace>\<lambda>s. cte_at' p s\<rbrace>
setCTE ptr cte
\<lbrace>\<lambda>uu. cte_at' p\<rbrace>"
by (rule typ_at_lifts, rule setCTE_typ_at')
lemma updateMDB_valid_cap:
"\<lbrace>valid_cap' c\<rbrace> updateMDB ptr f \<lbrace>\<lambda>_. valid_cap' c\<rbrace>"
unfolding updateMDB_def
apply simp
apply rule
apply (wp setCTE_valid_cap)
done
lemma set_is_modify:
"m p = Some cte \<Longrightarrow>
m (p \<mapsto> cteMDBNode_update (\<lambda>_. (f (cteMDBNode cte))) cte) =
m (p \<mapsto> cteMDBNode_update f cte)"
apply (case_tac cte)
apply (rule ext)
apply clarsimp
done
lemma updateMDB_ctes_of_wp:
"\<lbrace>\<lambda>s. (p \<noteq> 0 \<longrightarrow> P (modify_map (ctes_of s) p (cteMDBNode_update f))) \<and>
(p = 0 \<longrightarrow> P (ctes_of s))\<rbrace>
updateMDB p f
\<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>"
apply (simp add: updateMDB_def)
apply safe
apply wp
apply (rule hoare_pre)
apply (wp getCTE_wp)
apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply)
apply (simp add: modify_map_def set_is_modify)
done
lemma updateMDB_ctes_of_no_0 [wp]: