-
Notifications
You must be signed in to change notification settings - Fork 105
/
Retype_AC.thy
1208 lines (1085 loc) · 55.1 KB
/
Retype_AC.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 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory Retype_AC
imports ArchCNode_AC
begin
subsection\<open>invoke\<close>
(* put in here that we own the region mentioned in the invocation *)
definition authorised_untyped_inv :: "'a PAS \<Rightarrow> Invocations_A.untyped_invocation \<Rightarrow> bool" where
"authorised_untyped_inv aag ui \<equiv> case ui of
Retype src_slot reset base afr new_type obj_sz slots dev \<Rightarrow>
is_subject aag (fst src_slot)
\<and> (0 :: obj_ref) < of_nat (length slots)
\<and> (\<forall>x\<in>set (retype_addrs afr new_type (length slots) obj_sz). is_subject aag x)
\<and> (\<forall>x\<in>{afr..afr + of_nat (length slots)*2^(obj_bits_api new_type obj_sz) - 1}. is_subject aag x)
\<and> new_type \<noteq> ArchObject ASIDPoolObj
\<and> (\<forall>x\<in>set slots. is_subject aag (fst x))"
lemma ptr_range_memI:
"is_aligned p n \<Longrightarrow> p \<in> ptr_range p n"
unfolding ptr_range_def
apply (erule is_aligned_get_word_bits)
apply (drule (1) base_member_set)
apply (simp add: field_simps)
apply simp
done
lemma ptr_range_add_memI:
"\<lbrakk> is_aligned (p :: 'a :: len word) n; k < 2 ^ n \<rbrakk> \<Longrightarrow> (p + k) \<in> ptr_range p n"
unfolding ptr_range_def
apply (erule is_aligned_get_word_bits)
apply clarsimp
apply (rule conjI)
apply (erule (1) is_aligned_no_wrap')
apply (subst p_assoc_help, rule word_plus_mono_right)
apply simp
apply (erule is_aligned_no_overflow')
apply (subgoal_tac "2 ^ n = (0 :: 'a word)")
apply simp
apply (simp add: word_bits_conv)
done
lemma create_cap_integrity:
"\<lbrace>integrity aag X st and K (is_subject aag (fst (fst ref)))\<rbrace>
create_cap typ sz untyped_ptr is_device ref
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: create_cap_def split_def)
apply (wp set_cap_integrity_autarch[unfolded pred_conj_def K_def]
create_cap_extended.list_integ_lift
create_cap_list_integrity
set_original_integrity_autarch
| simp add: set_cdt_def)+
by (auto simp: integrity_def)
lemma mol_respects:
"machine_op_lift mop \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>"
unfolding machine_op_lift_def
apply (simp add: machine_rest_lift_def split_def)
apply wp
apply (clarsimp simp: integrity_def)
done
lemma dmo_mol_respects[wp]:
"do_machine_op (machine_op_lift mop) \<lbrace>integrity aag X st\<rbrace>"
unfolding do_machine_op_def
apply wpsimp
apply (erule use_valid)
apply (wp mol_respects)
apply simp
done
lemma dmo_bind_valid:
"\<lbrace>P\<rbrace> do_machine_op (a >>= b) \<lbrace>Q\<rbrace> =
\<lbrace>P\<rbrace> do_machine_op a >>= (\<lambda>rv. do_machine_op (b rv)) \<lbrace>Q\<rbrace>"
by (fastforce simp: do_machine_op_def gets_def get_def select_f_def
modify_def put_def return_def bind_def valid_def)
lemma dmo_bind_valid':
"\<lbrace>P\<rbrace> a >>= (\<lambda>rv. do_machine_op (b rv >>= c rv)) \<lbrace>Q\<rbrace> =
\<lbrace>P\<rbrace> a >>= (\<lambda>rv. do_machine_op (b rv) >>= (\<lambda>rv'. do_machine_op (c rv rv'))) \<lbrace>Q\<rbrace>"
by (fastforce simp: do_machine_op_def gets_def get_def select_f_def
modify_def put_def return_def bind_def valid_def)
lemma dmo_mapM_wp:
assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (f x) \<lbrace>\<lambda>rv. P\<rbrace>"
shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>rv. P\<rbrace>"
apply (induct xs)
apply (simp add: mapM_def sequence_def)
apply (simp add: mapM_Cons dmo_bind_valid dmo_bind_valid')
apply (wpsimp | rule x)+
done
lemma dmo_mapM_x_wp:
assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (f x) \<lbrace>\<lambda>rv. P\<rbrace>"
shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM_x f xs) \<lbrace>\<lambda>rv. P\<rbrace>"
apply (subst mapM_x_mapM)
apply (simp add: do_machine_op_return_foo)
apply wp
apply (rule dmo_mapM_wp)
apply (rule x)
apply assumption+
done
lemmas dmo_mapM_x_wp_inv = dmo_mapM_x_wp[where S=UNIV, simplified]
lemma foldr_upd_app_if':
"foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then (f x) else g x)"
apply (induct as)
apply simp
apply simp
apply (rule ext)
apply simp
done
lemma retype_region_ret_is_subject:
"\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects \<and>
(\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x))\<rbrace>
retype_region ptr num_objects us tp dev
\<lbrace>\<lambda>rv. K (\<forall>ref \<in> set rv. is_subject aag ref)\<rbrace>"
apply (rule hoare_gen_asm2 | rule hoare_gen_asm)+
apply (rule hoare_strengthen_post)
apply (rule retype_region_ret)
apply (simp only: K_def)
apply (rule ballI)
apply (elim conjE)
apply (erule bspec)
apply (rule rev_subsetD, assumption)
apply (simp add: p_assoc_help del: set_map)
apply (rule retype_addrs_subset_ptr_bits[simplified retype_addrs_def])
apply simp
done
declare wrap_ext_det_ext_ext_def[simp]
lemma thread_st_auth_detype[simp]:
"thread_st_auth (detype S s) = (\<lambda>x. if x \<in> S then {} else thread_st_auth s x)"
by (rule ext, simp add: thread_st_auth_def get_tcb_def detype_def tcb_states_of_state_def)
lemma thread_bound_ntfns_detype[simp]:
"thread_bound_ntfns (detype S s) = (\<lambda>x. if x \<in> S then None else thread_bound_ntfns s x)"
by (rule ext, simp add: thread_bound_ntfns_def get_tcb_def detype_def tcb_states_of_state_def)
lemma sita_detype:
"state_irqs_to_policy aag (detype R s) \<subseteq> state_irqs_to_policy aag s"
apply (clarsimp)
apply (erule state_irqs_to_policy_aux.induct)
apply (auto simp: detype_def intro: state_irqs_to_policy_aux.intros split: if_split_asm)
done
(* FIXME: move *)
lemmas pas_refined_by_subsets = pas_refined_state_objs_to_policy_subset
lemma dtsa_detype: "domains_of_state (detype R s) \<subseteq> domains_of_state s"
by (auto simp: detype_def detype_ext_def
intro: domtcbs
elim!: domains_of_state_aux.cases
split: if_splits)
locale retype_region_proofs' = retype_region_proofs +
constrains s :: "det_ext state"
and s' :: "det_ext state"
locale Retype_AC_1 =
fixes aag :: "'a PAS"
assumes state_vrefs_detype[simp]:
"x \<in> state_vrefs (detype R s) p \<Longrightarrow> x \<in> state_vrefs s p"
and sata_detype:
"state_asids_to_policy aag (detype R s) \<subseteq> state_asids_to_policy aag s"
and word_size_bits_untyped_min_bits:
"word_size_bits \<le> untyped_min_bits"
and word_size_bits_resetChunkBits:
"word_size_bits \<le> resetChunkBits"
and clas_default_cap:
"\<And>tp. tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_asid_slot aag l (default_cap tp p sz dev)"
and cli_default_cap:
"\<And>tp. tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_irq aag l (default_cap tp p sz dev)"
and aobj_refs'_default':
"\<And>tp. is_aligned p (obj_bits_api (ArchObject tp) n)
\<Longrightarrow> aobj_ref' (arch_default_cap tp p n dev) \<subseteq> ptr_range p (obj_bits_api (ArchObject tp) n)"
and init_arch_objects_pas_refined:
"\<And>tp. \<lbrace>pas_refined aag and post_retype_invs tp refs
and (\<lambda>s. \<forall>x\<in>set refs. x \<notin> global_refs s)
and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api tp obj_sz))\<rbrace>
init_arch_objects tp ptr bits obj_sz refs
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
and dmo_freeMemory_invs:
"do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>s :: det_ext state. invs s\<rbrace>"
and init_arch_objects_pas_cur_domain[wp]:
"\<And>tp. init_arch_objects tp ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
and retype_region_pas_cur_domain[wp]:
"\<And>tp. retype_region ptr n us tp dev \<lbrace>pas_cur_domain aag\<rbrace>"
and reset_untyped_cap_pas_cur_domain[wp]:
"reset_untyped_cap src_slot \<lbrace>pas_cur_domain aag\<rbrace>"
and arch_data_to_obj_type_not_ASIDPoolObj[simp]:
"arch_data_to_obj_type v \<noteq> Some ASIDPoolObj"
and data_to_nat_of_nat[simp]:
"\<And>x. of_nat (data_to_nat x) = x"
and nonzero_data_to_nat_simp:
"\<And>x. 0 < data_to_nat x \<Longrightarrow> 0 < x"
and retype_region_proofs'_pas_refined:
"\<lbrakk> retype_region_proofs' s ty us ptr sz n dev; invs s; pas_refined aag s \<rbrakk>
\<Longrightarrow> pas_refined aag (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us)
then Some (default_object ty dev us)
else kheap s x\<rparr>)"
and dmo_freeMemory_respects:
"\<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits
\<and> (\<forall>p \<in> ptr_range ptr bits. is_subject aag p))\<rbrace>
do_machine_op (freeMemory ptr bits)
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
and dmo_clearMemory_respects':
"\<lbrace>integrity aag X st and
K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and>
(\<forall>p \<in> ptr_range ptr bits. aag_has_auth_to aag Write p))\<rbrace>
do_machine_op (clearMemory ptr (2 ^ bits))
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
and init_arch_objects_integrity:
"\<lbrace>integrity aag X st and K (\<forall>x\<in>set refs. is_subject aag x)
and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
init_arch_objects new_type ptr num_objects obj_sz refs
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
and integrity_asids_detype:
"\<forall>r \<in> R. pasObjectAbs aag r \<in> subjects
\<Longrightarrow> integrity_asids aag subjects p a (detype R s) st = integrity_asids aag subjects p a s st"
"\<forall>r \<in> R. pasObjectAbs aag r \<in> subjects
\<Longrightarrow> integrity_asids aag subjects p a s (detype R st) = integrity_asids aag subjects p a s st"
and retype_region_integrity_asids:
"\<lbrakk> range_cover ptr sz (obj_bits_api typ o_bits) n; typ \<noteq> Untyped;
\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; integrity_asids aag {pasSubject aag} p a s st \<rbrakk>
\<Longrightarrow> integrity_asids aag {pasSubject aag} p a s
(st\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api typ o_bits)) ` {0 ..< n}
then Some (default_object typ dev o_bits)
else kheap s a\<rparr>)"
begin
lemma detype_integrity:
"\<lbrakk> integrity aag X st s; \<forall>r\<in>refs. is_subject aag r \<rbrakk>
\<Longrightarrow> integrity aag X st (detype refs s)"
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def integrity_asids_detype)
apply (clarsimp simp: detype_def detype_ext_def integrity_def)
done
lemma sta_detype:
"state_objs_to_policy (detype R s) \<subseteq> state_objs_to_policy s"
apply (clarsimp simp add: state_objs_to_policy_def state_refs_of_detype)
apply (erule state_bits_to_policy.induct)
apply (auto intro: state_bits_to_policy.intros dest: state_vrefs_detype
simp: state_objs_to_policy_def split: if_splits)
done
lemma pas_refined_detype:
"pas_refined aag s \<Longrightarrow> pas_refined aag (detype R s)"
apply (rule pas_refined_by_subsets)
apply (blast intro!: sta_detype sata_detype sita_detype interrupt_irq_node_detype dtsa_detype)+
done
lemma delete_objects_respects[wp]:
"\<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and>
word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace>
delete_objects ptr bits
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: delete_objects_def)
apply (rule_tac bind_wp_fwd)
apply (rule hoare_triv[of P _ "%_. P" for P])
apply (wp dmo_freeMemory_respects | simp)+
by (fastforce simp: ptr_range_def intro!: detype_integrity)
lemma integrity_work_units_completed_update[simp]:
"integrity aag X st (work_units_completed_update f s) = integrity aag X st s"
by (simp add: integrity_def)
lemma integrity_irq_state_independent[intro!, simp]:
"integrity x y z (s\<lparr>machine_state :=
machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) =
integrity x y z s"
by (simp add: integrity_def)
lemma reset_untyped_cap_integrity:
"\<lbrace>integrity aag X st and pas_refined aag and valid_objs
and cte_wp_at is_untyped_cap slot
and K (is_subject aag (fst slot))\<rbrace>
reset_untyped_cap slot
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: reset_untyped_cap_def)
apply (rule hoare_pre)
apply (wp set_cap_integrity_autarch dmo_clearMemory_respects'
| simp add: unless_def)+
apply (rule valid_validE)
apply (rule_tac P="cap_aligned cap \<and> is_untyped_cap cap \<and>
(\<forall>r \<in> cap_range cap. aag_has_auth_to aag Write r)" in hoare_gen_asm)
apply (rule validE_valid, rule mapME_x_wp')
apply (rule hoare_pre)
apply (wp mapME_x_inv_wp[OF hoare_pre(2)] preemption_point_inv'
set_cap_integrity_autarch dmo_clearMemory_respects' | simp)+
apply (clarsimp simp: cap_aligned_def is_cap_simps bits_of_def)
apply (subst aligned_add_aligned, assumption, rule is_aligned_shiftl, simp+)
apply (simp add: word_size_bits_resetChunkBits)
apply (clarsimp simp: arg_cong2[where f="(\<le>)", OF refl Kernel_Config.resetChunkBits_def [unfolded atomize_eq]])
apply (drule bspec, erule subsetD[rotated])
apply (simp only: ptr_range_def, rule new_range_subset'; simp add: is_aligned_shiftl)
apply (rule shiftl_less_t2n)
apply (rule word_of_nat_less)
apply simp
apply (simp add: word_bits_def)
apply clarsimp
apply (simp add: if_apply_def2)
apply (wp hoare_vcg_const_imp_lift get_cap_wp)+
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule caps_of_state_valid_cap, clarsimp+)
apply (clarsimp simp: cap_aligned_def is_cap_simps valid_cap_simps bits_of_def)
apply (frule(2) cap_cur_auth_caps_of_state)
apply (clarsimp simp: aag_cap_auth_def ptr_range_def aag_has_Control_iff_owns
pas_refined_refl le_trans[OF word_size_bits_untyped_min_bits])
done
lemma retype_region_integrity:
"\<lbrace>integrity aag X st and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and>
(\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x))\<rbrace>
retype_region ptr num_objects o_bits type dev
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)+
apply (simp only: retype_region_def retype_region_ext_extended.dxo_eq)
apply (simp only: retype_addrs_def retype_region_ext_def
foldr_upd_app_if' fun_app_def K_bind_def)
apply wp
apply (clarsimp simp: not_less)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def retype_region_integrity_asids)
apply (fastforce intro: tro_lrefl tre_lrefl
dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
simp: image_def p_assoc_help power_sub)
done
lemma invoke_untyped_integrity:
"\<lbrace>integrity aag X st and pas_refined aag and valid_objs
and valid_untyped_inv ui
and K (authorised_untyped_inv aag ui)\<rbrace>
invoke_untyped ui
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_name_pre_state)
apply (clarsimp simp only: valid_untyped_inv_wcap)
apply (cases ui)
apply (simp add: mapM_x_def[symmetric] authorised_untyped_inv_def
invoke_untyped_def)
apply (rule hoare_pre)
apply (wp mapM_x_wp[OF _ subset_refl] create_cap_integrity
init_arch_objects_integrity retype_region_integrity
retype_region_ret_is_subject
set_cap_integrity_autarch hoare_vcg_if_lift
whenE_wp reset_untyped_cap_integrity
| clarsimp simp: split_paired_Ball
| erule in_set_zipE
| blast)+
apply (clarsimp simp: ptr_range_def p_assoc_help bits_of_def
cte_wp_at_caps_of_state)
apply (frule(1) cap_cur_auth_caps_of_state, simp+)
apply (clarsimp simp: aag_cap_auth_def pas_refined_all_auth_is_owns)
apply (simp add: word_and_le2 field_simps
| erule ball_subset[where A="{a && c .. b}" for a b c]
| rule conjI impI)+
done
lemma obj_refs_default':
"is_aligned oref (obj_bits_api tp sz)
\<Longrightarrow> obj_refs_ac (default_cap tp oref sz dev) \<subseteq> ptr_range oref (obj_bits_api tp sz)"
by (cases tp; auto simp: ptr_range_memI obj_bits_api_def dest: rev_subsetD[OF _ aobj_refs'_default'])
lemma create_cap_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
K (tp \<noteq> ArchObject ASIDPoolObj \<and> is_subject aag (fst p) \<and> is_subject aag (fst (fst ref)) \<and>
(\<forall>x \<in> ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x) \<and>
is_aligned (snd ref) (obj_bits_api tp sz))\<rbrace>
create_cap tp sz p dev ref
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: create_cap_def split_def)
apply (wps | wp set_cdt_pas_refined set_cap_pas_refined set_original_wp | clarsimp)+
apply (rule conjI)
apply (cases "fst ref", clarsimp simp: pas_refined_refl)
apply (cases "tp = Untyped")
apply (simp add: cap_links_asid_slot_def pas_refined_refl cap_links_irq_def
aag_cap_auth_def ptr_range_def obj_bits_api_def)
apply (clarsimp simp: clas_default_cap pas_refined_refl cli_default_cap aag_cap_auth_def)
apply (drule obj_refs_default')
apply (case_tac tp, simp_all)
apply (auto intro: pas_refined_refl dest!: subsetD)
done
end
context retype_region_proofs begin
lemma ts_eq[simp]: "thread_st_auth s' = thread_st_auth s"
apply (rule ext)
apply (simp add: s'_def ps_def thread_st_auth_def get_tcb_def orthr tcb_states_of_state_def
split: option.split Structures_A.kernel_object.split)
apply (simp add: default_object_def default_tcb_def tyunt
split: Structures_A.apiobject_type.split)
done
lemma bas_eq[simp]: "thread_bound_ntfns s' = thread_bound_ntfns s"
apply (rule ext)
apply (simp add: s'_def ps_def thread_bound_ntfns_def get_tcb_def orthr tcb_states_of_state_def
split: option.split Structures_A.kernel_object.split)
apply (simp add: default_object_def default_tcb_def tyunt
split: Structures_A.apiobject_type.split)
done
end
context retype_region_proofs' begin
lemma domains_of_state: "domains_of_state s' \<subseteq> domains_of_state s"
unfolding s'_def by simp
(* FIXME MOVE next to cte_at_pres *)
lemma cte_wp_at_pres:
"cte_wp_at P p s \<Longrightarrow> cte_wp_at P p s'"
unfolding cte_wp_at_cases s'_def ps_def
apply (erule disjE)
apply (clarsimp simp: well_formed_cnode_n_def orthr)+
done
(* FIXME MOVE next to cte_at_pres *)
lemma caps_of_state_pres:
"caps_of_state s p = Some cap \<Longrightarrow> caps_of_state s' p = Some cap"
using cte_wp_at_pres by (simp add: F)
end
lemma retype_region_ext_kheap_update:
"\<lbrace>Q xs and R xs\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. Q xs\<rbrace>
\<Longrightarrow> \<lbrace>\<lambda>s. Q xs (kheap_update f s) \<and> R xs (kheap_update f s)\<rbrace>
retype_region_ext xs ty
\<lbrace>\<lambda>_ s. Q xs (kheap_update f s)\<rbrace>"
apply (clarsimp simp: valid_def retype_region_ext_def)
apply (erule_tac x="kheap_update f s" in allE)
apply (clarsimp simp: split_def bind_def gets_def get_def return_def modify_def put_def)
done
lemma use_retype_region_proofs_ext':
assumes x: "\<And>(s::det_ext state). \<lbrakk> retype_region_proofs s ty us ptr sz n dev; P s \<rbrakk>
\<Longrightarrow> Q (retype_addrs ptr ty n us)
(s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us)
then Some (default_object ty dev us )
else kheap s x\<rparr>)"
assumes y: "\<And>xs. \<lbrace>Q xs and R xs\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. Q xs\<rbrace>"
assumes z: "\<And>f xs s. R xs (kheap_update f s) = R xs s"
shows
"\<lbrakk> ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s \<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and>
caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and>
caps_no_overlap ptr sz s \<and> pspace_no_overlap_range_cover ptr sz s \<and>
(\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and>
P s \<and> R (retype_addrs ptr ty n us) s\<rbrace>
retype_region ptr n us ty dev \<lbrace>Q\<rbrace>"
apply (simp add: retype_region_def split del: if_split)
apply (rule hoare_pre, (wp | simp)+)
apply (rule retype_region_ext_kheap_update[OF y])
apply (wp | simp)+
apply (clarsimp simp: retype_addrs_fold
foldr_upd_app_if fun_upd_def[symmetric])
apply safe
apply (rule x)
apply (rule retype_region_proofs.intro, simp_all)[1]
apply (fastforce simp: range_cover_def obj_bits_api_def z slot_bits_def2 word_bits_def)+
done
lemmas use_retype_region_proofs_ext =
use_retype_region_proofs_ext'[where Q="\<lambda>_. Q" and P=Q, simplified] for Q
context is_extended begin
lemma pas_refined_tcb_domain_map_wellformed':
assumes tdmw: "\<lbrace>tcb_domain_map_wellformed aag and P\<rbrace> f \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace>"
shows "\<lbrace>pas_refined aag and P\<rbrace> f \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: pas_refined_def)
apply (wp tdmw)
apply (wp lift_inv)
apply simp+
done
end
lemma retype_region_ext_pas_refined:
"\<lbrace>pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in> set xs. is_subject aag x)\<rbrace>
retype_region_ext xs ty
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
including classic_wp_pre
apply (subst and_assoc[symmetric])
apply (wp retype_region_ext_extended.pas_refined_tcb_domain_map_wellformed')
apply (simp add: retype_region_ext_def, wp)
apply (clarsimp simp: tcb_domain_map_wellformed_aux_def)
apply (erule domains_of_state_aux.cases)
apply (clarsimp simp: foldr_upd_app_if' fun_upd_def[symmetric] split: if_split_asm)
apply (clarsimp simp: default_ext_def default_etcb_def split: apiobject_type.splits)
defer
apply (force intro: domtcbs)
done
context Retype_AC_1 begin
lemma retype_region_pas_refined:
"\<lbrace>pas_refined aag and invs and pas_cur_domain aag and
caps_overlap_reserved {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and
caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz and
(\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and
K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and
K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and
K ((type = CapTableObject \<longrightarrow> 0 < o_bits))\<rbrace>
retype_region ptr num_objects o_bits type dev
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_pre)
apply (rule use_retype_region_proofs_ext'[where P = "invs and pas_refined aag"])
apply clarsimp
apply (erule (2) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro])
apply (wp retype_region_ext_pas_refined)
apply simp
apply auto
done
end
lemma retype_region_ranges'':
"\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects \<and> num_objects \<noteq> 0)\<rbrace>
retype_region ptr num_objects us tp dev
\<lbrace>\<lambda>rv _. \<forall>y\<in>set rv. ptr_range y (obj_bits_api tp us) \<subseteq>
{ptr..ptr + of_nat num_objects * 2 ^ (obj_bits_api tp us) - 1}\<rbrace>"
apply simp
apply (rule hoare_gen_asm[where P'="\<top>", simplified])
apply (rule hoare_strengthen_post [OF retype_region_ret])
apply (clarsimp)
apply (frule_tac p=y in range_cover_subset)
apply assumption
apply simp
apply (rule conjI)
apply (fastforce simp: ptr_range_def ptr_add_def)
apply (clarsimp simp: ptr_range_def ptr_add_def intro: order_trans)
apply (erule order_trans)
apply (erule impE)
apply (simp add: p_assoc_help)
apply (rule is_aligned_no_wrap')
apply (rule is_aligned_add)
apply (fastforce simp: range_cover_def)
apply (simp add: is_aligned_mult_triv2)
apply (rule word_leq_le_minus_one, simp)
apply (rule power_not_zero)
apply (simp add: range_cover_def)
apply simp
done
lemma pspace_no_overlap_msu[simp]:
"pspace_no_overlap S (machine_state_update f s) = pspace_no_overlap S s"
by (clarsimp simp: pspace_no_overlap_def)
lemma descendants_range_in_msu[simp]:
"descendants_range_in S slot (machine_state_update f s) = descendants_range_in S slot s"
by (clarsimp simp: descendants_range_in_def)
lemma cte_wp_at_sym:
"cte_wp_at (\<lambda> c. c = cap) slot s = cte_wp_at ((=) cap) slot s"
by (simp add: cte_wp_at_def)
lemma untyped_slots_not_in_untyped_range:
"\<lbrakk> invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s;
is_untyped_cap cap; S = untyped_range cap; T \<subseteq> S\<rbrakk>
\<Longrightarrow> fst slot \<notin> T"
apply (erule contra_subsetD)
proof -
assume i: "invs s" and
dr: "descendants_range_in S slot s" and
ct: "cte_wp_at ((=) cap) slot s" and
ut: "is_untyped_cap cap" and
r: "S = untyped_range cap"
hence dt: "detype_locale cap slot s"
by (simp add: detype_locale_def descendants_range_def2 invs_untyped_children)
show "fst slot \<notin> S"
apply -
apply (insert r)
apply (simp, rule detype_locale.non_null_present[OF dt])
apply (insert ct ut)
apply (case_tac cap, simp_all)
apply (auto simp: cte_wp_at_def)
done
qed
lemma descendants_range_in_detype:
"\<lbrakk> invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s;
is_untyped_cap cap; S = untyped_range cap; T \<subseteq> S \<rbrakk>
\<Longrightarrow> descendants_range_in T slot (detype S s)"
apply (erule descendants_range_in_subseteq[rotated])
proof -
assume i: "invs s" and
dr: "descendants_range_in S slot s" and
ct: "cte_wp_at ((=) cap) slot s" and
ut: "is_untyped_cap cap" and
r: "S = untyped_range cap"
hence dt: "detype_locale cap slot s"
by (simp add: detype_locale_def descendants_range_def2 invs_untyped_children)
show "descendants_range_in S slot (detype S s)"
apply -
apply (insert i dr ct ut r)
apply (simp add: valid_mdb_descendants_range_in[OF invs_mdb])
apply (simp add: descendants_range_in_def)
apply (rule ballI)
apply (drule_tac x=p' in bspec, assumption)
apply (clarsimp simp: null_filter_def split: if_split_asm)
apply (rule conjI)
apply (simp add: cte_wp_at_caps_of_state)
apply (rule_tac t=a in ssubst[OF fst_conv[symmetric]])
apply (rule_tac ptr=slot and s=s in detype_locale.non_null_present)
apply (rule dt)
apply (simp add: cte_wp_at_caps_of_state)
apply fastforce
done
qed
lemma descendants_range_in_detype_ex:
"\<lbrakk> invs s; descendants_range_in S slot s; \<exists> cap. cte_wp_at ((=) cap) slot s \<and>
is_untyped_cap cap \<and> S = untyped_range cap; T \<subseteq> S \<rbrakk>
\<Longrightarrow> descendants_range_in T slot (detype S s)"
apply clarsimp
apply (blast intro: descendants_range_in_detype)
done
lemma descendants_range_in_detype_ex_strengthen:
"(invs s \<and> descendants_range_in S slot s \<and> T \<subseteq> S \<and>
(\<exists>cap. cte_wp_at ((=) cap) slot s \<and> is_untyped_cap cap \<and> S = untyped_range cap))
\<longrightarrow> descendants_range_in T slot (detype S s)"
by (blast intro: descendants_range_in_detype_ex)
lemma untyped_cap_aligned:
"\<lbrakk> cte_wp_at ((=) (UntypedCap dev word sz idx)) slot s; valid_objs s \<rbrakk>
\<Longrightarrow> is_aligned word sz"
by (fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def)
lemma range_cover_subset'':
"\<lbrakk> range_cover ptr sz sbit n; n \<noteq> 0 \<rbrakk>
\<Longrightarrow> {ptr ..ptr + of_nat n * 2 ^ sbit - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2^ sz - 1}"
apply (rule order_trans, erule(1) range_cover_subset')
apply (simp add: word_and_le2)
done
context Retype_AC_1 begin
lemma delete_objects_descendants_range_in':
"\<lbrace>invs and (\<lambda>s :: det_ext state. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s)
and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>
delete_objects word2 sz
\<lbrace>\<lambda>_. descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>"
unfolding delete_objects_def
apply (wp modify_wp dmo_freeMemory_invs | strengthen descendants_range_in_detype_ex_strengthen)+
apply (wp descendants_range_in_lift hoare_vcg_ex_lift | elim conjE | simp)+
apply fastforce
done
lemma delete_objects_descendants_range_in'':
"\<lbrace>invs and (\<lambda> s :: det_ext state. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s)
and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>
delete_objects word2 sz
\<lbrace>\<lambda>_. descendants_range_in {word2..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace>"
apply (clarsimp simp: valid_def)
apply (frule untyped_cap_aligned, fastforce)
apply (clarsimp)
apply (erule use_valid)
apply (wp delete_objects_descendants_range_in' | clarsimp | blast)+
done
lemma delete_objects_descendants_range_in''':
"\<lbrace>invs and (\<lambda>s :: det_ext state. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s)
and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>
delete_objects word2 sz
\<lbrace>\<lambda>_. descendants_range_in {word2 && ~~ mask sz..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace>"
apply (clarsimp simp: valid_def)
apply (frule untyped_cap_aligned, fastforce)
apply (clarsimp)
apply (erule use_valid)
apply (wp delete_objects_descendants_range_in' | clarsimp | blast)+
done
lemma delete_objects_descendants_range_in'''':
"\<lbrace>invs and (\<lambda> s :: det_ext state. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and
ct_active and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot and
K (range_cover word2 sz bits n \<and> n \<noteq> 0)\<rbrace>
delete_objects word2 sz
\<lbrace>\<lambda>_. descendants_range_in {word2..word2 + of_nat n * 2 ^ bits - 1} slot\<rbrace>"
apply (clarsimp simp: valid_def)
apply (rule descendants_range_in_subseteq)
apply (erule use_valid)
apply (wp delete_objects_descendants_range_in' | clarsimp | blast)+
apply (drule range_cover_subset'', simp)
apply (fastforce dest: untyped_cap_aligned)
done
lemmas delete_objects_descendants_range_in =
delete_objects_descendants_range_in'
delete_objects_descendants_range_in''
delete_objects_descendants_range_in'''
delete_objects_descendants_range_in''''
end
crunch delete_objects
for arch_state[wp]: "\<lambda>s. P (arch_state s)"
(ignore: do_machine_op freeMemory)
lemma bits_of_UntypedCap:
"bits_of (UntypedCap dev ptr sz free) = sz"
by (simp add: bits_of_def split: cap.splits)
(* clagged from Untyped_R.invoke_untyped_proofs.usable_range_disjoint *)
lemma usable_range_disjoint:
assumes cte_wp_at: "cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s"
assumes misc: "distinct slots" "idx \<le> unat (ptr && mask sz) \<or> ptr = ptr && ~~ mask sz"
"invs s" "slots \<noteq> []" "ct_active s"
"\<forall>slot\<in>set slots. cte_wp_at ((=) NullCap) slot s"
"\<forall>x\<in>set slots. ex_cte_cap_wp_to (\<lambda>_. True) x s"
assumes cover: "range_cover ptr sz (obj_bits_api tp us) (length slots)"
notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff
atLeastatMost_subset_iff atLeastLessThan_iff
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
shows
"usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz
(unat ((ptr && mask sz) +
of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter>
{ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}"
proof -
have not_0_ptr[simp]: "ptr\<noteq> 0"
using misc cte_wp_at
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (drule(1) caps_of_state_valid)
apply (clarsimp simp:valid_cap_def)
done
have idx_compare''[simp]:
"unat ((ptr && mask sz) + (of_nat (length slots) * 2 ^ obj_bits_api tp us)) < 2 ^ sz
\<Longrightarrow> ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1
< ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us"
apply (rule word_leq_le_minus_one,simp)
apply (rule neq_0_no_wrap)
apply (rule machine_word_plus_mono_right_split)
apply (simp add: shiftl_t2n range_cover_unat[OF cover] field_simps)
apply (simp only: word_bits_def range_cover.sz(1)[OF cover])
apply simp
done
show ?thesis
apply (clarsimp simp:mask_out_sub_mask blah)
apply (drule idx_compare'')
apply (simp add:not_le[symmetric])
done
qed
lemma set_free_index_invs':
"\<lbrace>(\<lambda>s. invs s \<and> cte_wp_at ((=) cap) slot s \<and>
(free_index_of cap \<le> idx' \<or>
(descendants_range_in {word1..word1 + 2 ^ (bits_of cap) - 1} slot s \<and>
pspace_no_overlap_range_cover word1 (bits_of cap) s)) \<and>
idx' \<le> 2 ^ cap_bits cap \<and> is_untyped_cap cap) and
K (word1 = obj_ref_of cap \<and> dev = (cap_is_device cap))\<rbrace>
set_cap (UntypedCap dev word1 (bits_of cap) idx') slot
\<lbrace>\<lambda>_. invs \<rbrace>"
apply (rule hoare_gen_asm)
apply (case_tac cap, simp_all add: bits_of_def)
apply (case_tac "free_index_of cap \<le> idx'")
apply simp
apply (cut_tac cap=cap and cref=slot and idx="idx'" in set_free_index_invs)
apply (simp add: free_index_of_def)
apply (rule hoare_weaken_pre, assumption, fastforce elim: cte_wp_at_weakenE)
apply simp
apply (wp set_untyped_cap_invs_simple | simp)+
apply (fastforce simp: cte_wp_at_def)
done
lemma delete_objects_pspace_no_overlap:
"\<lbrace>pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace>
delete_objects ptr sz
\<lbrace>\<lambda>_. pspace_no_overlap_range_cover ptr sz\<rbrace>"
unfolding delete_objects_def do_machine_op_def
apply (wp | simp add: split_def detype_machine_state_update_comm)+
apply clarsimp
apply (rule pspace_no_overlap_detype)
apply (auto dest: cte_wp_at_valid_objs_valid_cap)
done
lemma delete_objects_pspace_no_overlap':
"\<lbrace>pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace>
delete_objects ptr sz
\<lbrace>\<lambda>_. pspace_no_overlap_range_cover (ptr && ~~ mask sz) sz\<rbrace>"
apply (clarsimp simp: valid_def)
apply (frule untyped_cap_aligned, simp)
apply (clarsimp)
apply (frule(1) cte_wp_at_valid_objs_valid_cap)
apply (erule use_valid, wp delete_objects_pspace_no_overlap, auto)
done
(* FIXME: move *)
lemma valid_cap_range_untyped:
"\<lbrakk> valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s \<rbrakk>
\<Longrightarrow> cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s"
apply (rule cte_wp_at_weakenE)
apply simp
apply (clarsimp simp: word_and_le2 p_assoc_help)
done
fun slot_of_untyped_inv where "slot_of_untyped_inv (Retype slot _ _ _ _ _ _ _) = slot"
lemma aag_cap_auth_UntypedCap_idx_dev:
"aag_cap_auth aag l (UntypedCap dev base sz idx)
\<Longrightarrow> aag_cap_auth aag l (UntypedCap dev' base sz idx')"
by (clarsimp simp: aag_cap_auth_def cap_links_asid_slot_def
cap_links_irq_def)
lemma cte_wp_at_pas_cap_cur_auth_UntypedCap_idx_dev:
"\<lbrakk> cte_wp_at ((=) (UntypedCap dev base sz idx)) slot s;
is_subject aag (fst slot); pas_refined aag s\<rbrakk>
\<Longrightarrow> pas_cap_cur_auth aag (UntypedCap dev' base sz idx')"
apply (rule aag_cap_auth_UntypedCap_idx_dev)
apply (auto intro: cap_cur_auth_caps_of_state simp: cte_wp_at_caps_of_state)
done
lemmas caps_pas_cap_cur_auth_UntypedCap_idx_dev =
cte_wp_at_pas_cap_cur_auth_UntypedCap_idx_dev[OF caps_of_state_cteD]
lemma retype_addrs_aligned_range_cover:
assumes xin: "x \<in> set (retype_addrs ptr ty n us)"
and co: "range_cover ptr sz (obj_bits_api ty us) n"
shows "is_aligned x (obj_bits_api ty us)"
using co
apply (clarsimp simp: range_cover_def)
apply (rule retype_addrs_aligned[OF xin, where sz=sz], simp_all)
apply (simp add: word_bits_def)
done
lemma pas_refined_work_units_complete[simp]:
"pas_refined aag (work_units_completed_update f s) = pas_refined aag s"
by (simp add: pas_refined_def)
(*FIXME MOVE *)
lemma set_cap_sets_direct:
"P cap \<Longrightarrow> \<lbrace>\<top>\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>"
apply (rule hoare_strengthen_post)
apply (rule set_cap_sets)
apply (erule cte_wp_at_lift)
by blast
(*FIXME MOVE *)
lemma set_cap_sets_wp:
"\<lbrace>\<lambda>_. P cap\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>"
by (rule hoare_gen_asm2[simplified]) (erule set_cap_sets_direct)
lemma retype_region_post_retype_invs_spec:
"\<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz
and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}
and region_in_kernel_window {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}
and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s)
and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us)
and K (range_cover ptr sz (obj_bits_api ty us) n) \<rbrace>
retype_region ptr n us ty dev
\<lbrace>\<lambda>rv. post_retype_invs ty rv\<rbrace>"
apply (rule hoare_pre)
apply (wp retype_region_post_retype_invs)
apply (clarsimp simp del: split_paired_Ex)
apply (frule valid_cap_range_untyped[OF invs_valid_objs],simp)
apply fastforce
done
context Retype_AC_1 begin
lemma retype_region_pas_refined':
"\<lbrace>pas_refined aag and pas_cur_domain aag and invs and
caps_overlap_reserved {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and
(\<lambda>s. \<exists>idx. cte_wp_at (\<lambda> c. c = (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s \<and>
(idx \<le> unat (ptr && mask sz) \<or>
(descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s) \<and>
pspace_no_overlap_range_cover ptr sz s)) and
K (sz < word_bits) and
K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and
K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and
K ((type = CapTableObject \<longrightarrow> 0 < o_bits))\<rbrace>
retype_region ptr num_objects o_bits type dev
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)+
apply (rule hoare_weaken_pre)
apply (rule use_retype_region_proofs_ext'[where P="invs and pas_refined aag"])
apply clarsimp
apply (erule (2) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro])
apply (wp retype_region_ext_pas_refined)
apply simp
apply fastforce
apply fastforce
apply clarsimp
apply clarsimp
apply (frule valid_cap_range_untyped[OF invs_valid_objs])
apply (fastforce simp: cte_wp_at_caps_of_state)
apply (cases slot)
apply (auto intro: cte_wp_at_caps_no_overlapI descendants_range_caps_no_overlapI
cte_wp_at_pspace_no_overlapI
simp: cte_wp_at_sym)
done
lemma delete_objects_pas_refined:
"delete_objects ptr sz \<lbrace>pas_refined aag\<rbrace>"
apply (simp add: delete_objects_def do_machine_op_def)
apply (wp modify_wp | simp add: split_def)+
apply clarsimp
apply (rule pas_refined_detype)
apply simp
done
lemma delete_objects_pspace_aligned[wp]:
"delete_objects ptr sz \<lbrace>pspace_aligned\<rbrace>"
unfolding delete_objects_def do_machine_op_def
apply (wp | simp add: split_def detype_machine_state_update_comm)+
apply clarsimp
apply (auto simp add: detype_def pspace_aligned_def)
done
lemma reset_untyped_cap_pspace_aligned[wp]:
"reset_untyped_cap slot \<lbrace>pspace_aligned\<rbrace>"
apply (clarsimp simp: reset_untyped_cap_def)
apply (wpsimp wp: mapME_x_inv_wp )
apply (rule valid_validE)
apply (wpsimp wp: preemption_point_inv dxo_wp_weak hoare_drop_imps)+
done
lemma valid_vspace_objs_detype:
assumes "invs s"
assumes "cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s"
shows "valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s)"
proof -
obtain c where c_def: "cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}"
using assms by (fastforce dest: cte_wp_at_norm)
have detype: "detype_locale_arch c ptr s"
by unfold_locales (auto simp: assms c_def invs_untyped_children)
thus ?thesis
using detype_locale_arch.valid_vspace_obj_detype by (fastforce simp: c_def)
qed
lemma delete_objects_valid_vspace_objs:
"\<lbrace>\<lambda>s. invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and>
untyped_range c = {p..p + 2 ^ sz - 1}) ptr s)\<rbrace>
delete_objects p sz
\<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding delete_objects_def do_machine_op_def
apply (wp | simp add: split_def detype_machine_state_update_comm)+
apply (auto simp: valid_vspace_objs_detype)
done
lemma reset_untyped_cap_valid_vspace_objs:
"\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s\<rbrace>
reset_untyped_cap src_slot
\<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding reset_untyped_cap_def
apply (wpsimp wp: mapME_x_inv_wp preemption_point_inv)
apply (wp hoare_weak_lift_imp delete_objects_valid_vspace_objs)
apply (wpsimp wp: get_cap_wp)+
apply (cases src_slot)
apply (auto simp: cte_wp_at_caps_of_state)
apply (fastforce simp: bits_of_def is_cap_simps)+
done
lemma valid_arch_state_detype:
assumes "invs s"
assumes "cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s"
shows "valid_arch_state (detype {p..p + 2 ^ sz - 1} s)"
proof -
obtain c where c_def: "cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}"
using assms by (fastforce dest: cte_wp_at_norm)
have detype: "detype_locale_arch c ptr s"
by unfold_locales (auto simp: assms c_def invs_untyped_children)
thus ?thesis
using detype_locale_arch.valid_arch_state_detype by (fastforce simp: c_def)
qed
lemma delete_objects_valid_arch_state:
"\<lbrace>\<lambda>s. invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and>
untyped_range c = {p..p + 2 ^ sz - 1}) ptr s)\<rbrace>
delete_objects p sz
\<lbrace>\<lambda>_. valid_arch_state\<rbrace>"