-
Notifications
You must be signed in to change notification settings - Fork 106
/
Arch_DR.thy
1863 lines (1764 loc) · 93.1 KB
/
Arch_DR.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 Arch_DR
imports Untyped_DR
begin
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"make_arch_duplicate cap \<equiv> case cap of
cdl_cap.PageTableCap oid _ mp \<Rightarrow> cdl_cap.PageTableCap oid Fake None
| cdl_cap.FrameCap dev oid rghts sz _ mp \<Rightarrow> cdl_cap.FrameCap dev oid rghts sz Fake None"
definition
"get_pt_mapped_addr cap \<equiv>
case cap of (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) \<Rightarrow> transform_mapping asid
| _ \<Rightarrow> None"
definition
"transform_page_table_inv invok \<equiv> case invok of
ARM_A.PageTableMap cap slot pde slot' \<Rightarrow>
if (\<exists>oref attribs. pde = ARM_A.PageTablePDE (addrFromPPtr oref) attribs 0
\<and> is_pt_cap cap \<and> oref \<in> obj_refs cap)
then Some (cdl_page_table_invocation.PageTableMap (transform_cap cap)
(make_arch_duplicate (transform_cap cap))
(transform_cslot_ptr slot) (transform_pd_slot_ref slot'))
else None
| ARM_A.PageTableUnmap cap slot \<Rightarrow>
Some (cdl_page_table_invocation.PageTableUnmap (get_pt_mapped_addr cap)
(obj_ref_of cap) (transform_cslot_ptr slot))"
definition flush_type_map :: "ARM_A.flush_type \<Rightarrow> flush"
where "flush_type_map f \<equiv> case f of
ARM_A.Unify \<Rightarrow> flush.Unify
| ARM_A.Clean \<Rightarrow> flush.Clean
| ARM_A.Invalidate \<Rightarrow> flush.Invalidate
| ARM_A.CleanInvalidate \<Rightarrow> flush.CleanInvalidate"
definition transform_page_dir_inv :: "ARM_A.page_directory_invocation \<Rightarrow> cdl_page_directory_invocation option"
where "transform_page_dir_inv invok \<equiv> case invok of
ARM_A.page_directory_invocation.PageDirectoryFlush flush _ _ _ _ _ \<Rightarrow>
Some (cdl_page_directory_invocation.PageDirectoryFlush (flush_type_map flush))
|ARM_A.page_directory_invocation.PageDirectoryNothing \<Rightarrow>
Some (cdl_page_directory_invocation.PageDirectoryNothing) "
definition transform_page_inv :: "ARM_A.page_invocation \<Rightarrow> cdl_page_invocation option"
where "transform_page_inv invok \<equiv> case invok of
ARM_A.page_invocation.PageMap asid cap ct_slot entries \<Rightarrow>
Some (cdl_page_invocation.PageMap (transform_cap cap)
(case_sum (transform_pte \<circ> fst) (transform_pde \<circ> fst) entries)
(transform_cslot_ptr ct_slot)
(case_sum (\<lambda>pair. [ (transform_pt_slot_ref \<circ> hd \<circ> snd) pair])
(\<lambda>pair. [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) entries))
| ARM_A.page_invocation.PageUnmap (arch_cap.PageCap _ a _ sz asid) ref \<Rightarrow>
Some (cdl_page_invocation.PageUnmap (transform_mapping asid) a (transform_cslot_ptr ref) (pageBitsForSize sz))
| ARM_A.page_invocation.PageFlush flush _ _ _ _ _ \<Rightarrow>
Some (cdl_page_invocation.PageFlushCaches (flush_type_map flush))
| ARM_A.page_invocation.PageGetAddr base \<Rightarrow> Some (cdl_page_invocation.PageGetAddress)
| _ \<Rightarrow> None"
definition translate_arch_invocation :: "arch_invocation \<Rightarrow> cdl_invocation option"
where "translate_arch_invocation invo \<equiv> case invo of
arch_invocation.InvokePageTable oper \<Rightarrow> option_map cdl_invocation.InvokePageTable (transform_page_table_inv oper)
| arch_invocation.InvokePage oper \<Rightarrow> option_map cdl_invocation.InvokePage (transform_page_inv oper)
| arch_invocation.InvokePageDirectory oper \<Rightarrow> option_map cdl_invocation.InvokePageDirectory (transform_page_dir_inv oper)
| arch_invocation.InvokeASIDControl oper \<Rightarrow>
Some (case oper of ARM_A.MakePool frame slot parent base
\<Rightarrow> cdl_invocation.InvokeAsidControl
(cdl_asid_control_invocation.MakePool
(cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {})
(transform_cslot_ptr parent)
{frame..frame + 2 ^ pageBits - 1}
(transform_cslot_ptr slot)
(fst $ transform_asid base)))
| arch_invocation.InvokeASIDPool oper \<Rightarrow>
Some (case oper of ARM_A.Assign asid pool_ptr ct_slot
\<Rightarrow> cdl_invocation.InvokeAsidPool
(cdl_asid_pool_invocation.Assign
(transform_asid asid)
(transform_cslot_ptr ct_slot)
(pool_ptr, snd (transform_asid asid))))"
definition arch_invocation_relation :: "cdl_invocation \<Rightarrow> arch_invocation \<Rightarrow> bool"
where "arch_invocation_relation cdl_invok arch_invok \<equiv>
translate_arch_invocation arch_invok = Some cdl_invok"
lemma corres_symb_exec_in_gets:
"corres_underlying sr nf nf' r P P' f (gets g >>= j)
= (\<forall>v. corres_underlying sr nf nf' r P (P' and (\<lambda>s. g s = v)) f (j v))"
"corres_underlying sr nf nf' r P P' (gets g' >>= j') f'
= (\<forall>v. corres_underlying sr nf nf' r (P and (\<lambda>s. g' s = v)) P' (j' v) f')"
by (auto simp add: corres_underlying_def exec_gets split_def)
lemma select_ignored:
"select S >>= (\<lambda>_. f) = (if S = {} then select {} else f)"
apply (intro ext)
apply (simp add: select_def bind_def cart_singleton_image
image_image image_constant_conv)
done
lemma liftM_select:
"liftM f (select S) = select (f ` S)"
apply (rule ext)
apply (auto simp add: select_def bind_def liftM_def return_def split_def
cart_singleton_image image_image)
done
lemma gets_bind_alternative:
"((gets f >>= g) \<sqinter> h) = gets f >>= (\<lambda>x. g x \<sqinter> h)"
by (rule ext, simp add: alternative_def exec_gets)
lemma corres_from_rdonly:
assumes rdonly: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>"
assumes rv: "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk>
\<Longrightarrow> \<lbrace>(=) s'\<rbrace> g \<lbrace>\<lambda>rv s''. \<exists>rv' s'''. (rv', s''') \<in> fst (f s) \<and> r rv' rv\<rbrace>"
assumes nfl: "fl' \<Longrightarrow> no_fail P' g"
shows "corres_underlying sr fl fl' r P P' f g"
apply (clarsimp simp: corres_underlying_def no_failD[OF nfl])
apply (frule in_inv_by_hoareD[OF rdonly(2)], simp)
apply (frule(3) use_valid[OF _ rv], simp)
apply clarsimp
apply (frule in_inv_by_hoareD[OF rdonly(1)], simp)
apply fastforce
done
lemma get_pde_sp:
"\<lbrace>P\<rbrace> get_pde p \<lbrace>\<lambda>pde s. \<exists>pd. ko_at (ArchObj (arch_kernel_obj.PageDirectory pd)) (p && ~~ mask pd_bits) s
\<and> pde = (pd (ucast (p && mask pd_bits >> 2))) \<and> P s\<rbrace>"
apply (wp get_pde_wp)
apply auto
done
lemmas less_kernel_base_mapping_slots = less_kernel_base_mapping_slots_both[where x=0, simplified]
lemma dcorres_lookup_pt_slot:
"dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) \<top>
( valid_vspace_objs
and (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))
and valid_idle and pspace_aligned
and K (is_aligned pd 14 \<and> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
(cdl_lookup_pt_slot pd vptr) (lookup_pt_slot pd vptr)"
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:cdl_lookup_pt_slot_def
lookup_pt_slot_def liftE_bindE dcorres_lookup_pd_slot)
apply (rule corres_guard_imp)
apply (rule corres_split[OF dcorres_get_pde])
apply (rule_tac F = "case rv' of ARM_A.pde.PageTablePDE ptab x xa \<Rightarrow>
is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True"
in corres_gen_asm2)
apply (case_tac rv')
prefer 2
apply (clarsimp simp:transform_pde_def)
apply (rename_tac pt rights w)
apply (rule dcorres_returnOk)
apply (clarsimp simp:transform_pt_slot_ref_def
vaddr_segment_nonsense3 vaddr_segment_nonsense4)
apply (subst shiftl_shiftr_id)
apply simp
apply (rule le_less_trans)
apply (rule word_and_le1)
apply simp
apply simp
apply (simp add: transform_pde_def)+
apply (rule hoare_strengthen_post[where Q'="\<lambda>r. valid_pde r and pspace_aligned"] )
apply (wp get_pde_valid)
apply (clarsimp simp:valid_pde_def dest!:pt_aligned
split:ARM_A.pde.splits)
apply simp
apply auto
done
lemma lookup_pt_slot_aligned_6':
"\<lbrace> valid_vspace_objs
and (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))
and valid_idle and pspace_aligned
and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace>
lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv 6\<rbrace>, -"
apply (rule hoare_gen_asmE)
apply (simp add:lookup_pt_slot_def)
apply (wp|wpc)+
apply clarsimp
apply (rule hoare_strengthen_post[where Q'="\<lambda>r. valid_pde r and pspace_aligned"] )
apply wp
apply simp+
apply (clarsimp simp:valid_pde_def dest!:pt_aligned split:ARM_A.pde.splits)
apply (erule aligned_add_aligned)
apply (rule is_aligned_shiftl)
apply (rule is_aligned_andI1)
apply (rule is_aligned_shiftr)
apply simp+
done
lemma create_mapping_entries_dcorres:
assumes pdid: "pdid = pd_ptr"
and pd_aligned: "is_aligned pd_ptr pd_bits"
and vp_aligned: "vmsz_aligned vptr pgsz"
and kb: "vptr < kernel_base"
shows
"dcorres (dc \<oplus> (\<lambda>rv rv'. rv = case_sum (\<lambda>pair. [ (transform_pt_slot_ref \<circ> hd \<circ> snd) pair])
(\<lambda>pair. [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) rv'
\<and> case_sum (transform_pte \<circ> fst) (transform_pde \<circ> fst) rv'
= FrameCap False (ptrFromPAddr base)
vm_rights (pageBitsForSize pgsz) Fake None))
\<top>
(page_directory_at pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned
and (\<exists>\<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)))
(cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr)
(create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr)"
proof -
have aligned_4_hd:
"\<And>r :: word32. is_aligned r 6 \<Longrightarrow> hd (map (\<lambda>x. x + r) [0 , 4 .e. 0x3C]) = r"
apply (subgoal_tac "r \<le> r + 0x3C")
apply (clarsimp simp: upto_enum_step_def o_def | intro conjI)+
apply (subst hd_map)
apply (clarsimp simp:upto_enum_def)
apply (clarsimp simp:upto_enum_def hd_map)
apply (rule is_aligned_no_wrap')
apply simp
apply simp
done
show ?thesis using pdid vp_aligned
apply hypsubst_thin
proof (induct pgsz)
case ARMSmallPage
show ?case using ARMSmallPage.prems
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (rule dcorres_injection_handler_rhs)
apply (simp add:liftE_bindE cdl_page_mapping_entries_def)
apply (rule corres_dummy_returnOk_r)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
apply (rule dcorres_lookup_pt_slot)
apply (rule dcorres_returnOk; simp)
apply wp+
apply simp
apply (clarsimp simp:
dest!:page_directory_at_aligned_pd_bits )
apply (frule less_kernel_base_mapping_slots_both[OF kb,where x = 0])
apply simp
apply (simp add:pageBits_def pd_bits_def)
done
next
case ARMLargePage
show ?case using ARMLargePage.prems
apply (simp add: liftME_def[symmetric] o_def transform_pte_def pd_bits_def pageBits_def
lookup_error_injection dc_def[symmetric])
apply (rule dcorres_injection_handler_rhs)
apply (simp add:liftE_bindE cdl_page_mapping_entries_def largePagePTE_offsets_def)
apply (rule corres_dummy_returnOk_r)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
apply (rule dcorres_lookup_pt_slot)
apply (rule_tac F = "is_aligned rv' 6" in corres_gen_asm2)
apply (rule dcorres_returnOk)
apply (subst aligned_4_hd)
apply clarsimp
apply (clarsimp)
apply (wpsimp wp: lookup_pt_slot_aligned_6')+
apply (clarsimp dest!:page_directory_at_aligned_pd_bits)
apply (frule less_kernel_base_mapping_slots_both[OF kb,where x = 0])
apply simp
apply (clarsimp simp:pageBits_def pd_bits_def vmsz_aligned_def)
apply (rule_tac x=ref in exI, simp)
done
next
case ARMSection
show ?case using ARMSection.prems
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (simp add:liftE_bindE cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac F = "is_aligned pd_ptr 14" in corres_gen_asm2)
apply (rule dcorres_returnOk)
apply (clarsimp simp:transform_pde_def vmsz_aligned_def)
apply (simp add: dcorres_lookup_pd_slot)
apply simp
apply (clarsimp simp: pd_bits_def pageBits_def
dest!:page_directory_at_aligned_pd_bits )
done
next
case ARMSuperSection
show ?case using ARMSuperSection.prems
using pd_aligned
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (simp add:liftE_bindE cdl_page_mapping_entries_def superSectionPDE_offsets_def)
apply (rule corres_guard_imp)
apply (rule_tac F = "is_aligned pd_ptr 14" in corres_gen_asm2)
apply (rule dcorres_returnOk)
apply (clarsimp simp:transform_pde_def vmsz_aligned_def)
apply (subst aligned_4_hd)
apply (rule lookup_pd_slot_aligned_6)
apply (simp add:vmsz_aligned_def)+
apply (simp add: dcorres_lookup_pd_slot)
apply simp
apply (clarsimp simp: pd_bits_def pageBits_def
dest!:page_directory_at_aligned_pd_bits )
done
qed
qed
lemma create_mapping_entries_dcorres_select:
assumes pdid: "pdid = pd_ptr"
and pd_aligned: "is_aligned pd_ptr pd_bits"
and vp_aligned: "vmsz_aligned vptr pgsz"
and kb: "vptr < kernel_base"
shows
"dcorres (dc \<oplus> (\<lambda>rv rv'. rv = case_sum (\<lambda>pair. [ (transform_pt_slot_ref \<circ> hd \<circ> snd) pair])
(\<lambda>pair. [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) rv'
\<and> case_sum (transform_pte \<circ> fst) (transform_pde \<circ> fst) rv'
= FrameCap False (ptrFromPAddr base)
vm_rights (pageBitsForSize pgsz) Fake None))
(\<lambda>s. frslots = all_pd_pt_slots pd pdid s
\<and> cdl_objects s pdid = Some pd)
(page_directory_at pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned
and (\<exists>\<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)))
(liftE (select {M. set M \<subseteq> frslots \<and> distinct M}) \<sqinter> Monads_D.throw)
(create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr)"
proof -
have lookup_pd_slot_offs_times_4_mask_2[simp]:
"\<And>x. lookup_pd_slot pd_ptr vptr + of_nat x * 4 && mask 2 = 0"
apply (subst is_aligned_mask[symmetric])
apply (rule aligned_add_aligned[where n=2], simp_all add: word_bits_conv)
apply (simp add: lookup_pd_slot_def)
apply (rule aligned_add_aligned[OF pd_aligned],
simp_all add: pd_bits_def pageBits_def word_bits_conv)
apply (simp_all add: is_aligned_shiftl word_shift_by_2)
done
have inj_on_pd:
"inj_on (\<lambda>x. transform_pd_slot_ref (lookup_pd_slot pd_ptr vptr + toEnum x * 4)) {0 ..< 16}"
apply (rule inj_onI, clarsimp simp: transform_pd_slot_ref_def)
apply (drule bits_low_high_eq[rotated])
apply (simp add: mask_twice pd_bits_def pageBits_def)
apply (drule(1) mask_eqI[rotated])
apply (simp add: word_shift_by_2)
apply (rule ccontr, erule(3) of_nat_shift_distinct_helper)
apply (simp_all add: word_bits_conv)
done
have map_includedI:
"\<And>S g xs. \<lbrakk>set (map g xs) \<subseteq> S;xs \<noteq> []\<rbrakk> \<Longrightarrow> g (hd xs) \<in> S"
by (clarsimp simp:hd_map_simp neq_Nil_conv)
show ?thesis using pdid vp_aligned
apply clarsimp
proof (induct pgsz)
case ARMSmallPage
show ?case using ARMSmallPage.prems
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (rule dcorres_injection_handler_rhs)
apply (simp add: lookup_pt_slot_def liftE_bindE)
apply (rule corres_symb_exec_r[OF _ get_pde_sp get_pde_inv], simp_all)[1]
apply (clarsimp simp add: corres_alternate2 split: ARM_A.pde.split)
apply (rule corres_alternate1)
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (simp add: returnOk_def in_monad select_def, wp)
apply (clarsimp simp: transform_pt_slot_ref_def all_pd_pt_slots_def
opt_object_page_directory
obj_at_def object_slots_def transform_page_directory_contents_def
unat_map_def kernel_pde_mask_def lookup_pd_slot_pd
pd_aligned
dest!: a_type_pdD
del: disjCI)
apply (drule valid_vspace_objsD, simp add: obj_at_def, simp+)
apply (cut_tac less_kernel_base_mapping_slots[OF kb pd_aligned])
apply (drule_tac x="ucast (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)" in bspec)
apply simp
apply (drule_tac t="pda v" for v in sym, simp)
apply (clarsimp simp: obj_at_def del: disjCI)
apply (frule_tac p="ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (rule disjI2, rule conjI)
apply (rule_tac x="unat (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)"
in exI)
apply (simp add: transform_pde_def ucast_nat_def)
apply (subst is_aligned_add_helper, simp add: pt_bits_def pageBits_def)
apply (rule shiftl_less_t2n)
apply (rule order_le_less_trans, rule word_and_le1, simp add: pt_bits_def pageBits_def)
apply (simp add: pt_bits_def pageBits_def)
apply simp
apply (simp add: kernel_mapping_slots_def)
apply (subst is_aligned_add_helper, simp add: pt_bits_def pageBits_def)
apply (rule shiftl_less_t2n)
apply (rule order_le_less_trans, rule word_and_le1, simp add: pt_bits_def pageBits_def)
apply (simp add: pt_bits_def pageBits_def)
apply (simp add: dom_def transform_def transform_objects_def
restrict_map_def map_add_def)
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
done
next
case ARMLargePage
show ?case using ARMLargePage.prems
apply (simp add: liftME_def[symmetric] o_def transform_pte_def largePagePTE_offsets_def
lookup_error_injection dc_def[symmetric])
apply (rule dcorres_injection_handler_rhs)
apply (simp add: lookup_pt_slot_def liftE_bindE)
apply (rule corres_symb_exec_r[OF _ get_pde_sp get_pde_inv], simp_all)[1]
apply (clarsimp simp add: corres_alternate2 split: ARM_A.pde.split)
apply (rename_tac word1 set word2)
apply (rule corres_alternate1)
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (simp add: returnOk_def in_monad select_def, wp)
apply (clarsimp simp: pd_aligned obj_at_def lookup_pd_slot_pd
a_type_simps)
apply (drule valid_vspace_objsD, simp add: obj_at_def, simp+)
apply (cut_tac less_kernel_base_mapping_slots[OF kb pd_aligned])
apply (drule_tac x="ucast (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)" in bspec)
apply simp
apply (drule_tac t="pda v" for v in sym, simp)
apply (clarsimp simp: obj_at_def del: disjCI)
apply (frule_tac p="ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (rule map_includedI)
apply (clarsimp simp: transform_pt_slot_ref_def all_pd_pt_slots_def
opt_object_page_directory
object_slots_def transform_page_directory_contents_def
unat_map_def kernel_pde_mask_def
del: disjCI UnCI)
apply (subgoal_tac "x + (ptrFromPAddr word1 + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr word1")
apply (rule disjI2, rule conjI)
apply (rule_tac x="unat (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)"
in exI)
apply (simp add: transform_pde_def ucast_nat_def)
apply (simp add: kernel_mapping_slots_def)
apply (simp add: dom_def transform_def transform_objects_def
restrict_map_def)
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
apply (clarsimp simp: upto_enum_step_def pt_bits_def pageBits_def
split: if_split_asm)
apply (subst add.commute, subst add.assoc, subst is_aligned_add_helper, assumption)
apply (simp only: word_shift_by_2 word_shiftl_add_distrib[symmetric])
apply (rule shiftl_less_t2n)
apply (rule is_aligned_add_less_t2n[where n=4])
apply (rule is_aligned_andI1)
apply (rule is_aligned_shiftr)
apply (simp add: vmsz_aligned_def)
apply (simp add: word_leq_minus_one_le)
apply simp
apply (rule order_le_less_trans, rule word_and_le1, simp)
apply simp
apply simp
apply (simp add: upto_enum_step_def not_less upto_enum_def)
done
next
case ARMSection
show ?case using ARMSection.prems
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (rule corres_alternate1)
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (simp add: returnOk_def in_monad select_def, wp)
apply (clarsimp simp: transform_pde_def obj_at_def
opt_object_page_directory
dest!: a_type_pdD)
apply (simp add: transform_pd_slot_ref_def lookup_pd_slot_def
all_pd_pt_slots_def object_slots_def
transform_page_directory_contents_def
dom_def unat_map_def)
done
next
case ARMSuperSection
show ?case using ARMSuperSection.prems
using pd_aligned
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (rule corres_alternate1)
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (simp add: returnOk_def in_monad select_def, wp)
apply (clarsimp simp: transform_pde_def obj_at_def
opt_object_page_directory
dest!: a_type_pdD)
apply (rule map_includedI)
apply clarsimp
apply (clarsimp simp: all_pd_pt_slots_def transform_pd_slot_ref_def
object_slots_def transform_page_directory_contents_def
dom_def unat_map_def)
apply (simp add: not_less upto_enum_step_def upto_enum_def superSectionPDE_offsets_def)
done
qed
qed
schematic_goal get_master_pde_invalid_sp:
"\<lbrace>P\<rbrace> get_master_pde p
\<lbrace>\<lambda>pde s. pde = ARM_A.pde.InvalidPDE \<longrightarrow>
(\<exists>pd. ko_at (ArchObj (arch_kernel_obj.PageDirectory pd)) (?p && ~~ mask pd_bits) s \<and>
pde = pd (ucast (?p && mask pd_bits >> 2))) \<and> P s\<rbrace>"
apply (simp add:get_master_pde_def)
apply (wp get_pde_wp |wpc)+
apply (clarsimp simp:obj_at_def)
apply (auto simp add:mask_lower_twice pd_bits_def pageBits_def)
done
lemma shiftl_mod:
"\<lbrakk> n < 32; (x :: word32) < 2 ^ (32 - n) \<rbrakk> \<Longrightarrow> unat (x << n) mod 2 ^ n = 0"
apply (subst shiftl_t2n)
apply (clarsimp simp:unat_word_ariths)
apply (subgoal_tac "2 ^ n * unat x < 2 ^ 32")
apply (clarsimp)
apply (subst (asm) word_unat_power)
apply (drule unat_less_helper)
apply (rule_tac y="2^n * 2 ^(32-n)" in less_le_trans)
apply simp
apply (simp add:power_add[symmetric])
done
definition
select_ret_or_throw :: "'a set \<Rightarrow> 'x set \<Rightarrow> ('s, ('x + 'a)) nondet_monad"
where
"select_ret_or_throw S X = alternative (select S >>= returnOk) (select X >>= throwError)"
lemma to_select_ret_or_throw:
"returnOk x = select_ret_or_throw {x} {}"
"throwError e = select_ret_or_throw {} {e}"
"alternative (select_ret_or_throw S X) (select_ret_or_throw S' X')
= select_ret_or_throw (S \<union> S') (X \<union> X')"
apply (simp_all add: select_ret_or_throw_def alternative_def returnOk_def return_def
select_def bind_def throwError_def)
apply (simp add: Sigma_def return_def Un_ac)
done
lemma whenE_to_select_ret_or_throw:
"whenE P (select_ret_or_throw S X)
= select_ret_or_throw ({x. P \<longrightarrow> x \<in> S}) ({x. P \<and> x \<in> X})"
apply (simp add: whenE_def to_select_ret_or_throw UNIV_unit)
apply (strengthen arg_cong2[where f=select_ret_or_throw])
apply (simp add: set_eq_iff)
done
lemma select_ret_or_throw_twice:
"(do _ \<leftarrow> select_ret_or_throw S X; select_ret_or_throw S X od)
= select_ret_or_throw S X"
apply (simp add: select_ret_or_throw_def alternative_def returnOk_def return_def
select_def bind_def throwError_def Sigma_def)
apply (rule ext, auto)
done
lemma select_ret_or_throw_twiceE:
"(doE _ \<leftarrow> select_ret_or_throw S X; select_ret_or_throw S X odE)
= select_ret_or_throw S X"
apply (simp add: select_ret_or_throw_def alternative_def returnOk_def return_def
select_def bind_def throwError_def Sigma_def
bindE_def)
apply (rule ext, auto simp: throwError_def return_def)
done
crunch select_ret_or_throw
for inv[wp]: "P"
lemma corres_initial_bindE_rdonly_select_ret_or_throw:
assumes y: "\<And>rv'. corres_underlying sr nf nf' (e \<oplus> r) P P' (select_ret_or_throw S X) (d rv')"
assumes x: "corres_underlying sr nf nf' (e \<oplus> dc) P P' (select_ret_or_throw S X) c"
assumes z: "\<lbrace>P'\<rbrace> c \<lbrace>\<lambda>_. P'\<rbrace>,-"
shows "corres_underlying sr nf nf' (e \<oplus> r) P P' (select_ret_or_throw S X) (c >>=E (\<lambda>rv'. d rv'))"
apply (subst select_ret_or_throw_twiceE[symmetric])
apply (rule corres_initial_splitE[OF x y])
apply wp
apply (wp z)
done
lemma corres_select_ret_or_throw:
"\<forall>v \<in> S'. \<exists>v' \<in> S. r v' v
\<Longrightarrow> \<forall>x \<in> X'. \<exists>x' \<in> X. e x' x
\<Longrightarrow> corres_underlying sr nf nf' (e \<oplus> r) \<top> \<top>
(select_ret_or_throw S X) (select_ret_or_throw S' X')"
apply (simp add: select_ret_or_throw_def)
apply (rule corres_alternate_match)
apply (simp add: returnOk_def liftM_def[symmetric] o_def)
apply (rule corres_select, simp)
apply (simp add: throwError_def liftM_def[symmetric] o_def)
apply (rule corres_select, simp)
done
(*
* Decoding Arch invocations is equivalent.
*)
lemma decode_invocation_archcap_corres:
notes label_split_asm = invocation_label.split_asm gen_invocation_labels.split_asm
arch_invocation_label.split_asm
shows
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.ArchObjectCap x \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> (\<lambda>rv rv'. \<exists>ai. rv' = Invocations_A.InvokeArchObject ai
\<and> arch_invocation_relation rv ai))
\<top> (invs and valid_etcbs and valid_cap invoked_cap'
and (\<lambda>s. \<forall>x \<in> set (map fst excaps'). s \<turnstile> x)
and (\<lambda>s. \<forall>x \<in> set excaps'. cte_wp_at ((=) (fst x)) (snd x) s))
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (rule_tac F="\<forall>x \<in> set (map fst excaps'). cap_aligned x" in corres_req)
apply (fastforce simp add: valid_cap_aligned)
apply clarsimp
proof (induct x)
case (ASIDPoolCap ap_ptr asid)
thus ?case
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
split del: if_split)
apply (clarsimp simp: get_asid_pool_intent_def transform_intent_def
map_option_Some_eq2 throw_opt_def
decode_asid_pool_invocation_def
split del: if_split split: label_split_asm list.split_asm)
apply (simp add: split_beta corres_alternate2
liftE_bindE corres_symb_exec_in_gets
corres_whenE_throwError_split_rhs
split: cap.split arch_cap.split option.split)
apply (clarsimp simp: get_index_def transform_cap_list_def
throw_on_none_def split_beta bindE_assoc
dc_def[symmetric])
apply (rule corres_guard_imp)
apply (rule corres_symb_exec_r)
apply (clarsimp simp: corres_whenE_throwError_split_rhs
corres_alternate2)
apply (rule corres_alternate1)
apply (simp add: select_ext_def bind_assoc)
apply (rule dcorres_symb_exec_r)
apply (rule corres_assert_rhs)
apply (rule_tac x="unat (free_asid_pool_select pool asid)" in select_pick_corres_asm)
apply (rule CollectI)
apply (elim conjE)
apply (rule le_p2_minus_1)
apply (rule unat_le_helper)
apply (simp add: p2_low_bits_max)
apply (rule corres_returnOk[where P=\<top> and P'="\<lambda>rv. is_aligned asid asid_low_bits"])
apply (clarsimp simp:arch_invocation_relation_def translate_arch_invocation_def
transform_asid_def asid_high_bits_of_def shiftr_irrelevant
up_ucast_inj_eq)
apply (erule impE)
apply (rule arg_cong[where f=ucast])
apply (subst shiftr_irrelevant)
apply (rule word_leq_minus_one_le)
apply (simp add: asid_low_bits_def)
apply (subst ucast_le_migrate)
apply (simp add: asid_low_bits_def word_size)
apply (simp add: word_size)
apply (subst ucast_down_minus)
apply (simp add: is_down_def target_size_def source_size_def word_size)
apply (simp add: asid_low_bits_def)
apply simp
apply simp
apply (simp add: ucast_ucast_add)
apply (erule_tac P="ucast asid = 0" in notE)
apply (rule ucast_up_inj[where 'b=32])
apply (simp add: ucast_ucast_mask is_aligned_mask asid_low_bits_def)
apply simp
apply (wp | simp add:valid_cap_def split del: if_split)+
done
next
case ASIDControlCap
thus ?case
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
bindE_assoc
split del: if_split)
apply (clarsimp simp: get_asid_control_intent_def transform_intent_def
map_option_Some_eq2 throw_opt_def
decode_asid_control_invocation_def
transform_cnode_index_and_depth_def
split del: if_split split: label_split_asm list.split_asm)
apply (simp add: split_beta corres_alternate2
liftE_bindE corres_symb_exec_in_gets
corres_whenE_throwError_split_rhs
transform_cnode_index_and_depth_def
select_ignored
split: cap.split arch_cap.split option.split)
apply (clarsimp simp: get_index_def transform_cap_list_def
throw_on_none_def split_beta bindE_assoc
dc_def[symmetric])
apply (intro conjI impI allI)
apply (rule corres_symb_exec_r[OF dcorres_alternative_throw],
(wp | simp)+)
defer
apply ((rule corres_symb_exec_r[OF dcorres_alternative_throw],
(wp | simp)+)+)[11]
apply (rename_tac dev ptr sz v)
apply (case_tac dev)
apply simp
apply (rule corres_alternate2)
apply (rule corres_guard_imp)
apply (rule corres_symb_exec_r)
apply (rule dcorres_throw)
apply ((wp|simp)+)[5]
apply clarsimp
apply (rule conjI[rotated])
apply clarsimp
apply (rule corres_alternate2)
apply (rule corres_guard_imp)
apply (rule corres_symb_exec_r)
apply (rule dcorres_throw)
apply ((wp|simp)+)[5]
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_alternate1)
apply (clarsimp simp: select_ext_def bind_assoc)
apply (rule dcorres_symb_exec_r)
apply (rule corres_assert_rhs)
apply (rule_tac x="unat (free_asid_select v)" in select_pick_corres_asm)
apply (rule CollectI)
apply (elim conjE)
apply (rule le_p2_minus_1)
apply (rule unat_le_helper)
apply simp
apply (simp add:bindE_assoc)
apply (rule corres_splitEE[OF dcorres_ensure_no_children[where P="(\<noteq>) cap.NullCap"]])
apply (rule corres_splitEE)
apply (rule lookup_slot_for_cnode_op_corres; simp)
apply (simp, elim conjE)
apply (rule corres_splitEE[OF dcorres_ensure_empty])
apply (rule corres_returnOk[where P=\<top> and P'=\<top>])
apply (simp add:transform_def arch_invocation_relation_def
translate_arch_invocation_def)
apply (simp add:transform_asid_def unat_ucast asid_high_bits_def asid_low_bits_def
unat_lt2p[where 'a=8, simplified])
apply (thin_tac "free_asid_select v \<notin> dom v")
apply clarsimp
apply (subgoal_tac "unat ((ucast (free_asid_select v) :: word32) << 10) mod 1024=0")
apply (simp add: asid_high_bits_of_shift[simplified asid_low_bits_def[simplified]])
apply (rule shiftl_mod[where n=10, simplified])
apply (cut_tac x="free_asid_select v" and 'a=32 in ucast_less)
apply simp
apply (rule less_trans)
apply simp
apply simp
apply (wp lsfco_not_idle select_inv | simp)+
apply (simp add: cte_wp_at_caps_of_state neq_Nil_conv invs_mdb_cte mdb_cte_at_rewrite)
apply auto
done
next
case (PageCap dev base rights pgsz asid)
thus ?case
supply option.case_cong[cong] if_cong[cong]
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
split del: if_split)
apply (clarsimp simp: get_page_intent_def transform_intent_def
map_option_Some_eq2 throw_opt_def
decode_page_invocation_def
transform_intent_page_map_def
split del: if_split split: label_split_asm list.split_asm,
simp_all add: split_beta corres_alternate2
liftE_bindE corres_symb_exec_in_gets
corres_whenE_throwError_split_rhs
transform_cnode_index_and_depth_def
select_ignored throw_on_none_def
get_index_def transform_cap_list_def
dc_def[symmetric]
split: cap.split arch_cap.split option.split)
(* 45 subgoals, most are irrelevant invocations *)
apply (clarsimp simp: gets_bind_alternative gets_the_def bind_assoc
corres_symb_exec_in_gets assert_opt_def)
apply ((clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle
label_to_flush_type_def isPageFlushLabel_def
dest!: a_type_pdD)+)[35]
(* 10 subgoals *)
(* PageMap *)
apply (clarsimp simp: transform_mapping_def)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def opt_object_page_directory
invs_valid_idle label_to_flush_type_def isPageFlushLabel_def
dest!: a_type_pdD)
apply (intro conjI; clarsimp)
(* Unmapped *)
apply (rule_tac
r'=dc and P'="I" and Q'="\<lambda>rv. I and (\<exists>\<rhd> (lookup_pd_slot rv x21 && ~~ mask pd_bits))"
for I
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp+ | simp)+
apply (rule hoare_strengthen_post, rule hoare_TrueI)
apply (rename_tac rv s)
apply (case_tac rv, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
apply (rule corres_alternative_throw_splitE)
apply (rule corres_alternate1)
apply (rule corres_guard_imp,
rule create_mapping_entries_dcorres[OF refl])
apply (clarsimp simp: neq_Nil_conv cap_aligned_def
pd_bits_def pageBits_def)
apply (simp add: vmsz_aligned_def)
apply (simp only: linorder_not_le, erule order_le_less_trans[rotated])
apply simp
apply simp
apply (fastforce simp: neq_Nil_conv valid_cap_simps dest!: page_directory_at_rev)
apply (rule corres_from_rdonly[where P=\<top> and P'=\<top>], simp_all)[1]
apply (wp+ | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp+ | simp)+
apply (clarsimp simp add: in_monad conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
update_mapping_cap_status_def Types_D.cap_rights_def
mask_vm_rights_def transform_mapping_def)
apply wp+
apply simp
apply (rule hoare_pre, wp, auto)[1]
apply ((wpsimp simp: whenE_def split_del: if_split)+)[2]
(* Mapped *)
apply (clarsimp simp: bindE_assoc)
apply (clarsimp simp: corres_whenE_throwError_split_rhs corres_alternate2)
apply (rule_tac
r'=dc and P'="I" and Q'="\<lambda>rv. I and (\<exists>\<rhd> (lookup_pd_slot rv x21 && ~~ mask pd_bits))"
for I
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp+ | simp)+
apply (rule hoare_strengthen_post, rule hoare_TrueI)
apply (rename_tac rv s)
apply (case_tac rv, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
apply (rule corres_alternative_throw_splitE)
apply (rule corres_alternate1)
apply (rule corres_guard_imp[where P=P and Q=P and Q'="P' and _" and P'=P' for P P'])
apply (rule_tac F="x21 < kernel_base" in corres_gen_asm2)
apply (rule corres_guard_imp,
rule create_mapping_entries_dcorres[OF refl])
apply (clarsimp simp: neq_Nil_conv cap_aligned_def
pd_bits_def pageBits_def)
apply (simp add: vmsz_aligned_def)
apply simp
apply simp
apply simp
apply (fastforce simp: neq_Nil_conv valid_cap_simps dest!:page_directory_at_rev)
apply presburger
apply blast
apply (rule corres_from_rdonly[where P=\<top> and P'=\<top>], simp_all)[1]
apply (wp+ | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp+ | simp)+
apply (clarsimp simp add: in_monad conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
update_mapping_cap_status_def Types_D.cap_rights_def
mask_vm_rights_def transform_mapping_def)
apply wp+
apply (simp)
apply (rule hoare_pre, wp, auto)[1]
apply (wp | simp add: whenE_def split del: if_split)+
(* PageUnmap *)
apply (rule corres_alternate1)
apply (simp add: returnOk_def arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def)
(* PageClean *)
apply (clarsimp)
apply (rule corres_from_rdonly)
apply (wp, clarsimp)
apply (simp only: Let_unfold, (wp whenE_inv)+, clarsimp)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wpsimp simp: Let_unfold arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def)+
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply safe
apply blast
apply (metis flush.exhaust)
(* PageInvalidate *)
apply (rule corres_from_rdonly)
apply (wp, clarsimp)
apply (simp only: Let_unfold, (wp whenE_inv)+, clarsimp)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wpsimp simp: Let_unfold arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def)+
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply safe
apply blast
apply (metis flush.exhaust)
(* PageCleanInvalidate *)
apply (rule corres_from_rdonly)
apply (wp, clarsimp)
apply (simp only: Let_unfold, (wp whenE_inv)+, clarsimp)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wpsimp simp: Let_unfold arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def)+
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply safe
apply blast
apply (metis flush.exhaust)
(* PageUnify *)
apply (rule corres_from_rdonly)
apply (wp, clarsimp)
apply (simp only: Let_unfold, (wp whenE_inv)+, clarsimp)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wpsimp simp: Let_unfold arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def)+
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply safe
apply blast
apply (metis flush.exhaust)
(* PageGetAddress *)
apply (clarsimp simp: isPageFlushLabel_def)+
apply (rule corres_returnOk,clarsimp simp:arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def |
clarsimp simp: isPageFlushLabel_def)+
done
next
case (PageTableCap ptr asid)
thus ?case
supply if_cong[cong]
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
split del: if_split)
apply (clarsimp simp: get_page_table_intent_def transform_intent_def
map_option_Some_eq2 throw_opt_def cdl_get_pt_mapped_addr_def
decode_page_table_invocation_def
transform_intent_page_table_map_def
split del: if_split
split: label_split_asm list.split_asm)
apply (simp add: throw_on_none_def transform_cap_list_def
get_index_def split_beta alternative_refl
transform_mapping_def corres_whenE_throwError_split_rhs corres_alternate2
split: cap.split arch_cap.split option.split cdl_frame_cap_type.splits)
apply (clarsimp simp: dc_def[symmetric] liftE_bindE
gets_the_def bind_assoc transform_mapping_def
corres_symb_exec_in_gets gets_bind_alternative)
apply (rule_tac r'=dc and P'="I" and Q'="\<lambda>rv. I and (\<exists>\<rhd> (lookup_pd_slot rv ab && ~~ mask pd_bits))"
for I in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_TrueI)
apply (rename_tac rv s)
apply (case_tac rv, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply clarsimp
apply (rule corres_symb_exec_r
[OF _ get_master_pde_invalid_sp get_master_pde_inv],simp_all)[1]
apply (clarsimp simp add: corres_whenE_throwError_split_rhs
corres_alternate2)
apply (rule corres_alternate1)
apply (rule corres_from_rdonly,simp_all)[1]
apply (wp | simp)+
apply (simp add: returnOk_def, wp)
apply (clarsimp simp: in_monad select_def arch_invocation_relation_def
translate_arch_invocation_def transform_page_table_inv_def
addrFromPPtr_def is_cap_simps cap_object_def
cdl_lookup_pd_slot_def cap_has_object_def
neq_Nil_conv cap_aligned_def)
apply (simp add: make_arch_duplicate_def transform_pd_slot_ref_def)
apply (clarsimp simp add: free_pd_slots_def opt_object_page_directory
obj_at_def invs_valid_idle pd_shifting
object_slots_def transform_page_directory_contents_def
unat_map_def kernel_pde_mask_def
transform_pde_def transform_mapping_def)
apply (simp add: pd_shifting_dual ucast_nat_def shiftr_20_less triple_shift_fun
le_shiftr linorder_not_le)
apply (rule hoare_pre, wp, auto)[1]
apply (wp weak_if_wp | simp)+
apply (clarsimp simp: is_final_cap'_def
is_final_cap_def split:list.splits)
apply (simp add: liftE_bindE is_final_cap_def corres_symb_exec_in_gets
unlessE_whenE corres_whenE_throwError_split_rhs
corres_alternate2)
apply (rule corres_alternate1, simp add: returnOk_def)
apply (clarsimp simp: arch_invocation_relation_def translate_arch_invocation_def get_pt_mapped_addr_def
transform_page_table_inv_def is_cap_simps)
done
next
case (PageDirectoryCap pd_ptr asid)
thus ?case
(* abandon hope, all who enter here *)
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
get_page_directory_intent_def transform_intent_def
isPDFlushLabel_def
split del: if_split)
apply (clarsimp simp: get_page_directory_intent_def transform_intent_def
map_option_Some_eq2 throw_opt_def decode_page_directory_invocation_def
split: label_split_asm cdl_intent.splits
InvocationLabels_H.invocation_label.splits arch_invocation_label.splits)
apply (simp_all add: Let_def)
apply (all \<open>(intro conjI impI allI)\<close>)
apply (all \<open>(simp add: to_select_ret_or_throw whenE_to_select_ret_or_throw split_def
del: Collect_const;
intro corres_initial_bindE_rdonly_select_ret_or_throw
corres_select_ret_or_throw[THEN corres_guard_imp];
(wpsimp simp: if_apply_def2 ex_disj_distrib)?)?\<close>)
(* 20-odd subgoals, not going to indent *)
apply (all \<open>(simp split: option.split)?;