-
Notifications
You must be signed in to change notification settings - Fork 0
/
Recycle_C.thy
1777 lines (1704 loc) · 85.9 KB
/
Recycle_C.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
theory Recycle_C
imports Delete_C Retype_C
begin
context kernel_m
begin
lemma isArchPageCap_ArchObjectCap:
"isArchPageCap (ArchObjectCap acap)
= isPageCap acap"
by (simp add: isArchPageCap_def isPageCap_def)
definition
"replicateHider \<equiv> replicate"
lemma collapse_foldl_replicate:
"replicate (length xs) v = xs \<Longrightarrow>
foldl (op @) [] (map (\<lambda>_. xs) ys)
= replicateHider (length xs * length ys) v"
apply (induct ys rule: rev_induct)
apply (simp add: replicateHider_def)
apply (simp add: replicateHider_def)
apply (subst add.commute, simp add: replicate_add)
done
lemma coerce_memset_to_heap_update_user_data:
"heap_update_list x (replicateHider 4096 0)
= heap_update (Ptr x :: user_data_C ptr)
(user_data_C (FCP (\<lambda>_. 0)))"
apply (intro ext, simp add: heap_update_def)
apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
apply (simp add: to_bytes_def size_of_def typ_info_simps user_data_C_tag_def)
apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)
apply (simp add: typ_info_simps
user_context_C_tag_def thread_state_C_tag_def fault_C_tag_def
lookup_fault_C_tag_def update_ti_t_ptr_0s
ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td
ti_typ_combine_empty_ti ti_typ_combine_td
align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def
align_td_array' size_td_array)
apply (simp add: typ_info_array')
apply (subst access_ti_list_array)
apply simp
apply simp
apply (simp add: fcp_beta typ_info_word typ_info_ptr word_rsplit_0)
apply fastforce
apply (simp add: collapse_foldl_replicate)
done
lemma clift_foldl_hrs_mem_update:
"\<lbrakk> \<forall>x \<in> set xs. hrs_htd s \<Turnstile>\<^sub>t f x;
\<And>x s. hrs_htd s \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) s)
= g (clift s :: ('a :: c_type) ptr \<rightharpoonup> 'a) x \<rbrakk>
\<Longrightarrow>
clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) s)
= foldl g (clift s :: 'a ptr \<rightharpoonup> 'a) xs"
using [[hypsubst_thin]]
apply (cases s, clarsimp)
apply (induct xs arbitrary: a b)
apply (simp add: hrs_mem_update_def)
apply (clarsimp simp add: hrs_mem_update_def split_def hrs_htd_def)
done
lemma map_to_user_data_aligned:
"\<lbrakk> map_to_user_data (ksPSpace s) x = Some y; pspace_aligned' s \<rbrakk>
\<Longrightarrow> is_aligned x pageBits"
apply (clarsimp simp: map_comp_eq projectKOs split: option.split_asm)
apply (drule(1) pspace_alignedD')
apply (simp add: objBits_simps)
done
lemma help_force_intvl_range_conv:
"\<lbrakk> is_aligned (p::word32) n; v = 2 ^ n; n < word_bits \<rbrakk>
\<Longrightarrow> {p ..+ v} = {p .. p + 2 ^ n - 1}"
by (simp add: intvl_range_conv word_bits_def)
lemma cmap_relation_If_upd:
"\<lbrakk> cmap_relation f g ptrfun rel; rel v v'; ptrfun ` S = S'; inj ptrfun \<rbrakk>
\<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> S then Some v else f x)
(\<lambda>y. if y \<in> S' then Some v' else g y)
ptrfun rel"
apply (simp add: cmap_relation_def dom_If_Some)
apply (rule context_conjI)
apply blast
apply clarsimp
apply (case_tac "x \<in> S")
apply simp
apply clarsimp
apply (subst if_not_P)
apply (clarsimp simp: inj_eq)
apply (drule bspec, erule domI)
apply simp
done
lemma length_replicateHider [simp]:
"length (replicateHider n x) = n"
by (simp add: replicateHider_def)
lemma coerce_heap_update_to_heap_updates':
"n = chunk * m \<Longrightarrow>
heap_update_list x (replicateHider n 0)
= (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s
(map (\<lambda>n. x + (of_nat n * of_nat chunk)) [0 ..< m]))"
using [[hypsubst_thin]]
apply clarsimp
apply (induct m arbitrary: x)
apply (rule ext, simp)
apply (simp add: replicateHider_def)
apply (rule ext)
apply (simp only: map_upt_unfold map_Suc_upt[symmetric])
apply (simp add: replicate_add[folded replicateHider_def]
heap_update_list_concat_unfold
o_def field_simps
length_replicate[folded replicateHider_def])
done
lemma h_t_valid_dom_s:
"\<lbrakk> h_t_valid htd c_guard p; x = ptr_val (p :: ('a :: mem_type) ptr);
n = size_of TYPE ('a) \<rbrakk>
\<Longrightarrow> {x ..+ n} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s htd"
apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def
intvl_def)
apply (drule_tac x=k in spec, simp add: size_of_def)
apply (clarsimp simp: dom_s_def)
apply (drule_tac x=0 in map_leD, simp_all)
done
lemma user_page_at_rf_sr_dom_s:
"\<lbrakk> typ_at' UserDataT x s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> {x ..+ 2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))"
apply (drule rf_sr_heap_relation)
apply (drule user_data_at_ko)
apply (erule_tac x=x in cmap_relationE1)
apply (simp only: heap_to_page_data_def Let_def ko_at_projectKO_opt)
apply simp
apply (drule h_t_valid_clift)
apply (simp add: h_t_valid_dom_s pageBits_def)
done
lemma intvl_2_power_times_decomp:
"\<forall>y < 2 ^ (n - m). {x + y * 2 ^ m ..+ 2 ^ m} \<times> S \<subseteq> T
\<Longrightarrow> m \<le> n \<Longrightarrow> n < word_bits
\<Longrightarrow> {(x :: word32) ..+ 2 ^ n} \<times> S \<subseteq> T"
apply (clarsimp simp: intvl_def)
apply (drule_tac x="of_nat k >> m" in spec)
apply (drule mp)
apply (rule shiftr_less_t2n)
apply (rule word_of_nat_less)
apply (simp add: word_of_nat_less)
apply (erule subsetD)
apply (clarsimp simp: shiftl_t2n[unfolded mult.commute mult.left_commute, symmetric]
shiftr_shiftl1)
apply (rule_tac x="unat (of_nat k && mask m :: word32)" in exI)
apply (simp add: field_simps word_plus_and_or_coroll2)
apply (simp add: word_bits_def unat_less_power and_mask_less')
done
lemma flex_user_page_at_rf_sr_dom_s:
"\<lbrakk> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits).
typ_at' UserDataT (x + p * 2 ^ pageBits) s); (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> {x ..+ 2 ^ pageBitsForSize sz} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))"
apply (rule_tac m=pageBits in intvl_2_power_times_decomp,
simp_all add: pbfs_atleast_pageBits pbfs_less_wb')
apply (erule allEI, clarsimp)
apply (drule(1) user_page_at_rf_sr_dom_s)
apply (erule subsetD)
apply simp
done
lemma clearMemory_PageCap_ccorres:
"ccorres dc xfdc (invs' and valid_cap' (ArchObjectCap (PageCap ptr undefined sz None))
and K ({ptr .. ptr + 2 ^ (pageBitsForSize sz) - 1} \<inter> kernel_data_refs = {}))
(UNIV \<inter> {s. bits_' s = of_nat (pageBitsForSize sz)}
\<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr})
[]
(doMachineOp (clearMemory ptr (2 ^ pageBitsForSize sz))) (Call clearMemory_'proc)"
(is "ccorres dc xfdc ?P ?P' [] ?m ?c")
apply (cinit' lift: bits_' ptr___ptr_to_unsigned_long_')
apply (rule_tac P="capAligned (ArchObjectCap (PageCap ptr undefined sz None))"
in ccorres_gen_asm)
apply (rule ccorres_Guard_Seq)
apply (simp add: clearMemory_def)
apply (simp add: doMachineOp_bind ef_storeWord)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac P="?P" in ccorres_from_vcg[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: valid_cap'_def capAligned_def
is_aligned_no_wrap'[OF _ word32_power_less_1])
apply (subgoal_tac "2 \<le> pageBitsForSize sz")
prefer 2
apply (simp add: pageBitsForSize_def split: vmpage_size.split)
apply (rule conjI)
apply (erule is_aligned_weaken)
apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
apply (rule conjI)
apply (rule is_aligned_power2)
apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
apply (simp add: flex_user_page_at_rf_sr_dom_s)
apply (clarsimp simp: field_simps word_size_def mapM_x_storeWord_step)
apply (simp add: doMachineOp_def split_def exec_gets)
apply (simp add: select_f_def simpler_modify_def bind_def)
apply (fold replicateHider_def)[1]
apply (subst coerce_heap_update_to_heap_updates'
[where chunk=4096 and m="2 ^ (pageBitsForSize sz - pageBits)"])
apply (simp add: pageBitsForSize_def pageBits_def
split: vmpage_size.split)
apply (subst coerce_memset_to_heap_update_user_data)
apply (subgoal_tac "\<forall>p<2 ^ (pageBitsForSize sz - pageBits).
x \<Turnstile>\<^sub>c (Ptr (ptr + of_nat p * 0x1000) :: user_data_C ptr)")
prefer 2
apply (erule allfEI[where f=of_nat])
apply clarsimp
apply (subst(asm) of_nat_power, assumption)
apply simp
apply (insert pageBitsForSize_32 [of sz])[1]
apply (erule order_le_less_trans [rotated])
apply simp
apply (simp, drule ko_at_projectKO_opt[OF user_data_at_ko])
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def)
apply (erule cmap_relationE1, simp(no_asm) add: heap_to_page_data_def Let_def)
apply fastforce
apply (simp add: pageBits_def typ_heap_simps)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
apply (clarsimp simp: cpspace_relation_def typ_heap_simps
clift_foldl_hrs_mem_update foldl_id
carch_state_relation_def
cmachine_state_relation_def
foldl_fun_upd_const[unfolded fun_upd_def])
apply (subst help_force_intvl_range_conv, assumption)
apply (simp add: pageBitsForSize_def split: vmpage_size.split)
apply assumption
apply (subst heap_to_page_data_update_region)
apply (drule map_to_user_data_aligned, clarsimp)
apply (rule aligned_range_offset_mem_helper[where m=pageBits], simp_all)[1]
apply (rule pbfs_atleast_pageBits)
apply (erule cmap_relation_If_upd)
apply (clarsimp simp: cuser_data_relation_def fcp_beta
order_less_le_trans[OF unat_lt2p])
apply (fold word_rsplit_0, simp add: word_rcat_rsplit)[1]
apply (rule image_cong[OF _ refl])
apply (rule set_eqI, rule iffI)
apply (clarsimp simp del: atLeastAtMost_iff)
apply (drule map_to_user_data_aligned, clarsimp)
apply (simp only: mask_in_range[symmetric])
apply (rule_tac x="unat ((xa && mask (pageBitsForSize sz)) >> pageBits)" in image_eqI)
apply (simp add: subtract_mask(2)[symmetric])
apply (cut_tac w="xa - ptr" and n=pageBits in and_not_mask[symmetric])
apply (simp add: shiftl_t2n field_simps pageBits_def)
apply (subst aligned_neg_mask, simp_all)[1]
apply (erule aligned_sub_aligned, simp_all add: word_bits_def)[1]
apply (erule is_aligned_weaken)
apply (rule pbfs_atleast_pageBits[unfolded pageBits_def])
apply simp
apply (rule unat_less_power)
apply (fold word_bits_def, simp)
apply (rule shiftr_less_t2n)
apply (simp add: pbfs_atleast_pageBits)
apply (rule and_mask_less_size)
apply (simp add: word_bits_def word_size)
apply (rule IntI)
apply (clarsimp simp del: atLeastAtMost_iff)
apply (subst aligned_range_offset_mem_helper, assumption, simp_all)[1]
apply (rule order_le_less_trans[rotated], erule shiftl_less_t2n [OF of_nat_power],
simp_all add: word_bits_def)[1]
apply (insert pageBitsForSize_32 [of sz])[1]
apply (erule order_le_less_trans [rotated])
apply simp
apply (simp add: pageBits_def shiftl_t2n field_simps)
apply clarsimp
apply (drule_tac x="of_nat n" in spec)
apply (simp add: of_nat_power[where 'a=32, folded word_bits_def])
apply (rule exI)
apply (simp add: pageBits_def ko_at_projectKO_opt[OF user_data_at_ko])
apply simp
apply csymbr
apply (ctac add: cleanCacheRange_PoU_ccorres[unfolded dc_def])
apply wp
apply (simp add: guard_is_UNIV_def unat_of_nat
word_bits_def capAligned_def word_of_nat_less)
apply (clarsimp simp: word_bits_def valid_cap'_def
capAligned_def word_of_nat_less)
apply (frule is_aligned_addrFromPPtr_n, simp add: pageBitsForSize_def split: vmpage_size.splits)
apply (clarsimp simp: is_aligned_no_overflow'[where n=12, simplified]
is_aligned_no_overflow'[where n=16, simplified]
is_aligned_no_overflow'[where n=20, simplified]
is_aligned_no_overflow'[where n=24, simplified] pageBits_def
field_simps is_aligned_mask[symmetric] mask_AND_less_0
pageBitsForSize_def split: vmpage_size.splits)
done
lemma coerce_memset_to_heap_update_asidpool:
"heap_update_list x (replicateHider 4096 0)
= heap_update (Ptr x :: asid_pool_C ptr)
(asid_pool_C (FCP (\<lambda>x. Ptr 0)))"
apply (intro ext, simp add: heap_update_def)
apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
apply (simp add: to_bytes_def size_of_def typ_info_simps asid_pool_C_tag_def)
apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)
apply (simp add: typ_info_simps
user_context_C_tag_def thread_state_C_tag_def fault_C_tag_def
lookup_fault_C_tag_def update_ti_t_ptr_0s
ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td
ti_typ_combine_empty_ti ti_typ_combine_td
align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def
align_td_array' size_td_array)
apply (simp add: typ_info_array')
apply (subst access_ti_list_array)
apply simp
apply simp
apply (simp add: fcp_beta typ_info_word typ_info_ptr word_rsplit_0)
apply fastforce
apply (simp add: collapse_foldl_replicate)
done
declare replicate_numeral [simp]
lemma coerce_memset_to_heap_update_pte:
"heap_update_list x (replicateHider 4 0)
= heap_update (Ptr x :: pte_C ptr)
(pte_C.pte_C (FCP (\<lambda>x. 0)))"
apply (intro ext, simp add: heap_update_def)
apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
apply (simp add: to_bytes_def size_of_def typ_info_simps pte_C_tag_def)
apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)
apply (simp add: typ_info_simps align_td_array' size_td_array)
apply (simp add: typ_info_array' typ_info_word word_rsplit_0)
apply (simp add: replicateHider_def)
done
lemma coerce_memset_to_heap_update_pde:
"heap_update_list x (replicateHider 4 0)
= heap_update (Ptr x :: pde_C ptr)
(pde_C.pde_C (FCP (\<lambda>x. 0)))"
apply (intro ext, simp add: heap_update_def)
apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
apply (simp add: to_bytes_def size_of_def typ_info_simps pde_C_tag_def)
apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)
apply (simp add: typ_info_simps align_td_array' size_td_array)
apply (simp add: typ_info_array' typ_info_word word_rsplit_0)
apply (simp add: replicateHider_def)
done
lemma objBits_eq_by_type:
fixes x :: "'a :: pspace_storable" and y :: 'a
shows "objBits x = objBits y"
apply (simp add: objBits_def)
apply (rule objBits_type)
apply (simp add: koTypeOf_injectKO)
done
lemma mapM_x_store_memset_ccorres_assist:
fixes val :: "'a :: pspace_storable"
assumes nofail: "\<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>)"
assumes slots1: "\<forall>n < length slots. slots ! n = hd slots + (of_nat n << objBits val)"
assumes slots2: "n = length slots * (2 ^ objBits val)"
assumes ptr: "ptr = hd slots"
assumes ko: "\<And>ko :: 'a. updateObject ko = updateObject_default ko"
"\<And>ko :: 'a. (1 :: word32) < 2 ^ objBits ko"
assumes restr: "set slots \<subseteq> S"
assumes worker: "\<And>ptr s s' (ko :: 'a). \<lbrakk> (s, s') \<in> rf_sr; ko_at' ko ptr s; ptr \<in> S \<rbrakk>
\<Longrightarrow> (s \<lparr> ksPSpace := ksPSpace s (ptr \<mapsto> injectKO val)\<rparr>,
globals_update (t_hrs_'_update (hrs_mem_update
(heap_update_list ptr
(replicateHider (2 ^ objBits val) (ucast c))))) s') \<in> rf_sr"
assumes rf_sr: "(\<sigma>, s) \<in> rf_sr"
shows
"\<exists>(rv, \<sigma>') \<in> fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>).
(\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update
(heap_update_list ptr (replicateHider n c)))) s) \<in> rf_sr"
unfolding slots2 ptr using rf_sr slots1 nofail restr
proof (induct slots arbitrary: s \<sigma>)
case Nil
show ?case
using Nil.prems
apply (simp add: mapM_x_def sequence_x_def return_def replicateHider_def)
apply (simp add: rf_sr_def hrs_mem_update_def cstate_relation_def Let_def
carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff)
done
next
case (Cons x xs tPre sPre)
note nofail_bind = Cons.prems(3)[unfolded mapM_x_Cons K_bind_def]
have obj_at: "obj_at' (\<lambda>x :: 'a. True) x sPre"
using not_snd_bindI1[OF nofail_bind]
apply (subst(asm) setObject_obj_at_pre, simp_all add: ko snd_bind)
apply (clarsimp simp: stateAssert_def exec_get return_def)
apply (simp add: koTypeOf_injectKO typ_at_to_obj_at')
done
note in_setObject = setObject_eq[OF _ _ objBits_eq_by_type obj_at,
where ko=val, simplified ko, simplified]
note nofail_mapM = not_snd_bindI2[OF nofail_bind, OF in_setObject]
have hd_xs: "xs \<noteq> [] \<Longrightarrow> hd xs = x + (2 ^ objBits val)"
using Cons.prems(2)[rule_format, where n=1]
by (simp add: hd_conv_nth)
show ?case
using obj_at_ko_at'[OF obj_at] Cons.prems(4)
apply (clarsimp simp add: mapM_x_Cons bind_def split_def)
apply (rule rev_bexI, rule in_setObject)
apply (cut_tac Cons.hyps[OF _ _ nofail_mapM])
defer
apply (rule worker, rule Cons.prems, assumption+)
apply clarsimp
apply (case_tac "xs = []", simp_all)[1]
apply (insert Cons.prems, simp)[1]
apply (frule_tac x="Suc n" in spec)
apply (simp add: hd_xs shiftl_t2n field_simps)
apply assumption
apply clarsimp
apply (rule rev_bexI, assumption)
apply (simp add: o_def)
apply (case_tac "xs = []")
apply (simp add: hrs_mem_update_def split_def replicateHider_def)
apply (subst(asm) heap_update_list_concat_fold_hrs_mem)
apply (simp add: hd_xs replicateHider_def)
apply (simp add: replicateHider_def replicate_add)
done
qed
lemma invalidateTLBByASID_ccorres:
"ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits))
(UNIV \<inter> {s. asid_' s = asid}) []
(invalidateTLBByASID asid) (Call invalidateTLBByASID_'proc)"
apply (cinit lift: asid_')
apply (ctac(no_vcg) add: loadHWASID_ccorres)
apply csymbr
apply (simp add: case_option_If2 del: Collect_const)
apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>])
apply (clarsimp simp: pde_stored_asid_def to_bool_def split: split_if)
apply (rule ccorres_return_void_C[unfolded dc_def])
apply (simp add: dc_def[symmetric])
apply csymbr
apply (ctac add: invalidateTLB_ASID_ccorres)
apply vcg
apply (wp hoare_drop_imps)
apply (clarsimp simp: pde_stored_asid_def to_bool_def)
done
(* FIXME: also in VSpace_C *)
lemma ignoreFailure_liftM:
"ignoreFailure = liftM (\<lambda>v. ())"
apply (rule ext)+
apply (simp add: ignoreFailure_def liftM_def
catch_def)
apply (rule bind_apply_cong[OF refl])
apply (simp split: sum.split)
done
end
crunch pde_mappings'[wp]: invalidateTLBByASID "valid_pde_mappings'"
crunch ksArchState[wp]: invalidateTLBByASID "\<lambda>s. P (ksArchState s)"
context kernel_m begin
lemma page_table_at_rf_sr_dom_s:
"\<lbrakk> page_table_at' x s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> {x ..+ 2 ^ ptBits} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))"
apply (rule_tac m=2 in intvl_2_power_times_decomp,
simp_all add: shiftl_t2n field_simps ptBits_def pageBits_def
word_bits_def)
apply (clarsimp simp: page_table_at'_def intvl_def)
apply (drule spec, drule(1) mp)
apply (simp add: typ_at_to_obj_at_arches)
apply (drule obj_at_ko_at', clarsimp)
apply (erule cmap_relationE1[OF rf_sr_cpte_relation])
apply (erule ko_at_projectKO_opt)
apply (drule h_t_valid_clift)
apply (drule h_t_valid_dom_s[OF _ refl refl])
apply (erule subsetD)
apply (auto simp add: intvl_def shiftl_t2n)[1]
done
lemma page_directory_at_rf_sr_dom_s:
"\<lbrakk> page_directory_at' x s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> {x ..+ 2 ^ pdBits} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))"
apply (rule_tac m=2 in intvl_2_power_times_decomp,
simp_all add: shiftl_t2n field_simps pdBits_def pageBits_def
word_bits_def)
apply (clarsimp simp: page_directory_at'_def intvl_def)
apply (drule spec, drule(1) mp)
apply (simp add: typ_at_to_obj_at_arches)
apply (drule obj_at_ko_at', clarsimp)
apply (erule cmap_relationE1[OF rf_sr_cpde_relation])
apply (erule ko_at_projectKO_opt)
apply (drule h_t_valid_clift)
apply (drule h_t_valid_dom_s[OF _ refl refl])
apply (erule subsetD)
apply (auto simp add: intvl_def shiftl_t2n)[1]
done
lemma clearMemory_setObject_PTE_ccorres:
"ccorres dc xfdc (page_table_at' ptr and (\<lambda>_. is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr))
(UNIV \<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr} \<inter> {s. bits_' s = of_nat ptBits}) []
(do x \<leftarrow> mapM_x (\<lambda>a. setObject a Hardware_H.pte.InvalidPTE)
[ptr , ptr + 2 ^ objBits Hardware_H.pte.InvalidPTE .e. ptr + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) pstart)
od)
(Call clearMemory_'proc)"
apply (rule ccorres_gen_asm)+
apply (cinit' lift: ptr___ptr_to_unsigned_long_' bits_')
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac P="page_table_at' ptr"
in ccorres_from_vcg_nofail[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: replicateHider_def[symmetric])
apply (frule is_aligned_no_overflow')
apply (intro conjI)
apply (clarsimp simp add: ptBits_def pageBits_def
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (erule is_aligned_weaken, simp add: ptBits_def pageBits_def)
apply (clarsimp simp: is_aligned_def ptBits_def pageBits_def)
apply (simp add: unat_of_nat32 order_less_le_trans[OF pt_bits_stuff(2)]
word_bits_def page_table_at_rf_sr_dom_s)
apply (clarsimp simp add: ptBits_def pageBits_def
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (simp add: upto_enum_step_def objBits_simps ptBits_def pageBits_def
field_simps linorder_not_less[symmetric] archObjSize_def
upto_enum_word split_def)
apply (erule mapM_x_store_memset_ccorres_assist
[unfolded split_def, OF _ _ _ _ _ _ subset_refl],
simp_all add: shiftl_t2n hd_map objBits_simps archObjSize_def)[1]
apply (rule cmap_relationE1, erule rf_sr_cpte_relation, erule ko_at_projectKO_opt)
apply (subst coerce_memset_to_heap_update_pte)
apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps)
apply (rule conjI)
apply (simp add: cpspace_relation_def typ_heap_simps update_pte_map_tos
update_pte_map_to_ptes)
apply (rule cmap_relation_updI, simp_all)[1]
apply (simp add: cpte_relation_def Let_def pte_lift_def
fcp_beta pte_get_tag_def pte_tag_defs)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps)
apply csymbr
apply (rule ccorres_Guard)
apply (ctac add: cleanCacheRange_PoU_ccorres)
apply wp
apply (clarsimp simp: guard_is_UNIV_def ptBits_def pageBits_def)
apply (clarsimp simp: ptBits_def pageBits_def)
apply (frule is_aligned_addrFromPPtr_n, simp)
apply (clarsimp simp: is_aligned_no_overflow'[where n=10, simplified] pageBits_def
field_simps is_aligned_mask[symmetric] mask_AND_less_0)
done
lemma ccorres_make_xfdc:
"ccorresG rf_sr \<Gamma> r xf P P' h a c \<Longrightarrow> ccorresG rf_sr \<Gamma> dc xfdc P P' h a c"
apply (erule ccorres_rel_imp)
apply simp
done
lemma ccorres_if_True_False_simps:
"ccorres r xf P P' hs a (IF True THEN c ELSE c' FI) = ccorres r xf P P' hs a c"
"ccorres r xf P P' hs a (IF False THEN c ELSE c' FI) = ccorres r xf P P' hs a c'"
"ccorres r xf P P' hs a (IF True THEN c ELSE c' FI ;; d) = ccorres r xf P P' hs a (c ;; d)"
"ccorres r xf P P' hs a (IF False THEN c ELSE c' FI ;; d) = ccorres r xf P P' hs a (c' ;; d)"
by (simp_all add: ccorres_cond_iffs ccorres_seq_simps)
lemmas cap_tag_values =
cap_untyped_cap_def
cap_endpoint_cap_def
cap_async_endpoint_cap_def
cap_reply_cap_def
cap_cnode_cap_def
cap_thread_cap_def
cap_irq_handler_cap_def
cap_null_cap_def
cap_irq_control_cap_def
cap_zombie_cap_def
cap_small_frame_cap_def
cap_frame_cap_def
cap_page_table_cap_def
cap_page_directory_cap_def
cap_asid_pool_cap_def
lemma resetMemMapping_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. c_valid_cap (cap_' s)\<rbrace>
Call resetMemMapping_'proc
{s'. option_map ((\<lambda>acap. case acap of ArchObjectCap acap' \<Rightarrow> ArchObjectCap (resetMemMapping acap') | _ \<Rightarrow> acap) \<circ> cap_to_H) (cap_lift (cap_' s)) =
option_map cap_to_H (cap_lift (ret__struct_cap_C_' s')) \<and> c_valid_cap (ret__struct_cap_C_' s')}"
apply vcg
apply (subgoal_tac "\<forall>t cap. (scast (t :: sword32) = cap_get_tag cap) = (cap_get_tag cap = scast t)")
apply clarsimp
apply (intro impI allI conjI)
apply (auto simp: isCap_simps resetMemMapping_def cap_to_H_simps cap_lifts ccap_relation_def c_valid_cap_def cl_valid_cap_def
asidInvalid_def)[7]
apply (clarsimp split: capability.splits cap_CL.splits option.splits)
apply (rename_tac arch_capability)
apply (case_tac arch_capability,
auto simp: resetMemMapping_def cap_to_H_def
cap_small_frame_cap_lift_def cap_frame_cap_lift_def
cap_page_table_cap_lift_def cap_page_directory_cap_lift_def
cap_lift_def cap_tag_values Let_def
split: cap_CL.splits split_if_asm)
done
lemma ccorres_return_C_seq:
"\<lbrakk>\<And>s f. xf (global_exn_var_'_update f (xfu (\<lambda>_. v s) s)) = v s; \<And>s f. globals (xfu f s) = globals s; wfhandlers hs\<rbrakk>
\<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return rv) (return_C xfu v ;; d)"
apply (rule ccorres_guard_imp)
apply (rule ccorres_split_throws, rule ccorres_return_C, simp+)
apply vcg
apply simp_all
done
lemma arch_recycleCap_ccorres_helper:
notes Collect_const [simp del]
notes ccorres_if_True_False_simps [simp]
shows "ccorres (\<lambda>a. ccap_relation (ArchObjectCap a)) ret__struct_cap_C_'
(invs' and valid_cap' (ArchObjectCap cp) and K (ccap_relation (ArchObjectCap cp) cap))
UNIV [SKIP]
(do y \<leftarrow> ArchRetypeDecls_H.finaliseCap cp is_final;
return (resetMemMapping cp)
od)
(call (\<lambda>s. s\<lparr>cap_' := cap, final_' := from_bool is_final\<rparr>) Arch_finaliseCap_'proc (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>s t. Basic (\<lambda>s. s));;
(\<acute>ret__struct_cap_C :== CALL resetMemMapping(cap);;
(return_C ret__struct_cap_C_'_update ret__struct_cap_C_' ;; cruft)))"
apply (rule ccorres_guard_imp2)
apply (ctac (no_vcg) add: ccorres_make_xfdc [OF Arch_finaliseCap_ccorres])
apply csymbr -- "C reset mem mapping"
apply (rule ccorres_return_C_seq, simp_all)[1]
apply wp
apply (clarsimp elim!: ccap_relationE simp: option_map_Some_eq2 ccap_relation_def)
done
lemma arch_recycleCap_ccorres_helper':
notes Collect_const [simp del]
notes ccorres_if_True_False_simps [simp]
shows "ccorres (\<lambda>a. ccap_relation (ArchObjectCap a)) ret__struct_cap_C_'
(invs' and valid_cap' (ArchObjectCap cp) and K (ccap_relation (ArchObjectCap cp) cap))
UNIV
[SKIP]
(do y \<leftarrow> ArchRetypeDecls_H.finaliseCap cp is_final;
return (if is_final then resetMemMapping cp else cp)
od)
(call (\<lambda>s. s\<lparr>cap_' := cap, final_' := from_bool is_final\<rparr>) Arch_finaliseCap_'proc (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>s t. Basic (\<lambda>s. s));;
(Cond \<lbrace>from_bool is_final \<noteq> 0\<rbrace>
(\<acute>ret__struct_cap_C :== CALL resetMemMapping(cap);;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_')
SKIP;;
(return_C ret__struct_cap_C_'_update (\<lambda>s. cap);; cruft)))"
apply (rule ccorres_guard_imp2)
apply (ctac (no_vcg) add: ccorres_make_xfdc [OF Arch_finaliseCap_ccorres])
apply (simp add: if_distrib [where f = return])
apply (rule ccorres_if_cond_throws [where Q=\<top> and Q'=\<top>])
apply (simp add: from_bool_0)
apply csymbr
apply (rule ccorres_return_C, simp_all)[1]
apply (rule ccorres_return_C_seq, simp_all)[1]
apply vcg
apply wp
apply (clarsimp simp: from_bool_0 ccap_relation_def option_map_Some_eq2)
done
lemma arch_recycleCap_ccorres:
notes Collect_const [simp del]
notes ccorres_if_True_False_simps [simp]
notes if_cong[cong]
shows "ccorres (ccap_relation o ArchObjectCap) ret__struct_cap_C_'
(invs' and valid_cap' (ArchObjectCap cp)
and (\<lambda>s. capRange (ArchObjectCap cp) \<inter> kernel_data_refs = {}))
(UNIV \<inter> {s. (is_final_' s) = from_bool is_final} \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
) []
(ArchRetypeDecls_H.recycleCap is_final cp) (Call Arch_recycleCap_'proc)"
apply (rule ccorres_gen_asm)
apply (cinit lift: is_final_' cap_' )
apply csymbr
apply (simp add: ArchRetype_H.recycleCap_def cap_get_tag_isCap
cap_get_tag_isCap_ArchObject
isArchPageCap_ArchObjectCap
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_if_lhs)
apply (simp add: ccorres_cond_iffs Collect_True
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (csymbr, csymbr)
apply (simp add: doMachineOp_bind shiftL_nat)
apply (ctac (no_vcg) add: clearMemory_PageCap_ccorres)
apply (rule arch_recycleCap_ccorres_helper)
apply wp
apply (rule ccorres_if_lhs)
apply (simp add: ccorres_cond_iffs Collect_True Collect_False
Let_def
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_rhs_assoc)+
apply (csymbr, csymbr, csymbr)
apply (subst bind_assoc[symmetric])
apply (rule ccorres_split_nothrow_novcg_dc)
apply (simp add: storePTE_def)
apply (ctac add: clearMemory_setObject_PTE_ccorres)
apply csymbr
apply (rule_tac P="ret__unsigned_long = from_bool (capPTMappedAddress cp \<noteq> None)"
in ccorres_gen_asm2)
apply wpc
apply (simp add: false_def)
apply (rule arch_recycleCap_ccorres_helper')
apply (simp add: split_def true_def bind_assoc)
apply (rule ccorres_rhs_assoc)+
apply csymbr
apply csymbr
apply (ctac(no_vcg) add: pageTableMapped_ccorres)
apply (simp add: case_option_If del: Collect_const)
apply (ctac (no_vcg, no_simp) add: ccorres_when [where R = \<top>]) -- "leave guard = goal and a call to invalidateTLB"
apply (simp add: option_to_0_def option_to_ptr_def
split: option.splits)
apply (ctac (no_vcg) add: invalidateTLBByASID_ccorres)
apply (rule arch_recycleCap_ccorres_helper')
apply wp
apply simp
apply simp
apply (wp hoare_drop_imps)[1]
apply (rule_tac Q="\<lambda>rv. invs' and valid_cap' (ArchObjectCap cp)"
in hoare_post_imp)
apply (clarsimp simp: valid_cap'_def isCap_simps mask_def)
apply (wp mapM_x_wp' | simp)+
apply (clarsimp simp: guard_is_UNIV_def cap_get_tag_isCap_ArchObject)
apply (simp add: cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_lift_page_table_cap cap_to_H_def
cap_page_table_cap_lift_def to_bool_def
true_def false_def
elim!: ccap_relationE split: split_if_asm)
apply (clarsimp simp: word_neq_0_conv resetMemMapping_def
ccap_relation_def option_map_Some_eq2)
apply (rule ccorres_if_lhs)
apply (simp add: ccorres_cond_iffs Collect_True Collect_False
Let_def ARMSectionBits_def
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (csymbr, csymbr)
apply (rule ccorres_Guard_Seq)+
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac P="capPDBasePtr_CL (cap_page_directory_cap_lift cap) = capPDBasePtr cp"
in ccorres_gen_asm2)
apply (rule_tac P="valid_cap' (ArchObjectCap cp) and K (capPDBasePtr cp \<noteq> 0)"
in ccorres_from_vcg_nofail[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: replicateHider_def[symmetric] valid_cap'_def
capAligned_def)
apply (clarsimp simp: isCap_simps storePDE_def)
apply (subst is_aligned_no_wrap', assumption)
apply simp
apply clarsimp
apply (intro conjI)
apply (erule is_aligned_weaken, simp)
apply (clarsimp simp: is_aligned_def)
apply (clarsimp simp: valid_cap'_def)
apply (drule(1) page_directory_at_rf_sr_dom_s)
apply (clarsimp simp: pdBits_def pageBits_def)
apply (erule subsetD, simp)
apply (erule subsetD[rotated], rule intvl_start_le)
apply simp
apply (clarsimp simp: split_def upto_enum_word kernelBase_def
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (erule_tac S="{x. valid_pde_mapping_offset' (x && mask pdBits)}"
in mapM_x_store_memset_ccorres_assist[unfolded split_def],
simp_all add: hd_map objBits_simps archObjSize_def)[1]
apply (clarsimp simp: pdBits_def pageBits_def)
apply (subst field_simps, simp add: mask_add_aligned)
apply (simp add: valid_pde_mapping_offset'_def)
apply (subst iffD2[OF mask_eq_iff_w2p])
apply (simp add: word_size)
apply (rule shiftl_less_t2n)
apply (rule of_nat_power)
apply simp+
apply (rule notI, drule arg_cong[where f="\<lambda>a. a >> 2"],
subst(asm) shiftl_shiftr_id)
apply (simp add: word_bits_def)
apply (rule of_nat_power)
apply (simp add: word_bits_def)
apply (simp add: word_bits_def)
apply (erule notE[rotated], rule less_imp_neq, rule word_of_nat_less)
apply (simp add: pd_asid_slot_def)
apply (rule cmap_relationE1, erule rf_sr_cpde_relation, erule ko_at_projectKO_opt)
apply (subst coerce_memset_to_heap_update_pde)
apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps)
apply (rule conjI)
apply (simp add: cpspace_relation_def typ_heap_simps update_pde_map_tos
update_pde_map_to_pdes)
apply (rule cmap_relation_updI, simp_all)[1]
apply (simp add: cpde_relation_def Let_def pde_lift_def
fcp_beta pde_get_tag_def pde_tag_defs)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps pde_stored_asid_update_valid_offset)
apply csymbr
apply (rule ccorres_Guard_Seq)+
apply (ctac(no_vcg) add: cleanCacheRange_PoU_ccorres)
apply csymbr
apply (rule_tac P="capPDBasePtr_CL (cap_page_directory_cap_lift cap) = capPDBasePtr cp
\<and> ret__unsigned_long = from_bool (capPDMappedASID cp \<noteq> None)"
in ccorres_gen_asm2)
apply wpc
apply (simp add: false_def)
apply (rule arch_recycleCap_ccorres_helper')
apply (simp add: split_def true_def bind_assoc)
apply (rule ccorres_rhs_assoc)+
apply csymbr
apply csymbr
apply (simp add: true_def ccorres_cond_iffs ignoreFailure_liftM)
apply (rule ccorres_rhs_assoc2)
apply (rule ccorres_split_nothrow_novcg_dc)
apply simp
apply (rule ccorres_split_nothrowE)
apply (ctac add: findPDForASID_ccorres)
apply ceqv
apply (simp add: liftE_liftM when_def dc_def[symmetric] del: Collect_const)
apply (rule ccorres_cond2[where R=\<top>])
apply fastforce
apply (ctac add: invalidateTLBByASID_ccorres)
apply (rule ccorres_return_Skip)
apply (simp add: ccorres_cond_iffs throwError_def)
apply (rule ccorres_return_Skip')
apply (wp hoare_drop_imps)
apply simp
apply (vcg exspec=findPDForASID_modifies)
apply (rule arch_recycleCap_ccorres_helper')
apply (wp | simp)+
apply (clarsimp simp: guard_is_UNIV_def)
apply (wp hoare_vcg_all_lift static_imp_wp | wp_once mapM_x_wp' | simp)+
apply (clarsimp simp: guard_is_UNIV_def
cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: field_simps pdBits_def pageBits_def word_sle_def)
apply (clarsimp simp: cap_lift_page_directory_cap cap_to_H_def
cap_page_directory_cap_lift_def
to_bool_def true_def false_def
elim!: ccap_relationE split: split_if_asm)
apply (simp add: word_neq_0_conv)
apply (rule ccorres_if_lhs)
apply (simp add: ccorres_cond_iffs Collect_True Collect_False
Let_def
del: Collect_const)
apply (rule ccorres_split_throws, rule ccorres_return_C, simp+)
apply vcg
apply (rule ccorres_if_lhs)
apply (simp add: ccorres_cond_iffs Collect_True Collect_False
Let_def
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (csymbr, csymbr, csymbr)
apply (rule ccorres_Guard_Seq)+
apply (rule ccorres_symb_exec_l
[OF _ gets_inv gets_wp empty_fail_gets])
apply (rule ccorres_split_nothrow_novcg_dc)
apply (simp add: when_def del: Collect_const)
apply (rule_tac R="\<lambda>s. rv = armKSASIDTable (ksArchState s)
\<and> capASIDPool cp \<noteq> 0"
in ccorres_cond2)
apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_to_H_def cap_lift_asid_pool_cap
cap_asid_pool_cap_lift_def
elim!: ccap_relationE)
apply (subst ucast_asid_high_bits_is_shift)
apply (simp add: mask_def asid_bits_def)
apply (rule word_and_le1)
apply (subst rf_sr_armKSASIDTable, assumption)
apply (simp add: asid_high_bits_word_bits)
apply (rule shiftr_less_t2n)
apply (rule order_le_less_trans [OF _ and_mask_less_size])
apply (simp add: asid_low_bits_def asid_high_bits_def mask_def)
apply (rule order_refl)
apply (simp add: asid_low_bits_def asid_high_bits_def word_size)
apply (simp add: option_to_ptr_def option_to_0_def
split: option.split)
apply (rule ccorres_rhs_assoc)+
apply (ctac(no_vcg) add: deleteASIDPool_ccorres)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac P="valid_cap' (ArchObjectCap cp) and no_0_obj'"
in ccorres_from_vcg[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric]
asidLowBits_handy_convs word_sle_def
word_sless_def)
apply (clarsimp simp: ccap_relation_def cap_asid_pool_cap_lift
cap_to_H_def valid_cap'_def capAligned_def
typ_at_to_obj_at_arches)
apply (drule obj_at_ko_at', clarsimp)
apply (rule cmap_relationE1[OF rf_sr_cpspace_asidpool_relation],
assumption)
apply (erule ko_at_projectKO_opt)
apply (frule h_t_valid_clift)
apply (subst h_t_valid_dom_s, assumption, simp)
apply (simp add: asid_low_bits_def)
apply simp
apply (rule conjI, clarsimp)
apply (rule conjI, erule is_aligned_no_wrap')
apply (clarsimp simp: asid_low_bits_def)
apply (rule conjI)
apply (erule is_aligned_weaken)
apply (clarsimp simp: asid_low_bits_def)
apply (rule conjI)
apply (clarsimp simp: is_aligned_def asid_low_bits_def)
apply (clarsimp simp: typ_at_to_obj_at_arches)
apply (rule rev_bexI, rule setObject_eq[where P=\<top>],
(simp add: objBits_simps archObjSize_def pageBits_def)+)
apply (simp add: obj_at'_weakenE[OF _ TrueI])
apply (simp only: replicateHider_def[symmetric])
apply (clarsimp simp: asid_low_bits_def)
apply (subst coerce_memset_to_heap_update_asidpool)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def typ_heap_simps
update_asidpool_map_tos
update_asidpool_map_to_asidpools)
apply (rule conjI)
apply (erule cmap_relation_updI, simp_all)[1]
apply (simp add: makeObject_asidpool casid_pool_relation_def)
apply (clarsimp simp: array_relation_def
option_to_ptr_def option_to_0_def)
apply (subst fcp_beta)
apply (simp add: asid_low_bits_def, unat_arith)
apply simp
apply (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps)
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: word_sle_def word_sless_def
asidLowBits_handy_convs
exec_gets simpler_modify_def
simp del: rf_sr_upd_safe)
apply (simp add: cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_lift_asid_pool_cap cap_to_H_def
cap_asid_pool_cap_lift_def
elim!: ccap_relationE
simp del: rf_sr_upd_safe)
apply (clarsimp simp: rf_sr_def cstate_relation_def
Let_def carch_state_relation_def carch_globals_def
cmachine_state_relation_def
h_t_valid_clift_Some_iff
asid_shiftr_low_bits_less[unfolded mask_def asid_bits_def]
word_and_le1)
apply (subst ucast_asid_high_bits_is_shift)
apply (simp add: mask_def asid_bits_def
word_and_le1)
apply (erule array_relation_update[unfolded fun_upd_def])
apply simp
apply (simp add: option_to_ptr_def option_to_0_def)
apply (simp add: asid_high_bits_def)
apply wp
apply (simp add: guard_is_UNIV_def)
apply (wp typ_at_lifts [OF deleteASIDPool_typ_at'])
apply (rule hoare_strengthen_post, rule deleteASIDPool_invs)
apply clarsimp
apply (rule ccorres_return_Skip)
apply (rule ccorres_split_throws)
apply (rule ccorres_return_C, simp+)
apply vcg
apply wp
apply (simp add: guard_is_UNIV_def)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (cases cp, simp_all add: isCap_simps)[1]
apply (clarsimp simp: word_sle_def word_sless_def
asidLowBits_handy_convs
cap_get_tag_isCap_ArchObject)
apply (cases cp, simp_all add: isCap_simps valid_cap'_def
capRange_def)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_lift_asid_pool_cap cap_to_H_def
cap_asid_pool_cap_lift_def
order_le_less_trans[OF word_and_le1]
valid_cap'_def capAligned_def
asid_shiftr_low_bits_less[unfolded mask_def asid_bits_def]
word_and_le1
elim!: ccap_relationE cong: conj_cong)
apply (rename_tac vmpage_size opt)
apply (simp add: capAligned_def)
apply (case_tac "vmpage_size = ARMSmallPage")
apply (frule(1) cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_lift_small_frame_cap cap_to_H_def
cap_small_frame_cap_lift_def
order_le_less_trans[OF word_and_le1]
valid_cap'_def capAligned_def
get_capSizeBits_CL_def get_capPtr_CL_def
elim!: ccap_relationE cong: conj_cong)
apply (simp add: cap_tag_defs)
apply (frule(1) cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_lift_frame_cap cap_to_H_def