-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDpolicy.thy
1056 lines (972 loc) · 47.1 KB
/
Dpolicy.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, NICTA
*
* 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(NICTA_GPL)
*)
theory Dpolicy
imports
Access
"../drefine/Refine_D"
"../drefine/Include_D"
begin
definition
cdl_cap_auth_conferred :: "cdl_cap \<Rightarrow> auth set"
where
"cdl_cap_auth_conferred cap \<equiv>
case cap of
cdl_cap.NullCap \<Rightarrow> {}
| cdl_cap.UntypedCap refs frange \<Rightarrow> {Control}
| cdl_cap.EndpointCap oref badge r \<Rightarrow>
cap_rights_to_auth r True
| cdl_cap.AsyncEndpointCap oref badge r \<Rightarrow>
cap_rights_to_auth (r - {AllowGrant}) False
| cdl_cap.ReplyCap oref \<Rightarrow> {Control}
| cdl_cap.MasterReplyCap oref \<Rightarrow> {Control}
| cdl_cap.CNodeCap oref bits guard sz \<Rightarrow> {Control}
| cdl_cap.TcbCap obj_ref \<Rightarrow> {Control}
| cdl_cap.DomainCap \<Rightarrow> {Control}
| cdl_cap.PendingSyncSendCap oref badge call grant fault \<Rightarrow>
{SyncSend} \<union> (if grant then {Access.Grant} else {})
| cdl_cap.PendingSyncRecvCap oref fault \<Rightarrow> if fault then {} else {Receive}
| cdl_cap.PendingAsyncRecvCap oref \<Rightarrow> {Receive}
| cdl_cap.RestartCap \<Rightarrow> {}
| cdl_cap.IrqControlCap \<Rightarrow> {Control}
| cdl_cap.IrqHandlerCap irq \<Rightarrow> {Control}
| cdl_cap.FrameCap oref r sz is_real asid \<Rightarrow> vspace_cap_rights_to_auth r
| cdl_cap.PageTableCap oref is_real asid\<Rightarrow> {Control}
| cdl_cap.PageDirectoryCap oref is_real asid \<Rightarrow> {Control}
| cdl_cap.AsidControlCap \<Rightarrow> {Control}
| cdl_cap.AsidPoolCap oref asid \<Rightarrow> {Control}
| cdl_cap.ZombieCap ptr \<Rightarrow> {Control}
| _ \<Rightarrow> {}"
fun
cdl_obj_refs :: "cdl_cap \<Rightarrow> obj_ref set"
where
"cdl_obj_refs cdl_cap.NullCap = {}"
| "cdl_obj_refs (cdl_cap.UntypedCap rs frange) = rs"
| "cdl_obj_refs (cdl_cap.EndpointCap r b cr) = {r}"
| "cdl_obj_refs (cdl_cap.AsyncEndpointCap r b cr) = {r}"
| "cdl_obj_refs (cdl_cap.ReplyCap r) = {r}"
| "cdl_obj_refs (cdl_cap.MasterReplyCap r) = {r}"
| "cdl_obj_refs (cdl_cap.CNodeCap r guard bits sz) = {r}"
| "cdl_obj_refs (cdl_cap.TcbCap r) = {r}"
| "cdl_obj_refs (cdl_cap.DomainCap) = UNIV"
| "cdl_obj_refs (cdl_cap.PendingSyncSendCap r badge call guard fault) = {r}"
| "cdl_obj_refs (cdl_cap.PendingSyncRecvCap r fault) = {r}"
| "cdl_obj_refs (cdl_cap.PendingAsyncRecvCap r) = {r}"
| "cdl_obj_refs cdl_cap.RestartCap = {}"
| "cdl_obj_refs cdl_cap.IrqControlCap = {}"
| "cdl_obj_refs (cdl_cap.IrqHandlerCap irq) = {}"
| "cdl_obj_refs (cdl_cap.FrameCap x rs sz is_real asid) = ptr_range x sz"
| "cdl_obj_refs (cdl_cap.PageDirectoryCap x is_real asid) = {x}"
| "cdl_obj_refs (cdl_cap.PageTableCap x is_real asid) = {x}"
| "cdl_obj_refs (cdl_cap.AsidPoolCap p asid) = {p}"
| "cdl_obj_refs cdl_cap.AsidControlCap = {}"
| "cdl_obj_refs (cdl_cap.ZombieCap ptr) = {ptr}"
| "cdl_obj_refs _ = {}"
inductive_set
cdl_state_bits_to_policy for caps cdt
where
csbta_caps: "\<lbrakk> caps ptr = Some cap; oref \<in> cdl_obj_refs cap;
auth \<in> cdl_cap_auth_conferred cap \<rbrakk>
\<Longrightarrow> (fst ptr, auth, oref) \<in> cdl_state_bits_to_policy caps cdt"
| csbta_cdt: "\<lbrakk> cdt slot' = Some slot \<rbrakk>
\<Longrightarrow> (fst slot, Control, fst slot') \<in> cdl_state_bits_to_policy caps cdt"
definition
"cdl_state_objs_to_policy s = cdl_state_bits_to_policy (\<lambda>ref. opt_cap ref s)
(cdl_cdt s)"
fun
cdl_cap_irqs_controlled :: "cdl_cap \<Rightarrow> cdl_irq set"
where
"cdl_cap_irqs_controlled cdl_cap.IrqControlCap = UNIV"
| "cdl_cap_irqs_controlled (cdl_cap.IrqHandlerCap irq) = {irq}"
| "cdl_cap_irqs_controlled _ = {}"
inductive_set
cdl_state_irqs_to_policy_aux for aag caps
where
csita_controlled: "\<lbrakk> caps ref = Some cap; irq \<in> cdl_cap_irqs_controlled cap \<rbrakk>
\<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in>
cdl_state_irqs_to_policy_aux aag caps"
abbreviation
"cdl_state_irqs_to_policy aag s \<equiv> cdl_state_irqs_to_policy_aux aag
(\<lambda>ref. opt_cap ref s)"
definition
transform_asid_rev :: "cdl_asid \<Rightarrow> asid"
where
"transform_asid_rev asid = (of_nat (fst asid) << asid_low_bits) + of_nat (snd asid)"
fun
cdl_cap_asid' :: "cdl_cap \<Rightarrow> asid set"
where
"cdl_cap_asid' (Types_D.FrameCap _ _ _ _ asid) = transform_asid_rev ` Option.set asid"
| "cdl_cap_asid' (Types_D.PageTableCap _ _ asid) = transform_asid_rev ` Option.set asid"
| "cdl_cap_asid' (Types_D.PageDirectoryCap _ _ asid) = transform_asid_rev ` Option.set asid"
| "cdl_cap_asid' (Types_D.AsidPoolCap _ asid) =
{x. fst (transform_asid x) = fst asid \<and> x \<noteq> 0}"
| "cdl_cap_asid' (Types_D.AsidControlCap) = UNIV"
| "cdl_cap_asid' _ = {}"
definition
is_null_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_null_cap cap \<equiv> case cap of
cdl_cap.NullCap \<Rightarrow> True
| _ \<Rightarrow> False"
inductive_set
cdl_state_asids_to_policy_aux for aag caps asid_tab
where
csata_asid: "\<lbrakk> caps ptr = Some cap; asid \<in> cdl_cap_asid' cap \<rbrakk> \<Longrightarrow>
(pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in>
cdl_state_asids_to_policy_aux aag caps asid_tab"
| csata_asid_lookup: "\<lbrakk> asid_tab (fst (transform_asid asid)) = Some poolcap;
\<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap;
caps (cap_object poolcap, snd (transform_asid asid)) = Some pdcap \<rbrakk> \<Longrightarrow>
(pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in>
cdl_state_asids_to_policy_aux aag caps asid_tab"
| csata_asidpool: "\<lbrakk> asid_tab (fst (transform_asid asid)) = Some poolcap;
\<not> is_null_cap poolcap; asid \<noteq> 0 \<rbrakk> \<Longrightarrow>
(pasObjectAbs aag (cap_object poolcap), ASIDPoolMapsASID, pasASIDAbs aag asid) \<in>
cdl_state_asids_to_policy_aux aag caps asid_tab"
abbreviation
"cdl_state_asids_to_policy aag s \<equiv> cdl_state_asids_to_policy_aux aag
(\<lambda>ref. opt_cap ref s) (cdl_asid_table s)"
definition
"cdl_irq_map_wellformed_aux aag irqs \<equiv>
\<forall>irq. pasObjectAbs aag (irqs irq) = pasIRQAbs aag irq"
abbreviation
"cdl_irq_map_wellformed aag s \<equiv> cdl_irq_map_wellformed_aux aag (cdl_irq_node s)"
inductive_set
cdl_domains_of_state_aux for cdl_heap
where
domtcbs: "\<lbrakk> cdl_heap ptr = Some (Tcb cdl_tcb);
d = cdl_tcb_domain cdl_tcb\<rbrakk>
\<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state_aux cdl_heap" |
domidle: "(idle_thread_ptr, default_domain) \<in> cdl_domains_of_state_aux cdl_heap"
abbreviation
"cdl_domains_of_state s \<equiv> cdl_domains_of_state_aux (cdl_objects s)"
definition
"cdl_tcb_domain_map_wellformed_aux aag tcbs_doms \<equiv> \<forall>(ptr, d) \<in> tcbs_doms. pasObjectAbs aag ptr = pasDomainAbs aag d"
abbreviation
"cdl_tcb_domain_map_wellformed aag s \<equiv>
cdl_tcb_domain_map_wellformed_aux aag (cdl_domains_of_state s)"
definition
pcs_refined :: "'a PAS \<Rightarrow> cdl_state \<Rightarrow> bool"
where
"pcs_refined aag s \<equiv>
pas_wellformed aag
\<and> cdl_irq_map_wellformed aag s
\<and> cdl_tcb_domain_map_wellformed aag s
\<and> auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> (pasPolicy aag)
\<and> cdl_state_asids_to_policy aag s \<subseteq> pasPolicy aag
\<and> cdl_state_irqs_to_policy aag s \<subseteq> pasPolicy aag"
lemmas cdl_state_objs_to_policy_mem = eqset_imp_iff[OF cdl_state_objs_to_policy_def]
lemmas cdl_state_objs_to_policy_intros
= cdl_state_bits_to_policy.intros[THEN cdl_state_objs_to_policy_mem[THEN iffD2]]
lemmas csta_caps = cdl_state_objs_to_policy_intros(1)
and csta_cdt = cdl_state_objs_to_policy_intros(2)
lemmas cdl_state_objs_to_policy_cases
= cdl_state_bits_to_policy.cases[OF cdl_state_objs_to_policy_mem[THEN iffD1]]
lemma transform_asid_rev [simp]:
"asid \<le> 2 ^ ARM_Structs_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid"
apply (clarsimp simp:transform_asid_def transform_asid_rev_def
asid_high_bits_of_def ARM_Structs_A.asid_low_bits_def)
apply (clarsimp simp:ucast_nat_def)
apply (subgoal_tac "asid >> 10 < 2 ^ asid_high_bits")
apply (simp add:ARM_Structs_A.asid_high_bits_def ARM_Structs_A.asid_bits_def)
apply (subst ucast_ucast_len)
apply simp
apply (subst shiftr_shiftl1)
apply simp
apply (subst ucast_ucast_mask)
apply (simp add:mask_out_sub_mask)
apply (simp add:ARM_Structs_A.asid_high_bits_def)
apply (rule shiftr_less_t2n[where m=8, simplified])
apply (simp add:ARM_Structs_A.asid_bits_def)
done
abbreviation
"valid_asid_mapping mapping \<equiv> (case mapping of
None \<Rightarrow> True
| Some (asid, ref) \<Rightarrow> asid \<le> 2 ^ ARM_Structs_A.asid_bits - 1)"
lemma transform_asid_rev_transform_mapping [simp]:
"valid_asid_mapping mapping \<Longrightarrow>
transform_asid_rev ` Option.set (transform_mapping mapping) = fst ` Option.set mapping"
apply (simp add:transform_mapping_def option_map_def)
apply (case_tac mapping)
apply clarsimp+
done
lemma fst_transform_cslot_ptr:
"fst ptr = fst (transform_cslot_ptr ptr)"
apply (case_tac ptr)
apply (clarsimp simp:transform_cslot_ptr_def)
done
definition
transform_cslot_ptr_rev :: "cdl_cap_ref \<Rightarrow> cslot_ptr"
where
"transform_cslot_ptr_rev \<equiv> \<lambda>(a, b). (a, the (nat_to_bl WordSetup.word_bits b))"
lemma transform_cslot_pre_onto:
"snd ptr < 2 ^ WordSetup.word_bits \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr'"
apply (rule_tac x="transform_cslot_ptr_rev ptr" in exI)
apply (case_tac ptr)
apply (clarsimp simp:transform_cslot_ptr_def transform_cslot_ptr_rev_def)
apply (clarsimp simp:nat_to_bl_def bin_bl_bin' bintrunc_mod2p)
apply (subst int_mod_eq')
apply (clarsimp simp: not_leE)
apply (drule iffD2[OF zless_int])
apply (clarsimp)
apply simp
done
definition
is_thread_state_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_thread_state_cap cap \<equiv> case cap of
cdl_cap.PendingSyncSendCap _ _ _ _ _ \<Rightarrow> True
| cdl_cap.PendingSyncRecvCap _ _ \<Rightarrow> True
| cdl_cap.PendingAsyncRecvCap _ \<Rightarrow> True
| cdl_cap.RestartCap \<Rightarrow> True
| cdl_cap.RunningCap \<Rightarrow> True
| _ \<Rightarrow> False"
definition
is_real_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_real_cap cap \<equiv> case cap of
cdl_cap.FrameCap _ _ _ Fake _ \<Rightarrow> False
| cdl_cap.PageTableCap _ Fake _ \<Rightarrow> False
| cdl_cap.PageDirectoryCap _ Fake _ \<Rightarrow> False
| _ \<Rightarrow> True"
lemma is_real_cap_transform:
"cap = transform_cap cap' \<Longrightarrow> is_real_cap cap"
by (auto simp:transform_cap_def is_real_cap_def split:cap.splits arch_cap.splits)
lemma is_real_cap_infer_tcb_pending_op:
"is_real_cap (infer_tcb_pending_op a tcb)"
by (auto simp:infer_tcb_pending_op_def is_real_cap_def split:Structures_A.thread_state.splits)
definition
is_untyped_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_untyped_cap cap \<equiv> case cap of
cdl_cap.UntypedCap _ _ \<Rightarrow> True
| _ \<Rightarrow> False"
lemma caps_of_state_transform_opt_cap_rev:
"\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap;
is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap \<rbrakk> \<Longrightarrow>
\<exists>cap' ptr'. cap = transform_cap cap' \<and> ptr = transform_cslot_ptr ptr' \<and>
caps_of_state s ptr' = Some cap'"
apply clarify
apply (drule invs_valid_objs)
apply (case_tac ptr)
apply (clarsimp simp:opt_cap_def transform_def transform_objects_def
transform_cslot_ptr_def slots_of_def opt_object_def)
apply (rule_tac P="a=idle_thread s" in case_split)
apply (clarsimp simp: map_add_def object_slots_def)
apply (case_tac "kheap s a")
apply (clarsimp simp: map_add_def object_slots_def)
apply (clarsimp simp:valid_objs_def dom_def)
apply (drule_tac x=a in spec, clarsimp)
apply (case_tac aa, simp_all add:object_slots_def caps_of_state_def2)
apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def)
apply (clarsimp simp:transform_cnode_contents_def)
apply (rule_tac x=z in exI, simp)
apply (rule_tac x="the (nat_to_bl nata b)" in exI)
apply (clarsimp simp:option_map_join_def split:option.splits)
apply (rule nat_to_bl_to_bin, simp+)
apply (drule valid_etcbs_tcb_etcb [rotated], fastforce)
apply clarsimp
apply (clarsimp simp:transform_tcb_def tcb_slot_defs split:split_if_asm)
apply (simp add:is_thread_state_cap_def infer_tcb_pending_op_def is_null_cap_def
split:Structures_A.thread_state.splits)
apply (rule exI, rule conjI, simp, rule exI, rule conjI,
(rule bl_to_bin_tcb_cnode_index | rule bl_to_bin_tcb_cnode_index[symmetric]),
simp, simp add:tcb_cap_cases_def)+
apply (rule exI, rule conjI, simp)
apply (rule_tac x="tcb_cnode_index 0" in exI)
apply (subst bl_to_bin_tcb_cnode_index_le0)
apply simp+
apply (case_tac arch_kernel_obj, simp_all)
apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:split_if_asm)
apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_asid_pool_entry_def
split:option.splits)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:split_if_asm)
apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pte_def
split:ARM_Structs_A.pte.splits)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:split_if_asm)
apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pde_def
split:ARM_Structs_A.pde.splits)
done
abbreviation
"get_size cap \<equiv> case cap of
cdl_cap.FrameCap _ _ sz _ _ \<Rightarrow> sz
| cdl_cap.PageTableCap _ _ _ \<Rightarrow> 0"
lemma opt_cap_None_word_bits:
"\<lbrakk> einvs s; snd ptr \<ge> 2 ^ WordSetup.word_bits \<rbrakk> \<Longrightarrow> opt_cap ptr (transform s) = None"
apply (case_tac ptr)
apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def opt_object_def)
apply (rule_tac P="a=idle_thread s" in case_split)
apply (clarsimp simp: map_add_def object_slots_def)
apply (case_tac "kheap s a")
apply (clarsimp simp: map_add_def object_slots_def)
apply (drule invs_valid_objs)
apply (simp add:object_slots_def valid_objs_def)
apply (case_tac aa, simp_all)
apply (clarsimp simp:transform_cnode_contents_def object_slots_def)
apply (drule_tac x=a in bspec)
apply (simp add:dom_def)+
apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def)
apply (clarsimp simp:option_map_join_def nat_to_bl_def)
apply (drule not_leE)
apply (subgoal_tac "b < 2 ^ WordSetup.word_bits")
apply simp
apply (rule less_trans)
apply simp
apply (rule power_strict_increasing, simp+)
apply (frule valid_etcbs_tcb_etcb[rotated], fastforce)
apply (clarsimp simp:transform_tcb_def tcb_slot_defs WordSetup.word_bits_def
tcb_pending_op_slot_def)
apply (case_tac arch_kernel_obj, simp_all)
apply (simp add:transform_asid_pool_contents_def transform_page_table_contents_def
transform_page_directory_contents_def unat_map_def WordSetup.word_bits_def)+
done
lemma opt_cap_Some_rev:
"\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap \<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr'"
apply (rule transform_cslot_pre_onto)
apply (subst not_le[symmetric])
apply (rule notI)
apply (drule_tac ptr=ptr in opt_cap_None_word_bits)
apply simp+
done
lemma obj_refs_transform:
"\<not> (\<exists>x sz i. cap = cap.UntypedCap x sz i) \<Longrightarrow> obj_refs cap = cdl_obj_refs (transform_cap cap)"
apply (case_tac cap, clarsimp+)
apply (case_tac arch_cap, clarsimp+)
done
lemma untyped_range_transform:
"(\<exists>x sz i. cap = cap.UntypedCap x sz i) \<Longrightarrow> untyped_range cap = cdl_obj_refs (transform_cap cap)"
apply (case_tac cap, clarsimp+)
done
lemma cap_auth_conferred_transform:
"cap_auth_conferred cap = cdl_cap_auth_conferred (transform_cap cap)"
apply (case_tac cap, (clarsimp simp:cap_auth_conferred_def cdl_cap_auth_conferred_def)+)
apply (case_tac arch_cap, (clarsimp simp:is_page_cap_def)+)
done
lemma thread_states_transform:
"\<lbrakk> einvs s; (oref', auth) \<in> thread_states s oref \<rbrakk> \<Longrightarrow>
(oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s)"
apply clarify
apply (simp add:thread_states_def tcb_states_of_state_def)
apply (cases "get_tcb oref s")
apply simp+
apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce)
apply clarsimp
apply (rule_tac cap="infer_tcb_pending_op oref (tcb_state a)" in csta_caps[where ptr="(oref, 5)"
and auth=auth and oref=oref' and s="transform s", simplified])
apply (rule opt_cap_tcb[where sl=5, unfolded tcb_slot_defs tcb_pending_op_slot_def,
simplified])
apply simp
apply simp
apply (rule notI, drule invs_valid_idle, simp add:valid_idle_def st_tcb_def2)
apply (simp add:infer_tcb_pending_op_def, case_tac "tcb_state a",
(simp add:split_if_asm| erule disjE)+)
apply (simp add:infer_tcb_pending_op_def cdl_cap_auth_conferred_def,
case_tac "tcb_state a", (simp add:split_if_asm| erule disjE)+)
done
lemma thread_state_cap_transform_tcb:
"\<lbrakk> opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap \<rbrakk> \<Longrightarrow>
\<exists>tcb. get_tcb (fst ptr) s = Some tcb"
apply (case_tac ptr)
apply (simp add:opt_cap_def slots_of_def opt_object_def transform_def transform_objects_def)
apply (rule_tac P="a = idle_thread s" in case_split)
apply (clarsimp simp: map_add_def object_slots_def)
apply (case_tac "kheap s (fst ptr)")
apply (clarsimp simp: map_add_def object_slots_def)
apply (simp add:get_tcb_def object_slots_def)
apply (case_tac aa, simp_all)
apply (clarsimp simp:transform_cnode_contents_def)
apply (case_tac z, simp_all add:is_thread_state_cap_def split:split_if_asm)
apply (case_tac arch_cap, simp_all)
apply (case_tac arch_kernel_obj, simp_all)
apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def transform_asid_pool_entry_def
split:split_if_asm option.splits)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def
split:split_if_asm ARM_Structs_A.pte.splits)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def
split:split_if_asm ARM_Structs_A.pde.splits)
done
lemma thread_states_transform_rev:
"\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap;
oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; (fst ptr) \<noteq> idle_thread s \<rbrakk> \<Longrightarrow>
(oref, auth) \<in> thread_states s (fst ptr)"
apply (frule thread_state_cap_transform_tcb, simp)
apply (case_tac ptr)
apply (clarsimp simp:thread_states_def tcb_states_of_state_def)
apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce)
apply (frule_tac sl=b in opt_cap_tcb, assumption, simp)
apply (clarsimp split:split_if_asm)
apply (case_tac "aa tcb", simp_all add:is_thread_state_cap_def split:split_if_asm)
apply (case_tac "arch_cap", simp_all split:split_if_asm)
apply (case_tac "tcb_state tcb", auto simp:infer_tcb_pending_op_def cdl_cap_auth_conferred_def)
done
lemma idle_thread_null_cap:
"\<lbrakk> invs s; caps_of_state s ptr = Some cap; fst ptr = idle_thread s \<rbrakk> \<Longrightarrow> cap = cap.NullCap"
apply (rule_tac s=s and v="snd ptr" in valid_idle_has_null_cap,
(simp add:invs_def valid_state_def)+)
apply (drule_tac s="fst ?x" in sym, simp)
done
lemma idle_thread_no_authority:
"\<lbrakk> invs s; caps_of_state s ptr = Some cap; auth \<in> cap_auth_conferred cap \<rbrakk> \<Longrightarrow>
fst ptr \<noteq> idle_thread s"
apply (rule notI)
apply (drule idle_thread_null_cap, simp+)
apply (simp add:cap_auth_conferred_def)
done
lemma idle_thread_no_untyped_range:
"\<lbrakk> invs s; caps_of_state s ptr = Some cap; auth \<in> untyped_range cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s"
apply (rule notI)
apply (drule idle_thread_null_cap, simp+)
done
lemma fst':
"(a :: cdl_object_id) = fst (a, b)"
apply simp
done
lemma opt_cap_pt_Some':
"\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)) \<rbrakk>
\<Longrightarrow> (opt_cap (a, unat slot) (transform s)) = Some (transform_pte (fun slot))"
apply (clarsimp simp:opt_cap_def transform_def slots_of_def opt_object_def object_slots_def
transform_objects_def map_add_def restrict_map_def not_idle_thread_def)
apply (frule arch_obj_not_idle,simp)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def not_idle_thread_def)
apply (rule unat_lt2p[where 'a=8, simplified])
done
lemma pte_cdl_obj_refs:
"\<lbrakk> pte_ref pte = Some (a, b, c); ptr \<in> ptr_range a b \<rbrakk> \<Longrightarrow>
ptr \<in> cdl_obj_refs (transform_pte pte)"
apply (case_tac pte)
apply (simp_all add:pte_ref_def transform_pte_def)
done
lemma pte_cdl_cap_auth_conferred:
"\<lbrakk> pte_ref pte = Some (a, b, c); auth \<in> c \<rbrakk> \<Longrightarrow>
auth \<in> cdl_cap_auth_conferred (transform_pte pte)"
apply (case_tac pte)
apply (simp_all add:pte_ref_def transform_pte_def cdl_cap_auth_conferred_def)
done
lemma opt_cap_pd_Some':
"\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun));
slot < ucast (kernel_base >> 20) \<rbrakk> \<Longrightarrow>
(opt_cap (a, unat slot) (transform s)) = Some (transform_pde (fun slot))"
apply (clarsimp simp:opt_cap_def transform_def slots_of_def opt_object_def object_slots_def
transform_objects_def restrict_map_def map_add_def not_idle_thread_def)
apply (frule arch_obj_not_idle,simp)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def not_idle_thread_def
kernel_pde_mask_def word_not_le[symmetric])
apply (rule unat_lt2p[where 'a="12", simplified])
done
lemma pde_cdl_obj_refs:
"\<lbrakk> pde_ref2 pde = Some (a, b, c); ptr \<in> ptr_range a b \<rbrakk> \<Longrightarrow>
ptr \<in> cdl_obj_refs (transform_pde pde)"
apply (case_tac pde)
apply (simp_all add:pde_ref2_def transform_pde_def ptr_range_def)
done
lemma pde_cdl_cap_auth_conferred:
"\<lbrakk> pde_ref2 pde = Some (a, b, c); auth \<in> c \<rbrakk> \<Longrightarrow>
auth \<in> cdl_cap_auth_conferred (transform_pde pde)"
apply (case_tac pde)
apply (simp_all add:pde_ref2_def transform_pde_def cdl_cap_auth_conferred_def)
done
lemma state_vrefs_transform:
"\<lbrakk> invs s; ptr \<noteq> idle_thread s; (ptr', ref, auth) \<in> state_vrefs s ptr \<rbrakk> \<Longrightarrow>
(ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)"
apply (simp add:state_vrefs_def, case_tac "kheap s ptr", simp+)
apply (case_tac a, simp_all add:vs_refs_no_global_pts_def)
apply (case_tac arch_kernel_obj, simp_all add:vs_refs_no_global_pts_def)
apply (clarsimp simp:graph_of_def)
apply (subst fst')
apply (rule csta_caps)
apply (drule_tac asid="ucast aa" in opt_cap_asid_pool_Some[rotated])
apply (simp add:invs_valid_idle)
apply (simp add:ucast_up_ucast_id is_up_def source_size_def target_size_def word_size)
apply (simp add:transform_asid_pool_entry_def)
apply (simp add:transform_asid_pool_entry_def cdl_cap_auth_conferred_def)
apply (clarsimp simp:graph_of_def)
apply (subst fst')
apply (rule csta_caps)
apply (drule_tac slot=aa in opt_cap_pt_Some'[rotated])
apply (simp add:invs_valid_idle)
apply simp
apply (rule_tac a=ab and b=ac and c=b in pte_cdl_obj_refs, simp+)
apply (rule_tac a=ab and b=ac and c=b in pte_cdl_cap_auth_conferred, simp+)
apply (erule bexE)
apply (clarsimp simp:graph_of_def)
apply (subst fst')
apply (rule csta_caps)
apply (drule_tac slot=aa in opt_cap_pd_Some'[rotated])
apply (simp add:word_not_le[symmetric])
apply (simp add:invs_valid_idle)
apply simp
apply (rule_tac a=ab and b=ac and c=b in pde_cdl_obj_refs, simp+)
apply (rule_tac a=ab and b=ac and c=b in pde_cdl_cap_auth_conferred, simp+)
done
lemma pte_ref_transform_rev:
"ptr' \<in> cdl_obj_refs (transform_pte pte) \<Longrightarrow>
pte_ref pte = Some (cap_object (transform_pte pte), get_size (transform_pte pte),
cdl_cap_auth_conferred (transform_pte pte)) \<and>
ptr' \<in> ptr_range (cap_object (transform_pte pte)) (get_size (transform_pte pte))"
apply (case_tac pte)
apply (simp_all add:pte_ref_def transform_pte_def
vspace_cap_rights_to_auth_def cdl_cap_auth_conferred_def)
done
lemma pde_ref_transform_rev:
"ptr' \<in> cdl_obj_refs (transform_pde pde) \<Longrightarrow>
pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde),
cdl_cap_auth_conferred (transform_pde pde)) \<and>
ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde))"
apply (case_tac pde)
apply (simp_all add:pde_ref2_def transform_pde_def ptr_range_def
vspace_cap_rights_to_auth_def cdl_cap_auth_conferred_def)
done
lemma state_vrefs_transform_rev:
"\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap;
auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap \<rbrakk> \<Longrightarrow>
\<exists>ref. (ptr', ref, auth) \<in> state_vrefs s (fst ptr)"
apply (case_tac ptr, clarsimp)
apply (subgoal_tac "a \<noteq> idle_thread s")
prefer 2
apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
opt_cap_def slots_of_def opt_object_def)
apply (clarsimp simp: map_add_def object_slots_def)
apply (case_tac "kheap s a")
apply (clarsimp simp: state_vrefs_def transform_def transform_objects_def
opt_cap_def slots_of_def opt_object_def)
apply (clarsimp simp: map_add_def object_slots_def)
apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
opt_cap_def slots_of_def opt_object_def)
apply (case_tac aa, simp_all add:transform_object_def object_slots_def)
apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform)
apply (frule valid_etcbs_tcb_etcb [rotated], fastforce)
apply (clarsimp simp:transform_tcb_def is_real_cap_transform is_real_cap_infer_tcb_pending_op
split:split_if_asm)
apply (case_tac arch_kernel_obj, simp_all add:vs_refs_no_global_pts_def graph_of_def)
apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:split_if_asm)
apply (rule exI)
apply (case_tac "fun (of_nat b)")
apply (clarsimp simp:transform_asid_pool_entry_def)
apply (rule_tac x="(of_nat b, ptr')" in image_eqI)
apply (clarsimp simp:transform_asid_pool_entry_def cdl_cap_auth_conferred_def)
apply simp
apply (clarsimp simp:transform_asid_pool_entry_def)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:split_if_asm)
apply (rule exI)+
apply (drule pte_ref_transform_rev)
apply safe[1]
apply simp
apply (rule_tac x="(ptr', auth)" in image_eqI)
apply simp
apply simp
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:split_if_asm)
apply (subgoal_tac "(of_nat b :: 12 word) < ucast (kernel_base >> 20)")
prefer 2
apply (subst word_not_le[symmetric])
apply (rule notI)
apply (clarsimp simp:kernel_pde_mask_def transform_pde_def)
apply (simp add:kernel_pde_mask_def not_less[symmetric])
apply (rule exI)
apply (drule pde_ref_transform_rev, clarsimp)
apply (rule bexI)
prefer 2
apply fastforce
apply clarsimp
apply (rule_tac x="(ptr', auth)" in image_eqI)
apply simp
apply simp
done
lemma cdl_cdt_transform_rev:
"\<lbrakk> invs s; cdl_cdt (transform s) slot' = Some slot \<rbrakk> \<Longrightarrow>
\<exists>ptr' ptr. slot' = transform_cslot_ptr ptr' \<and> slot = transform_cslot_ptr ptr \<and>
cdt s ptr' = Some ptr"
apply (clarsimp simp:cdt_transform map_lift_over_def split:split_if_asm)
apply (rule_tac x=a in exI, rule_tac x=b in exI)
apply (subst (asm) inv_into_f_f)
apply (rule subset_inj_on)
apply (simp add:dom_def)+
done
lemma state_objs_transform:
"\<lbrakk> einvs s; (x, a, y) \<in> state_objs_to_policy s \<rbrakk> \<Longrightarrow>
(x, a, y) \<in> cdl_state_objs_to_policy (transform s)"
apply (rule state_objs_to_policy_cases, simp)
apply (simp add:fst_transform_cslot_ptr)
apply (rule_tac ptr="transform_cslot_ptr ptr" and auth=auth and oref=oref and
cap="transform_cap cap" and s="transform s" in csta_caps)
apply (rule caps_of_state_transform_opt_cap)
apply simp
apply fastforce
apply (simp add:idle_thread_no_authority)
apply (case_tac cap, simp+)
apply (case_tac arch_cap, simp+)
apply (simp add:cap_auth_conferred_transform)
apply (simp add:fst_transform_cslot_ptr)
apply (rule_tac ptr="transform_cslot_ptr ptr" and auth=Control and oref=oref and
cap="transform_cap cap" and s="transform s" in csta_caps)
apply (rule caps_of_state_transform_opt_cap)
apply simp
apply fastforce
apply (simp add:idle_thread_no_untyped_range)
apply (case_tac cap, (simp add:untyped_range_transform del:untyped_range.simps(1))+)
apply (case_tac cap, (simp add:cdl_cap_auth_conferred_def)+)
apply (rule thread_states_transform, simp+)
apply (simp add:fst_transform_cslot_ptr)
apply (rule_tac slot="transform_cslot_ptr slot" and slot'="transform_cslot_ptr slot'"
and s="transform s" in csta_cdt)
apply (simp add:transform_def)
apply (rule transform_cdt_some)
apply (simp add:invs_mdb_cte)
apply simp
apply (subgoal_tac "ptr \<noteq> idle_thread s")
apply (simp add:state_vrefs_transform)
apply (clarsimp simp:state_vrefs_def vs_refs_no_global_pts_def invs_def valid_state_def
valid_idle_def st_tcb_at_def obj_at_def)
done
lemma state_objs_transform_rev:
"\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s) \<rbrakk> \<Longrightarrow>
(x, a, y) \<in> state_objs_to_policy s"
apply (rule cdl_state_objs_to_policy_cases, simp)
apply (rule_tac P="is_thread_state_cap cap" in case_split)
apply simp
apply (rule sta_ts)
apply (rule thread_states_transform_rev, simp+)
apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def opt_object_def)
apply (clarsimp simp: map_add_def object_slots_def)
apply (rule_tac P="is_real_cap cap" in case_split[rotated])
apply (drule state_vrefs_transform_rev, simp+)
apply clarsimp
apply (rule sta_vref)
apply simp
apply (subgoal_tac "\<not> is_null_cap cap")
prefer 2
apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits)
apply (frule caps_of_state_transform_opt_cap_rev, simp+)
apply (rule_tac P="is_untyped_cap cap" in case_split)
apply (subgoal_tac "a = Control")
apply clarsimp
apply (subst fst_transform_cslot_ptr[symmetric])
apply (rule_tac cap=cap' in sta_untyped)
apply simp
apply (subst (asm) untyped_range_transform[symmetric])
apply (simp add:is_untyped_cap_def transform_cap_def
split:cap.splits arch_cap.splits split_if_asm)
apply simp
apply (simp add:cdl_cap_auth_conferred_def is_untyped_cap_def split:cdl_cap.splits)
apply clarsimp
apply (subst fst_transform_cslot_ptr[symmetric])
apply (rule_tac cap=cap' in sta_caps)
apply simp
apply (subst (asm) obj_refs_transform[symmetric])
apply (simp add:is_untyped_cap_def transform_cap_def
split:cap.splits arch_cap.splits split_if_asm)
apply simp
apply (simp add:cap_auth_conferred_transform)
apply (drule cdl_cdt_transform_rev [rotated], simp+)
apply clarsimp
apply (subst fst_transform_cslot_ptr[symmetric])+
apply (rule sta_cdt)
apply simp
done
lemma state_vrefs_asidpool_control:
"(pdptr, Invariants_AI.VSRef asid (Some Invariants_AI.AASIDPool), auth) \<in>
state_vrefs s poolptr \<Longrightarrow> auth = Control"
apply (clarsimp simp:state_vrefs_def )
apply (cases "kheap s poolptr")
apply clarsimp
apply (simp add: vs_refs_no_global_pts_def, case_tac a, clarsimp+)
apply (case_tac arch_kernel_obj, clarsimp+)
done
lemma idle_thread_no_asid:
"\<lbrakk> invs s; Invariants_AI.caps_of_state s ptr = Some cap;
asid \<in> cap_asid' cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s"
apply (rule notI)
apply (drule idle_thread_null_cap, simp+)
done
lemma asid_table_entry_transform:
"arm_asid_table (arch_state s) (asid_high_bits_of asid) = poolptr \<Longrightarrow>
cdl_asid_table (transform s) (fst (transform_asid asid)) =
Some (transform_asid_table_entry poolptr)"
apply (clarsimp simp:transform_def transform_asid_table_def unat_map_def
transform_asid_table_entry_def transform_asid_def)
apply (simp add:transform_asid_def asid_high_bits_of_def asid_low_bits_def)
apply (rule unat_lt2p[where 'a=8, simplified])
done
lemma transform_asid_high_bits_of:
"of_nat (fst (transform_asid asid)) = asid_high_bits_of asid"
apply (clarsimp simp:transform_asid_def asid_high_bits_of_def)
done
lemma transform_asid_high_bits_of':
"fst (transform_asid asid) = unat (asid_high_bits_of asid)"
apply (clarsimp simp:transform_asid_def asid_high_bits_of_def)
done
lemma transform_asid_low_bits_of:
"of_nat (snd (transform_asid asid)) = (ucast asid :: 10 word)"
apply (clarsimp simp:transform_asid_def)
done
lemma cap_asid'_transform:
"\<lbrakk> invs s; caps_of_state s ptr = Some cap \<rbrakk> \<Longrightarrow> cap_asid' cap = cdl_cap_asid' (transform_cap cap)"
apply (case_tac cap, simp_all)
apply (drule caps_of_state_valid, simp)
apply (case_tac arch_cap, simp_all)
apply (clarsimp simp:transform_asid_high_bits_of' valid_cap_def split:option.splits)+
done
lemma state_asids_transform:
"\<lbrakk> einvs s; (x, a, y) \<in> state_asids_to_policy aag s \<rbrakk> \<Longrightarrow>
(x, a, y) \<in> cdl_state_asids_to_policy aag (transform s)"
apply (drule state_asids_to_policy_aux.induct)
prefer 4
apply simp
apply (simp add:fst_transform_cslot_ptr)
apply (rule_tac cap="transform_cap cap" in csata_asid)
apply (rule caps_of_state_transform_opt_cap)
apply simp
apply fastforce
apply (clarsimp simp:idle_thread_no_asid)
apply (fastforce simp: cap_asid'_transform)
apply (frule state_vrefs_asidpool_control, simp)
apply (simp add:state_vrefs_def, case_tac "kheap s poolptr", simp_all)
apply (case_tac aa, simp_all add:vs_refs_no_global_pts_def)
apply (case_tac arch_kernel_obj, simp_all add:graph_of_def, safe)
apply (rule_tac pdcap="cdl_cap.PageDirectoryCap b Fake None" in csata_asid_lookup)
apply (simp add:asid_table_entry_transform)
apply (simp add:is_null_cap_def transform_asid_table_entry_def)
apply (simp add:is_null_cap_def transform_asid_table_entry_def)
apply (simp add:ucast_up_ucast_id is_up_def source_size_def target_size_def word_size)
apply (simp add:transform_asid_table_entry_def)
apply (drule_tac asid="asid" in opt_cap_asid_pool_Some[rotated])
apply (simp add:invs_valid_idle)
apply (subst (asm) mask_asid_low_bits_ucast_ucast)
apply (subst (asm) up_ucast_inj_eq)
apply simp
apply (simp add:transform_asid_pool_entry_def)
apply (cut_tac aag=aag and asid=asid and asid_tab="cdl_asid_table (transform s)" in csata_asidpool)
apply (clarsimp simp:transform_def transform_asid_table_def unat_map_def)
apply safe[1]
apply (simp add:transform_asid_table_entry_def transform_asid_high_bits_of)
apply (simp add:transform_asid_def unat_lt2p[where 'a=8, simplified])
apply (simp add:is_null_cap_def)
apply simp
apply simp
done
lemma opt_cap_Some_asid_real:
"\<lbrakk> opt_cap ref (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; einvs s \<rbrakk> \<Longrightarrow> is_real_cap cap"
apply (case_tac ref)
apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def opt_object_def)
apply (rule_tac P="a=idle_thread s" in case_split)
apply (clarsimp simp: map_add_def object_slots_def)
apply (case_tac "kheap s a")
apply (clarsimp simp: map_add_def object_slots_def)
apply (case_tac aa, simp_all add:object_slots_def valid_objs_def)
apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform)
apply (frule valid_etcbs_tcb_etcb[rotated], fastforce)
apply (clarsimp simp:transform_tcb_def tcb_slot_defs is_real_cap_transform
is_real_cap_infer_tcb_pending_op split:split_if_asm)
apply (case_tac arch_kernel_obj, simp_all)
apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:split_if_asm)
apply (clarsimp simp:transform_asid_pool_entry_def split:option.splits)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:split_if_asm)
apply (clarsimp simp:transform_pte_def split:ARM_Structs_A.pte.splits)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:split_if_asm)
apply (clarsimp simp:transform_pde_def split:ARM_Structs_A.pde.splits)
done
lemma state_vrefs_asid_pool_transform_rev:
"\<lbrakk> einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap;
\<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap;
opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap \<rbrakk> \<Longrightarrow>
(pdptr, VSRef (asid && mask ARM_Structs_A.asid_low_bits) (Some AASIDPool), Control)
\<in> state_vrefs s (cap_object poolcap)"
apply (subgoal_tac "cap_object poolcap \<noteq> idle_thread s")
prefer 2
apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
opt_cap_def slots_of_def opt_object_def)
apply (clarsimp simp: map_add_def object_slots_def)
apply (case_tac "kheap s (cap_object poolcap)")
apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
opt_cap_def slots_of_def opt_object_def)
apply (clarsimp simp: map_add_def object_slots_def)
apply (clarsimp simp:transform_asid_high_bits_of')
apply (simp add:asid_table_transform transform_asid_table_entry_def is_null_cap_def
split:option.splits)
apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def
opt_cap_def slots_of_def opt_object_def)
apply (drule invs_valid_asid_table)
apply (clarsimp simp:valid_asid_table_def)
apply (drule bspec)
apply fastforce
apply (case_tac a, simp_all add:transform_object_def object_slots_def)
apply (clarsimp simp:obj_at_def a_type_def split:split_if_asm)+
apply (case_tac arch_kernel_obj, simp_all add:vs_refs_no_global_pts_def graph_of_def)
apply (simp add:transform_asid_pool_contents_def unat_map_def transform_asid_low_bits_of
split:split_if_asm)
apply (rule_tac x="(ucast asid, cap_object pdcap)" in image_eqI)
apply (simp add:mask_asid_low_bits_ucast_ucast)
apply (clarsimp simp:transform_asid_pool_entry_def split:option.splits)
done
lemma state_asids_transform_rev:
"\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s) \<rbrakk> \<Longrightarrow>
(x, a, y) \<in> state_asids_to_policy aag s"
apply (erule cdl_state_asids_to_policy_aux.induct)
apply (rule_tac P="is_thread_state_cap cap" in case_split)
apply (clarsimp simp:is_thread_state_cap_def split:cdl_cap.splits)
apply (rule_tac P="\<not> is_real_cap cap" in case_split)
apply (clarsimp simp:opt_cap_Some_asid_real)
apply (rule_tac P="is_null_cap cap" in case_split)
apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits)
apply (frule caps_of_state_transform_opt_cap_rev, simp+)
apply clarsimp
apply (subst fst_transform_cslot_ptr[symmetric])
apply (rule sata_asid)
apply simp
apply (simp add:cap_asid'_transform)
apply (rule_tac poolptr="cap_object poolcap" in sata_asid_lookup)
apply (clarsimp simp:transform_asid_high_bits_of')
apply (simp add:asid_table_transform transform_asid_table_entry_def is_null_cap_def
split:option.splits)
apply (drule_tac t=poolcap in sym)
apply simp
apply (rule state_vrefs_asid_pool_transform_rev, simp_all)
apply (rule sata_asidpool)
apply (clarsimp simp:transform_asid_high_bits_of')
apply (simp add:asid_table_transform transform_asid_table_entry_def is_null_cap_def
split:option.splits)
apply (drule_tac t=poolcap in sym)
apply simp
apply simp
done
lemma idle_thread_no_irqs:
"\<lbrakk> invs s; Invariants_AI.caps_of_state s ptr = Some cap;
irq \<in> cap_irqs_controlled cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s"
apply (rule notI)
apply (drule idle_thread_null_cap, simp+)
done
lemma cap_irqs_controlled_transform:
"cap_irqs_controlled cap = cdl_cap_irqs_controlled (transform_cap cap)"
apply (case_tac cap, simp_all)
apply (case_tac arch_cap, simp_all)
done
lemma state_irqs_transform:
"\<lbrakk> einvs s; (x, a, y) \<in> state_irqs_to_policy aag s \<rbrakk> \<Longrightarrow>
(x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s)"
apply (erule state_irqs_to_policy_aux.induct)
apply (simp add: fst_transform_cslot_ptr)
apply (rule_tac cap="transform_cap cap" in csita_controlled)
apply (rule caps_of_state_transform_opt_cap)
apply simp
apply fastforce
apply (clarsimp simp:idle_thread_no_irqs)
apply (simp add: cap_irqs_controlled_transform)
done
lemma state_irqs_transform_rev:
"\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s) \<rbrakk> \<Longrightarrow>
(x, a, y) \<in> state_irqs_to_policy aag s"
apply (erule cdl_state_irqs_to_policy_aux.induct)
apply (rule_tac P="is_thread_state_cap cap" in case_split)
apply (clarsimp simp:is_thread_state_cap_def split:cdl_cap.splits)
apply (rule_tac P="\<not> is_real_cap cap" in case_split)
apply (clarsimp simp:is_real_cap_def split:cdl_cap.splits)
apply (rule_tac P="is_null_cap cap" in case_split)
apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits)
apply (frule caps_of_state_transform_opt_cap_rev, simp+)
apply clarsimp
apply (subst fst_transform_cslot_ptr[symmetric])
apply (rule_tac cap=cap' in sita_controlled)
apply simp
apply (simp add:cap_irqs_controlled_transform)
done
lemma irq_map_wellformed_transform:
"irq_map_wellformed aag s = cdl_irq_map_wellformed aag (transform s)"
apply (clarsimp simp:irq_map_wellformed_aux_def cdl_irq_map_wellformed_aux_def
transform_def)
done
lemma einvs_idle:
"einvs s \<Longrightarrow> idle_thread s = idle_thread_ptr"
by (simp add: invs_def valid_state_def valid_idle_def)
lemma einvs_idle_domain:
"einvs s \<Longrightarrow> \<exists>etcb. ekheap s idle_thread_ptr = Some etcb \<and> tcb_domain etcb = default_domain"
apply (clarsimp simp: valid_sched_def valid_idle_etcb_def etcb_at_def
valid_etcbs_def invs_def valid_state_def valid_idle_def st_tcb_at_def obj_at_def is_etcb_at_def
split: option.splits)
apply (erule_tac x="idle_thread s" in allE)
apply simp
done
lemma cdl_domains_of_state_transform:
assumes e: "einvs s"
shows "cdl_domains_of_state (transform s) = domains_of_state s"
proof -
{ fix ptr d
assume "(ptr, d) \<in> cdl_domains_of_state (transform s)"
hence "(ptr, d) \<in> domains_of_state s"
apply (cases)
using e
apply (clarsimp simp: transform_def transform_objects_def restrict_map_def
split: split_if_asm Structures_A.kernel_object.splits)
apply (case_tac z, simp_all)
prefer 2
apply (case_tac arch_kernel_obj, simp_all)
apply (drule valid_etcbs_tcb_etcb [rotated], fastforce)
apply clarsimp
apply (rule domains_of_state_aux.intros, assumption)
apply (clarsimp simp: transform_tcb_def transform_full_intent_def Let_def)
apply (insert einvs_idle [OF e])
apply (insert einvs_idle_domain [OF e])
apply clarsimp
apply (erule domains_of_state_aux.domtcbs)
apply simp
done
}
note a = this
{