-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathFinalise_DR.thy
3841 lines (3570 loc) · 173 KB
/
Finalise_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 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 Finalise_DR
imports
KHeap_DR
"../invariant-abstract/PDPTEntries_AI"
begin
declare dxo_wp_weak[wp del]
definition
"transform_pd_slot_ref x
= (x && ~~ mask pd_bits,
unat ((x && mask pd_bits) >> 2))"
definition
"transform_pt_slot_ref x
= (x && ~~ mask pt_bits,
unat ((x && mask pt_bits) >> 2))"
lemma trancl_image:
assumes inj: "inj_on f (Domain S \<union> Range S)"
shows "trancl ((\<lambda>(x, y). (f x, f y)) ` S) = (\<lambda>(x, y). (f x, f y)) ` trancl S"
(is "?lhs = ?rhs")
apply safe
apply (erule trancl.induct)
apply clarsimp
apply (erule image_eqI[rotated, OF r_into_trancl])
apply simp
apply (clarsimp simp: inj_on_iff[OF inj]
RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]]
DomainI)
apply (erule(1) image_eqI[rotated, OF trancl_into_trancl])
apply simp
apply (erule trancl.induct)
apply (rule r_into_trancl, erule image_eqI[rotated])
apply simp
apply (erule trancl_into_trancl)
apply (erule image_eqI[rotated])
apply simp
done
lemma descendants_of_eqv:
assumes cte_at: "mdb_cte_at (swp (cte_wp_at P) s) (cdt s)"
and cte_at_p: "cte_at p s"
shows "KHeap_D.descendants_of (transform_cslot_ptr p) (transform s)
= transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s)"
proof -
note inj = transform_cdt_slot_inj_on_mdb_cte_at[OF cte_at]
have P: "{(x, y). KHeap_D.is_cdt_parent (transform s) x y}
= (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y))
` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}"
apply (simp add: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def)
apply (simp add: transform_def transform_cdt_def map_lift_over_eq_Some
inj)
apply auto
done
have inj': "inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s))"
using cte_at_p mdb_cte_atD[OF _ cte_at]
apply -
apply (rule transform_cdt_slot_inj_on_cte_at[where P=\<top> and s=s])
apply (fastforce simp: cte_wp_at_caps_of_state elim!: ranE)
done
show ?thesis
apply (simp add: KHeap_D.descendants_of_def CSpaceAcc_A.descendants_of_def
KHeap_D.cdt_parent_rel_def CSpaceAcc_A.cdt_parent_rel_def)
apply (simp add: P)
apply (subst trancl_image)
apply (rule subset_inj_on[OF inj])
apply (auto simp: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def)[1]
apply safe
apply (subst(asm) inj_on_iff[OF inj'], simp_all)
apply (drule DomainI[THEN eqset_imp_iff[OF trancl_domain, THEN iffD1]])
apply (auto simp: CSpaceAcc_A.is_cdt_parent_def)
done
qed
lemma dcorres_revoke_cap_no_descendants:
"slot' = transform_cslot_ptr slot \<Longrightarrow>
dcorres dc \<top> (\<lambda>s. valid_mdb s \<and> cte_at slot s \<and> CSpaceAcc_A.descendants_of slot (cdt s) = {})
(revoke_cap_simple slot')
(return x)"
apply (rule dcorres_revoke_cap_simple_helper)
apply (simp add:gets_def)
apply (rule dcorres_absorb_get_l)
apply (subgoal_tac "(KHeap_D.descendants_of slot' (transform s')) = {}")
apply clarsimp
apply (rule dcorres_absorb_get_l)
apply clarsimp
apply (clarsimp simp:descendants_of_eqv valid_mdb_def)
done
lemma dcorres_revoke_cap_unnecessary:
"dcorres dc \<top> (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr
and cte_at (ptr,tcb_cnode_index 2) and not_idle_thread ptr and valid_idle)
(revoke_cap_simple (ptr, tcb_replycap_slot))
(return x)"
apply (subst transform_tcb_slot_simp[symmetric])
apply (rule corres_guard_imp)
apply (rule dcorres_revoke_cap_no_descendants)
apply (simp add:transform_tcb_slot_simp[symmetric])+
apply (rule not_waiting_reply_slot_no_descendants)
apply simp_all
done
lemma descendants_exist_in_cdt:
"\<lbrakk> a \<in> descendants_of p (cdt s) \<rbrakk>
\<Longrightarrow> cdt s a \<noteq> None"
apply (simp add: descendants_of_def cdt_parent_rel_def)
apply (frule RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]])
apply (clarsimp simp: is_cdt_parent_def)
done
lemma descendants_exist_in_cdl_cdt:
"\<lbrakk> a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk>
\<Longrightarrow> cdl_cdt (transform s) a \<noteq> None"
apply (simp add: KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def)
apply (frule RangeI)
apply (frule DomainI)
apply (clarsimp simp: KHeap_D.is_cdt_parent_def)
done
lemma cdl_cdt_parent_cte_at_lift:
"\<lbrakk> mdb_cte_at (swp (cte_wp_at P) s) (cdt s) ; a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk>
\<Longrightarrow> (\<exists>slot. cte_at slot s \<and> p = transform_cslot_ptr slot)"
apply (simp add:KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def)
apply (frule DomainI)
apply (clarsimp simp:KHeap_D.is_cdt_parent_def)
apply (simp add:transform_def transform_cdt_def)
apply (clarsimp simp:transform_cdt_slot_inj_on_mdb_cte_at map_lift_over_eq_Some split:if_splits)
apply (rule_tac x = ab in exI,rule_tac x = bb in exI)
apply (drule(1) mdb_cte_atD)
apply (clarsimp simp :cte_wp_at_cte_at)
done
lemma descendants_not_null_cap:
"\<lbrakk> a \<in> descendants_of p (cdt s); mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<rbrakk>
\<Longrightarrow> cte_wp_at P a s"
apply (drule descendants_exist_in_cdt)
apply clarsimp
apply (drule(1) mdb_cte_atD)
apply simp
done
lemma descendants_in_cte_wp_set:
"mdb_cte_at (swp (cte_wp_at P ) s) (cdt s)
\<Longrightarrow> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> Collect (\<lambda>x. cte_wp_at (P) x s)"
by (auto simp:descendants_not_null_cap)
lemma ex_in_none_empty_set:
"a\<noteq>{} \<Longrightarrow> \<exists>x. x\<in>a"
by auto
lemma finite_descendants_if_from_transform:
" mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s))"
apply (case_tac "KHeap_D.descendants_of x (transform s) = {}")
apply simp
apply (drule ex_in_none_empty_set)
apply clarsimp
apply (frule(1) cdl_cdt_parent_cte_at_lift)
apply clarsimp
apply (frule(1) descendants_of_eqv)
apply clarsimp
apply (rule finite_imageI)
apply (rule finite_subset)
apply (rule descendants_in_cte_wp_set)
apply simp
apply (simp add:cte_wp_at_set_finite)
done
lemma delete_cdt_slot_shrink_descendants:
"\<lbrace>\<lambda>s. valid_mdb s \<and> x = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p x \<and> x = y \<rbrace>
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
\<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and>
CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p y \<rbrace>"
apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def)
apply (rule conjI)
apply (subgoal_tac "mdb_empty_abs s")
apply (clarsimp simp:mdb_empty_abs.descendants mdb_empty_abs_def vmdb_abs_def)+
done
lemma delete_cap_one_shrink_descendants:
"\<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace> cap_delete_one slot
\<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and>
CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace>"
apply (simp add:cap_delete_one_def unless_def)
apply wp
apply (clarsimp simp add:empty_slot_def)
apply (wp dxo_wp_weak)
apply simp
apply (rule_tac P="\<lambda>s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s)
\<and> mdb_cte_at (swp (cte_wp_at (op\<noteq> cap.NullCap)) s) (cdt s)"
in hoare_vcg_precond_imp)
apply (rule_tac Q ="\<lambda>r s. Q r s \<and> (mdb_cte_at (swp (cte_wp_at (op\<noteq> cap.NullCap)) s) (cdt s))" for Q in hoare_strengthen_post)
apply (rule hoare_vcg_conj_lift)
apply (rule delete_cdt_slot_shrink_descendants[where y= "cdt pres" and p = p])
apply (rule_tac Q="\<lambda>s. mdb_cte_at (swp (cte_wp_at (op\<noteq>cap.NullCap)) s ) xa" in hoare_vcg_precond_imp)
apply (case_tac slot)
apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def mdb_cte_at_def)
apply (assumption)
apply clarsimp+
apply (assumption)
apply wp
apply (rule hoare_vcg_conj_lift[where P="\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at (op\<noteq>cap.NullCap)) s) (cdt s)"])
prefer 2
apply (rule hoare_drop_imp)
apply wp
apply (clarsimp simp:valid_def in_get_cap_cte_wp_at)
apply (drule sym)
apply clarsimp
apply (drule descendants_not_null_cap)
apply simp
apply (simp add:cte_wp_at_def)
apply (wp|simp)+
apply (rule hoare_vcg_conj_lift)
apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise])
apply (clarsimp simp:valid_mdb_def swp_def)
apply wp
apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise])
apply (clarsimp simp:valid_mdb_def swp_def)
apply wp
apply (clarsimp simp:valid_def in_get_cap_cte_wp_at)
apply (clarsimp simp:invs_def valid_mdb_def valid_state_def)
apply (drule descendants_not_null_cap)
apply simp
apply (clarsimp simp:cte_wp_at_def)
done
lemma invs_emptyable_descendants:
"\<lbrakk>invs s;CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}\<rbrakk>
\<Longrightarrow> emptyable (a, b) s"
apply (clarsimp simp:emptyable_def)
apply (frule reply_slot_not_descendant)
apply simp
apply fastforce
done
lemma cap_delete_one_cte_at:
"\<lbrace>invs and emptyable sl and cte_at x\<rbrace> cap_delete_one sl \<lbrace>\<lambda>_. cte_at x\<rbrace>"
apply (simp add:cap_delete_one_def)
apply wp
apply (clarsimp simp:unless_def when_def | rule conjI)+
apply (wp|clarsimp)+
done
lemma nat_to_bl_zero_zero:
"(nat_to_bl 0 0) = (Some [])"
by (clarsimp simp: nat_to_bl_def)
lemma caps_of_state_transform_opt_cap_no_idle:
"\<lbrakk>caps_of_state s p = Some cap; valid_etcbs s\<rbrakk>
\<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s)
= Some (transform_cap cap) \<or>
opt_cap (transform_cslot_ptr p) (transform s)
= None"
apply (frule caps_of_state_cteD)
apply (cases p)
apply (erule cte_wp_atE)
apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def object_slots_def
slots_of_def opt_object_def transform_def transform_objects_def
transform_cnode_contents_def well_formed_cnode_n_def
restrict_map_def
split: option.splits split_if_asm nat.splits)
apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI])
apply (simp add: nat_to_bl_zero_zero option_map_join_def)
apply clarsimp
apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI])
apply (simp add: option_map_join_def nat_to_bl_dest)
apply (clarsimp simp: cap_installed_at_irq_def valid_irq_node_def
obj_at_def is_cap_table_def well_formed_cnode_n_def
length_set_helper word_bl.Abs_inverse
object_slots_def nat_bl_to_bin_lt2p)
apply (frule(1) valid_etcbs_tcb_etcb)
apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def
slots_of_def opt_object_def restrict_map_def
transform_def object_slots_def transform_objects_def
valid_irq_node_def obj_at_def is_cap_table_def
transform_tcb_def tcb_slot_defs
tcb_cap_cases_def bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
split: split_if_asm option.splits)
done
lemma transform_cap_Null [simp]:
"(transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap)"
apply (cases cap, simp_all)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all)
done
lemma dcorres_revoke_the_cap_corres:
"dcorres dc \<top>
(invs and cte_at slot and valid_etcbs)
(revoke_cap_simple (transform_cslot_ptr slot))
(do descs \<leftarrow> gets (CSpaceAcc_A.descendants_of slot \<circ> cdt);
when (descs \<noteq> {}) (do y \<leftarrow> assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od)"
apply (rule dcorres_revoke_cap_simple_helper)
apply (simp add:gets_def)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
apply (subgoal_tac "finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'))")
apply (clarsimp simp: finite_descendants_if_from_transform valid_mdb_def
invs_def valid_state_def descendants_of_eqv)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp: when_def assert_def corres_free_fail)
apply (subgoal_tac "cte_wp_at (op \<noteq> cap.NullCap) (a,b) s'")
prefer 2
apply (erule descendants_not_null_cap [rotated])
apply fastforce
apply (rule conjI)
prefer 2
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (subgoal_tac "a \<noteq> idle_thread s'")
apply (drule_tac p="(a,b)" in caps_of_state_transform_opt_cap)
apply clarsimp
apply clarsimp
apply clarsimp
apply clarsimp
apply (erule notE, rule sym)
apply (erule (4) valid_idle_has_null_cap)
apply clarsimp
apply (rule corres_dummy_return_r)
apply (rule corres_guard_imp)
apply (rule corres_split[OF dcorres_revoke_cap_no_descendants])
apply simp
apply (rule delete_cap_simple_corres)
apply (wp cap_delete_one_cte_at)
apply (rule_tac pres1 = s' and p1 = slot in hoare_strengthen_post[OF delete_cap_one_shrink_descendants])
apply (simp_all add:invs_def valid_state_def valid_mdb_def)
apply fastforce
apply (rule conjI)
apply (rule ccontr)
apply (subgoal_tac "cte_wp_at (op\<noteq>cap.NullCap) (a,b) s")
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (drule valid_idle_has_null_cap)
apply (simp add:not_idle_thread_def)+
apply (rule invs_emptyable_descendants)
apply (simp add:invs_def valid_state_def valid_mdb_def)+
apply (clarsimp simp:finite_descendants_if_from_transform)
done
lemma valid_aep_after_reomve_slot:
"valid_aep (async_ep.WaitingAEP list) s'\<Longrightarrow>
valid_aep (case remove1 ptr list of [] \<Rightarrow> async_ep.IdleAEP | a # lista \<Rightarrow> async_ep.WaitingAEP (remove1 ptr list)) s'"
by (clarsimp simp:valid_aep_def split:async_ep.splits list.split_asm)
lemma finalise_ipc_cancel:
"dcorres dc \<top> (not_idle_thread ptr and invs and valid_etcbs)
(CSpace_D.ipc_cancel ptr)
(ipc_cancel ptr)"
apply (simp add:CSpace_D.ipc_cancel_def ipc_cancel_def get_thread_state_def thread_get_def)
apply (rule dcorres_gets_the)
apply (simp add:opt_object_tcb not_idle_thread_def transform_tcb_def, clarsimp)
apply (frule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp: opt_cap_tcb tcb_pending_op_slot_def
tcb_caller_slot_def tcb_cspace_slot_def tcb_ipcbuffer_slot_def
tcb_replycap_slot_def tcb_vspace_slot_def assert_opt_def)
apply (case_tac "tcb_state obj'")
apply (simp_all add:not_idle_thread_def infer_tcb_pending_op_def
tcb_pending_op_slot_def[symmetric] tcb_replycap_slot_def[symmetric])
apply (simp add:blocked_ipc_cancel_def)
apply (rule corres_guard_imp)
apply (rule corres_symb_exec_r)
apply (rule corres_symb_exec_r)
apply (rule corres_symb_exec_r)
apply (rule corres_dummy_return_pl)
apply (rule corres_split[ OF _ corres_dummy_set_sync_ep])
apply clarsimp
apply (rule corres_dummy_return_pr)
apply (rule corres_split [OF _ dcorres_revoke_cap_unnecessary])
apply (simp add: when_def dc_def[symmetric])
apply (rule set_thread_state_corres)
apply (wp sts_only_idle sts_st_tcb_at' valid_ep_queue_subset | clarsimp simp:not_idle_thread_def)+
apply (simp add:get_blocking_ipc_endpoint_def | wp)+
apply (clarsimp dest!:get_tcb_rev simp:invs_def )
apply (frule(1) valid_tcb_if_valid_state)
apply (clarsimp simp:valid_tcb_def valid_tcb_state_def
valid_state_def valid_pspace_def infer_tcb_pending_op_def
st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD)
apply (rule tcb_at_cte_at_2,clarsimp simp:tcb_at_def dest!:get_tcb_rev,simp)
apply (simp add:blocked_ipc_cancel_def)
apply (rule corres_guard_imp)
apply (rule corres_symb_exec_r)
apply (rule corres_symb_exec_r)
apply (rule corres_symb_exec_r)
apply (rule corres_dummy_return_pl)
apply (rule corres_split[ OF _ corres_dummy_set_sync_ep])
apply clarsimp
apply (rule corres_dummy_return_pr)
apply (rule corres_split [OF _ dcorres_revoke_cap_unnecessary])
unfolding K_bind_def
apply (rule set_thread_state_corres)
apply (wp sts_only_idle sts_st_tcb_at' valid_ep_queue_subset
| clarsimp simp:not_idle_thread_def)+
apply (simp add:get_blocking_ipc_endpoint_def | wp)+
apply (clarsimp dest!:get_tcb_rev simp:invs_def)
apply (frule(1) valid_tcb_if_valid_state)
apply (clarsimp simp:valid_tcb_def valid_tcb_state_def
valid_state_def valid_pspace_def infer_tcb_pending_op_def
st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD)
apply (rule tcb_at_cte_at_2,clarsimp simp:tcb_at_def dest!:get_tcb_rev,simp)
apply (simp add:reply_ipc_cancel_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ thread_set_fault_corres])
apply (rule corres_symb_exec_r)
apply (simp add:when_False revoke_cap_simple.simps )
apply (subst transform_tcb_slot_simp[symmetric])
apply (rule dcorres_revoke_the_cap_corres)
apply (wp thread_set_invs_trivial[OF ball_tcb_cap_casesI]
thread_set_cte_at|clarsimp)+
apply (clarsimp simp: not_idle_thread_def
tcb_at_cte_at_2[unfolded tcb_at_def])
apply (simp add:async_ipc_cancel_def)
apply (rule corres_guard_imp)
apply (rule_tac Q'="\<lambda>r. valid_aep r and op=s'" in corres_symb_exec_r)
apply (rule corres_symb_exec_r)
apply (rule corres_dummy_return_pl)
apply (rule corres_split[ OF _ corres_dummy_set_async_ep])
unfolding K_bind_def
apply (rule corres_dummy_return_pr)
apply (rule corres_split[OF _ dcorres_revoke_cap_unnecessary])
unfolding K_bind_def
apply (rule set_thread_state_corres)
apply (wp set_aep_valid_objs | clarsimp simp:not_idle_thread_def)+
apply (clarsimp simp:valid_def fail_def return_def split:async_ep.splits)+
apply (clarsimp simp:invs_def)
apply (frule(1) valid_tcb_if_valid_state)
apply (clarsimp simp:valid_tcb_def tcb_at_cte_at_2
valid_tcb_state_def invs_def valid_state_def valid_pspace_def
st_tcb_at_def generates_pending_def obj_at_def infer_tcb_pending_op_def
dest!:get_tcb_SomeD)
apply (simp add:valid_aep_after_reomve_slot)
apply (wp | clarsimp split:async_ep.splits)+
apply (clarsimp simp:invs_def, frule(1) valid_tcb_if_valid_state)
apply (clarsimp simp:valid_tcb_def tcb_at_cte_at_2 valid_tcb_state_def invs_def valid_state_def valid_pspace_def
st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD)
apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp:opt_object_tcb opt_cap_tcb)
done
lemma dcorres_get_irq_slot:
"dcorres (\<lambda>r r'. r = transform_cslot_ptr r') \<top> \<top> (gets (CSpace_D.get_irq_slot x)) (KHeap_A.get_irq_slot x)"
apply (simp add:gets_def CSpace_D.get_irq_slot_def KHeap_A.get_irq_slot_def)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp: return_def transform_def corres_underlying_def transform_cslot_ptr_def)
done
lemma dcorres_deleting_irq_handler:
"dcorres dc \<top> (invs and valid_etcbs)
(CSpace_D.deleting_irq_handler word)
(CSpace_A.deleting_irq_handler word)"
apply (simp add:CSpace_D.deleting_irq_handler_def CSpace_A.deleting_irq_handler_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ dcorres_get_irq_slot])
apply (simp, rule delete_cap_simple_corres,simp)
apply (rule hoare_vcg_precond_imp [where Q="invs and valid_etcbs"])
apply (wp |clarsimp simp:get_irq_slot_def)+
apply (rule irq_node_image_not_idle)
apply (simp add:invs_def valid_state_def)+
done
lemma do_machine_op_wp:
"\<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
\<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op mop \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>"
apply (clarsimp simp:do_machine_op_def gets_def get_def return_def bind_def select_f_def simpler_modify_def)
apply (clarsimp simp:valid_def)
apply (drule_tac x = "(machine_state s)" in spec)
apply (drule_tac x = "(a,b)" in bspec)
apply simp
apply clarsimp
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (simp add: transform_objects_def2)
done
lemmas dmo_dwp = do_machine_op_wp [OF allI]
lemma machine_op_lift[wp]:
"\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> machine_op_lift x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp:machine_rest_lift_def ignore_failure_def machine_op_lift_def)
apply wp
apply (clarsimp simp:simpler_modify_def valid_def)
apply (assumption)
apply wp
apply clarsimp
done
lemma invalidateTLB_ASID_underlying_memory[wp]:
"\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateTLB_ASID a \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp: invalidateTLB_ASID_def, wp)
done
lemma dsb_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> dsb \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp: dsb_def, wp)
done
lemma invalidate_I_PoU_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidate_I_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp: invalidate_I_PoU_def , wp)
done
lemma clean_D_PoU_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>clean_D_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp: clean_D_PoU_def , wp)
done
lemma cleanCachesPoU_underlying_memory[wp]:
"\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp: cleanCaches_PoU_def, wp)
done
lemma flush_space_dwp[wp]:
"\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> flush_space x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>"
apply (clarsimp simp:flush_space_def)
apply (wp|wpc)+
apply (clarsimp split:option.splits)
apply (rule do_machine_op_wp)
apply clarsimp
apply (wp static_imp_wp)
apply (rule do_machine_op_wp)
apply clarsimp
apply wp
apply (rule hoare_allI)
apply (rule hoare_drop_imp)
apply (rule do_machine_op_wp)
apply clarsimp
apply wp
apply (rule hoare_conjI)
apply (rule hoare_drop_imp)
apply (clarsimp simp:load_hw_asid_def)
apply wp
apply (clarsimp simp:load_hw_asid_def)
apply wp
done
lemma invalidate_asid_dwp[wp]:
"\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>x ps. transform ps = cs\<rbrace>"
apply (clarsimp simp:invalidate_asid_def)
apply wp
apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
done
lemma invalidate_asid_entry_dwp[wp]:
"\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid_entry x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>"
apply (clarsimp simp:invalidate_asid_entry_def)
apply wp
apply (clarsimp simp:invalidate_asid_def)
apply wp
apply (clarsimp simp:invalidate_hw_asid_entry_def)
apply wp
apply (subgoal_tac "transform s = cs")
prefer 2
apply (assumption)
apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
apply (clarsimp simp:load_hw_asid_def)
apply wp
apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
done
lemma invalidate_hw_asid_entry_dwp[wp]:
"\<lbrace>\<lambda>s. transform s = cs\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>"
apply (clarsimp simp:invalidate_hw_asid_entry_def)
apply wp
apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
done
lemma set_current_pd_dwp[wp]:
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setCurrentPD (Platform.addrFromPPtr x) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
by (clarsimp simp:setCurrentPD_def writeTTBR0_def isb_def dsb_def,wp)
lemma set_hardware_asid_dwp[wp]:
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setHardwareASID hw_asid \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
by (clarsimp simp:setHardwareASID_def,wp)
lemma store_hardware_asid_dwp[wp]:
"\<lbrace>\<lambda>s. transform s = cs\<rbrace> store_hw_asid a xa \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>"
apply (clarsimp simp:store_hw_asid_def)
apply wp
apply (simp add:find_pd_for_asid_assert_def)
apply wp
apply (simp add:find_pd_for_asid_def)
apply (wp|wpc)+
apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
done
lemma transform_arch_state:
"\<lbrakk> arm_globals_frame (arch_state a) = arm_globals_frame x;
arm_asid_table (arch_state a) = arm_asid_table x \<rbrakk>
\<Longrightarrow> transform (a\<lparr>arch_state := x \<rparr>) = transform a"
by (clarsimp simp:transform_def transform_objects_def2 transform_cdt_def
transform_current_thread_def transform_asid_table_def)
lemma find_free_hw_asid_dwp[wp]:
"\<lbrace>\<lambda>s. transform s = cs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>xa s. transform s = cs\<rbrace>"
apply (clarsimp simp:find_free_hw_asid_def)
apply (wp|wpc)+
apply (clarsimp simp:transform_arch_state)
apply (wp do_machine_op_wp |clarsimp simp:)+
done
lemma arch_obj_not_idle:
"\<lbrakk>valid_idle s;kheap s ptr = Some (ArchObj x )\<rbrakk> \<Longrightarrow> not_idle_thread ptr s"
by (clarsimp simp:not_idle_thread_def valid_idle_def obj_at_def st_tcb_at_def)
lemma asid_pool_at_rev:
"\<lbrakk> kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow> asid_pool_at a s"
apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def)
apply (clarsimp simp:a_type_def
split:arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits)
done
lemma asid_pool_not_idle:
"\<lbrakk> valid_idle s; asid_pool_at a s \<rbrakk> \<Longrightarrow> not_idle_thread a s"
apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def)
apply (clarsimp simp:a_type_def not_idle_thread_def
split:arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits)
done
lemma opt_object_asid_pool:
"\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow>
opt_object a (transform s) = Some (cdl_object.AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents fun\<rparr>)"
apply (frule asid_pool_at_rev)
apply (frule(1) asid_pool_not_idle)
apply (clarsimp simp:transform_objects_def opt_object_def transform_def
not_idle_thread_def restrict_map_def)
done
lemma transform_asid_pool_contents_upd:
"transform_asid_pool_contents (pool(ucast asid := pd)) =
transform_asid_pool_contents pool(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)"
apply (clarsimp simp:transform_asid_pool_contents_def transform_asid_def)
apply (rule ext)
apply (case_tac x)
apply (clarsimp simp:unat_eq_0 unat_map_def)
apply (safe | clarsimp)+
apply (safe | clarsimp simp:unat_map_def)+
apply (subst (asm) of_nat_Suc[symmetric])
apply (rule_tac P="Suc nat = unat (ucast asid)" in notE, simp)
apply (cut_tac x="Suc nat" and y="unat (ucast asid :: 10 word)" in word_unat.Abs_inject[symmetric, where 'a=10])
apply (simp add:unats_def)+
apply (rule unat_lt2p[where x="ucast asid :: 10 word", simplified])
apply simp
done
lemma dcorres_set_asid_pool:
"\<lbrakk> pool' = pool (ucast asid := pd); slot = snd (transform_asid asid);
cap = transform_asid_pool_entry pd \<rbrakk> \<Longrightarrow>
dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) a)
(KHeap_D.set_cap (a, slot) cap)
(set_asid_pool a pool')"
apply (simp add:KHeap_D.set_cap_def set_asid_pool_def get_object_def gets_the_def
gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp:obj_at_def opt_object_asid_pool assert_opt_def has_slots_def)
apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def
corres_underlying_def update_slots_def return_def object_slots_def)
apply (clarsimp simp:KHeap_A.set_object_def get_def put_def bind_def return_def)
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (drule(1) arch_obj_not_idle)
apply (rule ext)
apply (clarsimp simp:not_idle_thread_def transform_objects_def restrict_map_def map_add_def)
apply (rule transform_asid_pool_contents_upd)
done
lemma dcorres_set_vm_root:
"dcorres dc \<top> \<top> (return x) (set_vm_root rvd)"
apply (clarsimp simp: set_vm_root_def)
apply (rule dcorres_symb_exec_r)+
apply (clarsimp simp:catch_def throwError_def)
apply (rule corres_dummy_return_r)
apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]])+
apply wp
apply wpc
apply (wp do_machine_op_wp | clarsimp)+
apply (rule_tac Q = "\<lambda>_ s. transform s = cs" in hoare_post_imp)
apply simp
apply (rule hoare_pre)
apply (wp hoare_whenE_wp do_machine_op_wp [OF allI] hoare_drop_imps find_pd_for_asid_inv
| wpc | simp add: arm_context_switch_def get_hw_asid_def load_hw_asid_def if_apply_def2)+
done
lemma dcorres_delete_asid_pool:
"dcorres dc \<top> \<top>
(CSpace_D.delete_asid_pool (unat (asid_high_bits_of asid)) oid)
(ArchVSpace_A.delete_asid_pool asid oid)"
apply (simp add:CSpace_D.delete_asid_pool_def ArchVSpace_A.delete_asid_pool_def)
apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified])
apply (clarsimp simp:gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:when_def)
apply (rule conjI)
prefer 2
apply (clarsimp, rule corres_alternate2)
apply (clarsimp)
apply clarsimp
apply (rule corres_alternate1)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified])
apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified])
apply (rule corres_dummy_return_l)
apply (rule corres_underlying_split[where r'=dc and P="\<lambda>rv. \<top>" and P'="\<lambda>rv. \<top>", simplified])
prefer 2
apply clarsimp
apply (rule dcorres_absorb_get_r)
apply (rule corres_guard_imp)
apply (rule dcorres_set_vm_root)
apply clarsimp+
apply (rule corres_guard_imp[where Q=\<top> and Q'=\<top>, simplified])
apply (clarsimp simp:simpler_modify_def put_def bind_def corres_underlying_def)
apply (clarsimp simp:transform_def transform_objects_def transform_cdt_def
transform_current_thread_def)
apply (clarsimp simp:transform_asid_table_def)
apply (rule ext)
apply (clarsimp simp:unat_map_def asid_high_bits_of_def
transform_asid_table_entry_def transform_asid_def)
apply safe
apply (drule unat_cong)
apply (subst (asm) word_unat.Abs_inverse)
apply (clarsimp simp:unats_def unat_ucast)+
apply (rule mapM_wp)
apply clarsimp
apply wp
apply fastforce
apply wp
apply simp
done
lemma descendants_of_page:
"\<lbrakk>valid_mdb s;page_table_at oid s\<rbrakk>\<Longrightarrow> KHeap_D.descendants_of (oid, 0) (transform s) = {}"
apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def)
apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits)
apply (rule ccontr)
apply (clarsimp simp:valid_mdb_def dest!:not_emptyI)
apply (frule(1) cdl_cdt_parent_cte_at_lift)
apply clarsimp
apply (simp add:descendants_of_eqv cte_at_cases)
apply (clarsimp simp:transform_cslot_ptr_def)
done
lemma page_table_aligned:
"\<lbrakk>pspace_aligned s;page_table_at oid s\<rbrakk> \<Longrightarrow>
(oid && ~~ mask pt_bits) = oid"
apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def)
apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits)
apply (drule_tac x = oid in bspec)
apply clarsimp
apply (clarsimp simp:obj_bits_def arch_kobj_size_def pt_bits_def pageBits_def)
apply (simp add:is_aligned_neg_mask_eq)
done
lemma invalidateTLB_VAASID_underlying_memory[wp]:
"\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateTLB_VAASID word \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp: invalidateTLB_VAASID_def, wp)
done
lemma dcorres_flush_page:
"dcorres dc \<top> \<top> (return x) (flush_page aa a b word)"
apply (rule corres_dummy_return_r)
apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]])
apply wp
apply (simp add:flush_page_def)
apply wp
apply (rule dcorres_to_wp[OF dcorres_set_vm_root])
apply wp
apply clarsimp
apply (wp do_machine_op_wp, clarsimp)
apply (wp)
apply (simp add:load_hw_asid_def)
apply wp
apply (clarsimp simp:set_vm_root_for_flush_def)
apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+
apply (wpc)
apply wp
apply (rule hoare_conjI,rule hoare_drop_imp)
apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+
apply (wpc|wp)+
apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post)
apply (wp|clarsimp)+
done
lemma dcorres_flush_table:
"dcorres dc \<top> \<top> (return x) (flush_table aa a b word)"
apply (rule corres_dummy_return_r)
apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]])
apply wp
apply (simp add:flush_table_def)
apply wp
apply (rule dcorres_to_wp[OF dcorres_set_vm_root])
apply wp
apply clarsimp
apply (wp do_machine_op_wp|clarsimp)+
apply (clarsimp simp:load_hw_asid_def)
apply wp
apply (clarsimp simp:set_vm_root_for_flush_def)
apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+
apply wpc
apply wp
apply (rule hoare_conjI,rule hoare_drop_imp)
apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+
apply (wpc|wp)+
apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post)
apply (wp|clarsimp)+
done
lemma flush_table_exec:
"\<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow>dcorres dc R P h ((flush_table aa a b word) >>= g)"
apply (rule corres_dummy_return_pl)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ dcorres_flush_table])
apply (simp|wp)+
done
lemma transform_cap_not_new_invented:
"transform_cap z \<noteq> cdl_cap.PageTableCap word Fake asid"
by (auto simp:transform_cap_def split:arch_cap.splits cap.splits)
lemma page_table_not_idle:
"\<lbrakk>valid_idle s;page_table_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s"
apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def)
apply (clarsimp simp:a_type_def not_idle_thread_def
split:arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits)
done
lemma page_directory_not_idle:
"\<lbrakk>valid_idle s;page_directory_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s"
apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def)
apply (clarsimp simp:a_type_def not_idle_thread_def
split:arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits)
done
lemma page_table_at_rev:
"\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> page_table_at a s"
apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def)
apply (clarsimp simp:a_type_def
split:arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits)
done
lemma page_directory_at_rev:
"\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> \<Longrightarrow> page_directory_at a s"
apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def)
apply (clarsimp simp:a_type_def
split:arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits)
done
lemma mask_pd_bits_less':
"uint ((ptr::word32) && mask pd_bits >> (2\<Colon>nat)) < (4096\<Colon>int)"
apply (clarsimp simp:pd_bits_def pageBits_def)
using shiftr_less_t2n'[where m = 12 and x ="(ptr && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
apply (clarsimp simp:mask_twice )
done
lemma mask_pd_bits_less:
"nat (uint ((y::word32) && mask pd_bits >> 2)) < 4096"
apply (clarsimp simp:pd_bits_def pageBits_def)
apply (rule iffD2[OF nat_less_eq_zless[where z = 4096,simplified]])
apply (simp)
using shiftr_less_t2n'[where m = 12 and x ="(y && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
apply (clarsimp simp:mask_twice)
done
lemma mask_pt_bits_less':
"uint (((ptr::word32) && mask pt_bits) >> 2)< 256"
apply (clarsimp simp:pt_bits_def pageBits_def)
using shiftr_less_t2n'[where m = 8 and x ="(ptr && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
apply (clarsimp simp:mask_twice )
done
lemma mask_pt_bits_less:
"nat (uint ((y::word32) && mask pt_bits >> 2)) < 256"
apply (clarsimp simp:pt_bits_def pageBits_def)
apply (rule iffD2[OF nat_less_eq_zless[where z = 256,simplified]])
apply (simp)
using shiftr_less_t2n'[where m = 8 and x ="(y && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
apply (clarsimp simp:mask_twice)
done
definition pd_pt_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_pt_relation pd pt offset s \<equiv>
\<exists>fun u v ref. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> page_table_at pt s \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_Structs_A.pde.PageTablePDE ref u v
\<and> pt = Platform.ptrFromPAddr ref )"
definition pd_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_section_relation pd pt offset s \<equiv>
\<exists>fun u v ref1 ref2. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_Structs_A.pde.SectionPDE ref1 u ref2 v
\<and> pt = Platform.ptrFromPAddr ref1 )"
definition pd_super_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_super_section_relation pd pt offset s \<equiv>
\<exists>fun u v ref1. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_Structs_A.pde.SuperSectionPDE ref1 u v
\<and> pt = Platform.ptrFromPAddr ref1 )"
definition pt_page_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>vmpage_size set\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pt_page_relation pt page offset S s \<equiv>
\<exists>fun. (kheap s pt = Some (ArchObj (arch_kernel_obj.PageTable fun)))
\<and> (case fun (ucast (offset && mask pt_bits >> 2)) of
ARM_Structs_A.pte.LargePagePTE ref fun1 fun2 \<Rightarrow>
page = Platform.ptrFromPAddr ref \<and> ARMLargePage \<in> S
| ARM_Structs_A.pte.SmallPagePTE ref fun1 fun2 \<Rightarrow>
page = Platform.ptrFromPAddr ref \<and> ARMSmallPage \<in> S
| _ \<Rightarrow> False)"
lemma slot_with_pt_frame_relation:
"\<lbrakk>valid_idle s;pt_page_relation a oid y S s\<rbrakk>\<Longrightarrow>
(a, nat (uint (y && mask pt_bits >> 2))) \<in>
((slots_with (\<lambda>x. \<exists>rights sz asid. x = FrameCap oid rights sz Fake asid)) (transform s))"
apply (clarsimp simp:pt_page_relation_def)
apply (frule page_table_at_rev)
apply (frule(1) page_table_not_idle)
apply (clarsimp simp:slots_with_def transform_def transform_objects_def restrict_map_def)
apply (clarsimp simp:not_idle_thread_def has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def)
apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] )
apply (clarsimp simp:mask_pt_bits_less split:ARM_Structs_A.pte.split_asm)
done
lemma below_kernel_base:
"ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
\<Longrightarrow> kernel_pde_mask f (of_nat (unat (y && mask pd_bits >> 2)))
= f (of_nat (unat (y && mask pd_bits >> 2)))"
apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )
apply (simp add:ucast_nat_def[symmetric] unat_def)
done
lemma slot_with_pd_pt_relation:
"\<lbrakk>valid_idle s; pd_pt_relation a b y s; ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
(a, unat (y && mask pd_bits >> 2)) \<in>
(slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap b Fake asid)) (transform s)"
apply (clarsimp simp :pd_pt_relation_def)
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
apply (clarsimp simp:restrict_map_def a_type_def page_table_not_idle not_idle_thread_def pt_bits_def
split:Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp:has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (clarsimp simp:ucast_def)
apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def below_kernel_base)
apply (simp add:mask_pd_bits_less)
done
lemma slot_with_pd_section_relation:
"\<lbrakk>valid_idle s; pd_super_section_relation a b y s \<or> pd_section_relation a b y s;
ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
(a, unat (y && mask pd_bits >> 2)) \<in>
(slots_with (\<lambda>x. \<exists>rights sz asid. x = cdl_cap.FrameCap b rights sz Fake asid)) (transform s)"
apply (erule disjE)
apply (clarsimp simp :pd_super_section_relation_def)
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
apply (clarsimp simp:restrict_map_def a_type_def page_table_not_idle not_idle_thread_def pt_bits_def
split:Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp:has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (clarsimp simp:ucast_def)
apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def mask_pd_bits_less)
apply (clarsimp simp :pd_section_relation_def)
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
apply (clarsimp simp:restrict_map_def a_type_def page_table_not_idle not_idle_thread_def pt_bits_def
split:Structures_A.kernel_object.split_asm if_splits arch_kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp:has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (clarsimp simp:ucast_def)
apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def)
apply (simp add:mask_pd_bits_less)
done
lemma opt_cap_page_table:"\<lbrakk>valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
(opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s))
= Some (cdl_cap.PageTableCap pt_id Fake None)"
apply (clarsimp simp:pd_pt_relation_def opt_cap_def transform_def unat_def slots_of_def opt_object_def)
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
restrict_map_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def unat_def[symmetric] unat_map_def | rule conjI )+
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def)
apply (clarsimp simp:below_kernel_base)
apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] unat_def ucast_def)
apply (simp add:mask_pd_bits_less unat_def)
done