-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathKHeap_DR.thy
3528 lines (3278 loc) · 167 KB
/
KHeap_DR.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory KHeap_DR
imports Intent_DR
begin
context begin interpretation Arch . (*FIXME: arch-split*)
declare arch_post_cap_deletion_def[simp]
lemmas post_cap_deletion_simps[simp] = post_cap_deletion_def[simplified arch_post_cap_deletion_def]
declare arch_mask_irq_signal_def[simp]
lemma nat_bl_to_bin_surj:
"\<exists>bl. n = nat (bl_to_bin bl)"
using n_less_equal_power_2[where n=n, folded of_nat_less_iff, simplified]
apply (rule_tac x="bin_to_bl n (int n)" in exI)
apply (simp only: bin_bl_bin bintrunc_mod2p)
apply simp
done
lemma transform_tcb_slot_0:
"transform_cslot_ptr (a, tcb_cnode_index 0) = (a,tcb_cspace_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_cspace_slot_def)
apply (simp add: tcb_cnode_index_def bl_to_bin_def)
done
lemma transform_tcb_slot_1:
"transform_cslot_ptr (a,tcb_cnode_index 1) = (a,tcb_vspace_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_vspace_slot_def)
apply (simp add: tcb_cnode_index_def)
done
lemma transform_tcb_slot_2:
"transform_cslot_ptr (a,tcb_cnode_index 2) = (a,tcb_replycap_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_replycap_slot_def)
apply (simp add: tcb_cnode_index_def)
apply (simp add:bl_to_bin_def)
done
lemma transform_tcb_slot_3:
"transform_cslot_ptr (a,tcb_cnode_index 3) = (a,tcb_caller_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_caller_slot_def)
apply (simp add: tcb_cnode_index_def)
apply (simp add:bl_to_bin_def)
done
lemma transform_tcb_slot_4:
"transform_cslot_ptr (a,tcb_cnode_index 4) = (a,tcb_ipcbuffer_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_ipcbuffer_slot_def)
apply (simp add: tcb_cnode_index_def)
apply (simp add:bl_to_bin_def)
done
lemmas transform_tcb_slot_simp =
transform_tcb_slot_0 transform_tcb_slot_1
transform_tcb_slot_2 transform_tcb_slot_3
transform_tcb_slot_4
lemma cap_table_at_cte_wp_at_length:
"\<lbrakk> cap_table_at n p s; cte_wp_at P (p, p') s \<rbrakk>
\<Longrightarrow> length p' = n"
by (auto simp: cte_wp_at_cases obj_at_def is_cap_table well_formed_cnode_n_def length_set_helper)
context
begin
(* avoid spurious warning in termination proof below *)
declare CSpace_D.resolve_address_bits.simps [simp del]
termination CSpace_D.resolve_address_bits
by (relation "measure (\<lambda>(a,b,c). c)") (clarsimp simp:in_monad)+
end
crunch
"KHeap_D.set_cap", "PageTableUnmap_D.cancel_all_ipc", "PageTableUnmap_D.unbind_maybe_notification"
for cdl_cdt [wp]: "\<lambda>s. P (cdl_cdt s)"
(wp: crunch_wps simp: crunch_simps)
lemma descendants_cdl_cdt_lift:
"(\<And>P. \<lbrace>\<lambda>s. P (cdl_cdt s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cdl_cdt s)\<rbrace>) \<Longrightarrow>
\<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace> f \<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s)\<rbrace>"
apply (simp add: KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def
KHeap_D.is_cdt_parent_def)
apply assumption
done
lemma fast_finalise_descendants:
"\<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace>
PageTableUnmap_D.fast_finalise cap fin
\<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s) \<rbrace>"
apply (cases cap, simp_all)
apply (wp descendants_cdl_cdt_lift|simp)+
done
lemmas set_cap_descendants = descendants_cdl_cdt_lift [OF KHeap_D_set_cap_cdl_cdt]
lemma removed_descendants_subset:
assumes slot: "slot \<in> KHeap_D.descendants_of p s"
defines "s' \<equiv> s\<lparr>cdl_cdt :=
\<lambda>x. if x = slot
then None
else if cdl_cdt s x = Some slot
then cdl_cdt s slot
else cdl_cdt s x\<rparr>"
shows "KHeap_D.descendants_of p s' \<subset> KHeap_D.descendants_of p s" (is "?new \<subset> ?old")
proof
have "slot \<notin> ?new"
apply (clarsimp simp: KHeap_D.descendants_of_def)
apply (erule tranclE)
apply (clarsimp simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def)
apply (clarsimp simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def)
done
with slot show "?new \<noteq> ?old" by auto
{ fix p' assume p': "p' \<in> ?new"
then
have "p' \<in> ?old"
unfolding KHeap_D.descendants_of_def
apply clarsimp
apply (induct rule: trancl_induct)
apply (fastforce simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def
split: if_split_asm
intro: trancl_trans)
apply (erule trancl_trans)
apply (fastforce simp: KHeap_D.cdt_parent_rel_def KHeap_D.is_cdt_parent_def s'_def
split: if_split_asm
intro: trancl_trans)
done
}
thus "?new \<subseteq> ?old" by auto
qed
lemma always_empty_slot_card:
"\<lbrace>\<lambda>s'. s' = s \<and> slot \<in> KHeap_D.descendants_of x s' \<and>
finite (KHeap_D.descendants_of x s') \<rbrace>
always_empty_slot slot
\<lbrace>\<lambda>_ s'. card (KHeap_D.descendants_of x s') < card (KHeap_D.descendants_of x s)\<rbrace>"
apply (clarsimp simp: always_empty_slot_def remove_parent_def)
apply (wp set_cap_descendants)
apply clarsimp
apply (erule psubset_card_mono)
apply (erule removed_descendants_subset)
done
termination revoke_cap_simple
apply (relation "measure (\<lambda>(a,b). card (KHeap_D.descendants_of a b))")
apply (rule wf_measure)
apply (simp add: in_monad select_def)
apply (clarsimp simp: delete_cap_simple_def in_monad gets_the_def)
apply (clarsimp simp: PageTableUnmap_D.is_final_cap_def in_monad)
apply (drule use_valid,
rule_tac P="(=) (KHeap_D.descendants_of (a,b) s)" in
fast_finalise_descendants,
rule refl)
apply clarsimp
apply (drule use_valid, rule always_empty_slot_card)
apply (rule conjI, rule refl)
apply (erule conjI)
apply assumption
apply simp
done
declare revoke_cap_simple.simps [simp del]
declare KHeap_DR.resolve_address_bits.simps [simp del]
lemma dcorres_revoke_cap_simple_helper:
"\<lbrakk> dcorres r P P'
(do descendants \<leftarrow> gets $ KHeap_D.descendants_of victim;
assert (finite descendants);
non_null \<leftarrow> gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
non_null_descendants \<leftarrow> return (descendants \<inter> non_null);
if non_null_descendants \<noteq> {}
then do a \<leftarrow> select non_null_descendants;
y \<leftarrow> delete_cap_simple a;
revoke_cap_simple victim
od
else return ()
od)
h \<rbrakk> \<Longrightarrow> dcorres r P P' (revoke_cap_simple victim) h"
apply (rule corres_dummy_get_pl)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp:corres_underlying_def)
apply (rename_tac s' a b)
apply (subst revoke_cap_simple.simps)
apply (erule_tac x=s' in allE, simp)
apply (clarsimp cong: if_cong)
apply (drule_tac x="(a,b)" in bspec)
apply simp
apply clarsimp
done
lemma valid_irq_node_cte_at_irq_slot:
"valid_irq_node s \<Longrightarrow> cte_at (interrupt_irq_node s x,[]) s"
apply (clarsimp simp:valid_irq_node_def)
apply (drule_tac x = x in spec)
apply (clarsimp simp:obj_at_def is_cap_table_def)
apply (clarsimp split: Structures_A.kernel_object.splits
simp: cte_wp_at_cases well_formed_cnode_n_def)
apply auto
done
lemma transform_cslot_ptr_inj:
"\<lbrakk> cte_at p s; cte_at p' s \<rbrakk> \<Longrightarrow>
(transform_cslot_ptr p = transform_cslot_ptr p') = (p = p')"
apply (clarsimp simp: transform_cslot_ptr_def
bl_to_bin_ge0 eq_nat_nat_iff split_def
valid_irq_node_def)
apply (cases p, cases p')
apply (safe, simp_all)
apply (drule bl_to_bin_inj)
apply (erule(1) cte_at_cref_len)
apply simp
done
lemma transform_cdt_slot_inj_on_cte_at:
"\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> cte_wp_at P x s \<rbrakk> \<Longrightarrow>
inj_on (transform_cslot_ptr) S"
apply (rule inj_onI)
apply (subst(asm) transform_cslot_ptr_inj, simp_all)
apply (fastforce simp: cte_wp_at_caps_of_state)+
done
lemma get_cur_thread_corres:
"dcorres (\<lambda>rv rv'. rv = rv') \<top>
(\<lambda>s. not_idle_thread (cur_thread s) s)
(gets_the cdl_current_thread)
(gets cur_thread)"
apply (simp add:gets_the_def gets_def)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_opt_def transform_def transform_current_thread_def)
apply (simp add:corres_underlying_def not_idle_thread_def)
done
lemma not_in_dom_dest:
"\<lbrakk>dom f = P; f x = None\<rbrakk> \<Longrightarrow> x\<notin> P"
by (clarsimp simp:dom_def)
lemma in_dom_dest:
"\<lbrakk>dom f = P; f x \<noteq> None\<rbrakk> \<Longrightarrow> x\<in> P"
by (clarsimp simp:dom_def)
lemma nat_to_bl_dest:
"b\<in>Collect (%x. length x= n)\<Longrightarrow> nat_to_bl n (nat (bl_to_bin b)) = Some b"
apply (unfold nat_to_bl_def)
apply (subgoal_tac "0 \<le> bl_to_bin b")
apply (subst nat_0_le)
apply simp
apply (subgoal_tac "length b = n")
apply (erule subst[where s="length b" and t=n])
apply (subst bl_bin_bl)
apply (simp add: not_le)
apply (clarsimp simp: bl_to_bin_lt2p)
apply clarsimp
apply (simp add:not_less)
apply (rule bl_to_bin_ge0)
done
lemma bl_to_bin_tcb_cnode_index_le0:
"n < 8 \<Longrightarrow> (bl_to_bin (tcb_cnode_index n) \<le> 0) = (n = 0)"
by (simp add: tcb_cnode_index_def uint_nat unat_of_nat)
lemma nat_bl_to_bin_lt2p: "nat(bl_to_bin b) < 2 ^ length b"
apply (rule iffD2[OF nat_less_iff[OF bl_to_bin_ge0]])
apply (simp add:bl_to_bin_lt2p)
done
lemma caps_of_state_transform_opt_cap:
"\<lbrakk> caps_of_state s p = Some cap; valid_etcbs s;
fst p \<noteq> idle_thread s \<rbrakk>
\<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s)
= Some (transform_cap cap)"
apply (frule caps_of_state_cteD)
apply (cases p)
apply (erule cte_wp_atE)
apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def
slots_of_def transform_objects_def
transform_def object_slots_def
transform_cnode_contents_def well_formed_cnode_n_def
split: nat.splits)
apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI])
apply (simp add: option_map_join_def nat_to_bl_dest)
apply (fastforce simp: nat_to_bl_def split: nat.splits)
apply (frule(1) valid_etcbs_tcb_etcb)
apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def slots_of_def
transform_def transform_objects_def object_slots_def
valid_irq_node_def obj_at_def is_cap_table_def
transform_tcb_def tcb_slots tcb_cap_cases_def
bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
split: if_split_asm)
done
lemma cap_slot_cnode_property_lift:
"\<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; b\<in> dom cs\<rbrakk>
\<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s')) =
(case (cs b) of None \<Rightarrow> None | Some y \<Rightarrow> Some (transform_cap y))"
apply clarsimp
apply (subgoal_tac "cte_wp_at ((=) y) (a, b) s'")
apply (subst caps_of_state_transform_opt_cap, simp_all)
apply (simp add: cte_wp_at_caps_of_state)
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
apply (rule cte_wp_at_cteI, fastforce, simp+)
done
lemma get_cap_no_fail:
"dcorres r P (P' and cte_at slot) f (get_cap slot>>=h) \<Longrightarrow> dcorres r P P' f (get_cap slot>>=h)"
apply (rule dcorres_expand_pfx)
apply (case_tac "cte_at slot s'")
apply (drule dcorres_absorb_pfx)
apply simp+
apply (case_tac slot)
apply (simp(no_asm) add:get_cap_def[simplified tcb_cnode_map_def])
apply (clarsimp simp:bind_assoc get_object_def gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp: assert_def corres_free_fail)
apply (case_tac y)
apply (simp_all add:corres_free_fail assert_def cte_at_cases)
apply (rule impI)
apply (simp add:dom_def assert_opt_def corres_free_fail)
apply (simp add:assert_opt_def corres_free_fail)
apply auto
done
lemma get_cap_helper:
"dcorres r P (P') f (get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and (cte_wp_at ((=) cap) slot)) f (g cap)"
by (clarsimp simp:bind_def corres_underlying_def cte_wp_at_def)
lemma get_cap_corres:
"ptr' = transform_cslot_ptr ptr \<Longrightarrow>
dcorres (\<lambda>rv rv'. rv = transform_cap rv') \<top>
(valid_idle and not_idle_thread (fst ptr) and valid_etcbs)
(KHeap_D.get_cap ptr')
(CSpaceAcc_A.get_cap ptr)"
apply (case_tac ptr)
apply (clarsimp simp:CSpaceAcc_A.get_cap_def[simplified tcb_cnode_map_def]
gets_def get_object_def gets_the_def bind_assoc)
apply (rule dcorres_get)
apply (clarsimp simp:assert_def corres_free_fail assert_opt_def)
apply (case_tac y)
apply (simp_all add:assert_def corres_free_fail)
apply (rename_tac nat "fun")
apply (case_tac "fun b")
apply (simp add:corres_free_fail)
apply clarsimp
apply (drule (2) cap_slot_cnode_property_lift, simp, fastforce)
apply simp
apply (clarsimp simp:transform_tcb_slot_simp[simplified])
apply (drule get_tcb_rev)
apply (drule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp:lift_simp not_idle_thread_def)
done
definition
opt_cap_wp_at :: "(cdl_cap \<Rightarrow> bool) \<Rightarrow> (cdl_object_id \<times> nat) \<Rightarrow> cdl_state \<Rightarrow> bool"
where
"opt_cap_wp_at P slot s \<equiv> \<exists>cap. fst (KHeap_D.get_cap slot s) = {(cap, s)} \<and> P cap"
lemma opt_cap_wp_at_def':
"opt_cap_wp_at P slot s = (case (opt_cap slot s) of Some a \<Rightarrow> P a | _ \<Rightarrow> False) "
apply (clarsimp simp:opt_cap_wp_at_def opt_cap_def gets_the_def gets_def get_def return_def assert_opt_def bind_def)
apply (auto simp:fail_def return_def split:option.splits)
done
lemma nat2p: "nat (2^(x::nat)) = 2^(x::nat)"
by (rule nat_int.Rep_inverse',simp)
lemma nat_to_bl_to_bin:
"nat_to_bl bits n = Some xs \<Longrightarrow> n = nat (bl_to_bin xs)"
by (clarsimp simp:nat_to_bl_def bin_bl_bin' bintrunc_mod2p split: if_split_asm)
lemma cap_counts_inv:
assumes "\<And>cap. P cap\<Longrightarrow> cap_counts cap"
shows "\<lbrakk>opt_cap_wp_at P slot (transform s);valid_objs s; valid_etcbs s\<rbrakk>
\<Longrightarrow> \<exists>slot'. slot = transform_cslot_ptr slot' \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) slot' s"
apply (clarsimp simp:opt_cap_wp_at_def' split:option.splits)
apply (case_tac slot)
apply (rename_tac ptr offset)
apply (clarsimp simp:slots_of_def KHeap_D.opt_cap_def transform_def split:option.splits)
apply (rule_tac x = ptr in exI)
apply (clarsimp simp:transform_objects_def restrict_map_Some_iff object_slots_def split:cdl_object.splits)
apply (frule assms)
apply (clarsimp simp: cte_wp_at_cases transform_object_def transform_tcb_def
tcb_pending_op_slot_def tcb_boundntfn_slot_def
split: Structures_A.kernel_object.splits nat.splits if_splits
| drule(1) valid_etcbs_tcb_etcb)+
apply (clarsimp simp: cap_counts_def infer_tcb_bound_notification_def split:option.splits)
apply (clarsimp simp:cap_counts_def infer_tcb_pending_op_def split:Structures_A.thread_state.splits nat.splits)
using transform_tcb_slot_simp[simplified,symmetric]
apply (rule_tac x= "tcb_cnode_index 4" in exI)
apply (clarsimp)
using transform_tcb_slot_simp[simplified,symmetric]
apply (rule_tac x= "tcb_cnode_index 3" in exI)
apply (clarsimp)
using transform_tcb_slot_simp[simplified,symmetric]
apply (rule_tac x= "tcb_cnode_index 2" in exI)
apply (clarsimp)
using transform_tcb_slot_simp[simplified,symmetric]
apply (rule_tac x= "tcb_cnode_index 1" in exI)
apply (clarsimp)
using transform_tcb_slot_simp[simplified,symmetric]
apply (rule_tac x= "tcb_cnode_index 0" in exI)
apply (clarsimp)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj,simp_all)
apply (simp_all add:object_slots_def transform_object_def)
apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
split:option.splits Structures_A.kernel_object.splits nat.splits)
apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits)
apply (rule_tac x = x2b in exI,simp add: nat_to_bl_to_bin)
apply (drule(1) valid_etcbs_tcb_etcb, simp)
prefer 6 (* IRQ Node *)
apply (clarsimp split: Structures_A.kernel_object.splits nat.splits option.splits)
apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
split:option.splits Structures_A.kernel_object.splits nat.splits)
apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits)
apply (rule_tac x = x2a in exI,simp add: nat_to_bl_to_bin)
apply (frule assms)
apply ((simp_all add:Let_def cap_counts_def transform_tcb_def
split:option.splits if_splits arch_kernel_obj.splits
Structures_A.kernel_object.splits cdl_object.splits nat.splits|
drule(1) valid_etcbs_tcb_etcb |
clarsimp simp: unat_map_def transform_page_table_contents_def cap_counts_def
transform_page_directory_contents_def transform_asid_pool_contents_def
transform_pte_def transform_pde_def transform_asid_pool_entry_def
split:option.splits if_splits ARM_A.pte.splits ARM_A.pde.splits
dest!:assms)+)
done
lemma eqset_imp': "A = B \<Longrightarrow> \<forall>x. ((x\<in> A) = (x\<in> B))" by simp
lemma eq_singleton_set: "\<lbrakk>A = f` B; \<forall>x\<in>B. \<forall>y\<in> B. x\<noteq> y \<longrightarrow> f x\<noteq> f y \<rbrakk>\<Longrightarrow> (\<exists>a. A = {a}) = (\<exists>b. B = {b})"
apply (subgoal_tac "card A = card B")
apply (auto simp: trans[OF eq_commute card_Suc_eq])[1]
apply (metis card_image inj_onI)
done
lemma final_cap_set_map:
"\<lbrakk>valid_idle s'; valid_irq_node s';valid_objs s';if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'\<rbrakk>
\<Longrightarrow> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap'
\<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')}
= transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}"
apply (rule set_eqI)
apply (rule iffI)
apply (clarsimp simp: image_def)
apply (drule cap_counts_inv[rotated])
apply simp+
apply clarsimp
apply (rule_tac x=aa in exI)
apply (rule_tac x=ba in exI)
apply simp+
apply (erule cte_wp_at_weakenE_customised)
(*defer till the otherway around comes up*)
defer
apply (clarsimp simp:image_def opt_cap_wp_at_def')
apply (drule iffD1[OF cte_wp_at_caps_of_state])
apply clarsimp
apply (frule caps_of_state_transform_opt_cap, simp)
apply clarsimp
apply (frule valid_idle_has_null_cap)
(*It is true since idle thread should not get any cap installed *)
apply simp+
apply (thin_tac "opt_cap x y = Q" for x y Q)
by (auto simp: transform_cap_def cap_has_object_def cap_counts_def cdl_cap_irq_def
split: cap.splits arch_cap.splits if_split_asm)
lemma opt_cap_wp_at_ex_opt_cap:
"opt_cap_wp_at P p s = (\<exists>cap'. opt_cap p s = Some cap' \<and> P cap')"
by (simp add: opt_cap_wp_at_def' split: option.split)
lemma is_final_cap_corres:
"\<lbrakk>cdl_cap = transform_cap cap;cap\<noteq> cap.NullCap\<rbrakk>
\<Longrightarrow> dcorres ((=)) \<top> (valid_objs and valid_irq_node and valid_idle and if_unsafe_then_cap and valid_global_refs and valid_etcbs)
(PageTableUnmap_D.is_final_cap (cdl_cap))
(IpcCancel_A.is_final_cap (cap))"
apply (clarsimp simp: IpcCancel_A.is_final_cap_def PageTableUnmap_D.is_final_cap_def)
apply (clarsimp simp: IpcCancel_A.is_final_cap'_def PageTableUnmap_D.is_final_cap'_def)
apply (subst cte_wp_at_def[symmetric])
apply (subst opt_cap_wp_at_ex_opt_cap[symmetric])
apply (rule iffI)
apply clarsimp
apply (drule final_cap_set_map)
apply (simp+)[6] (* sseefried: Brittle proof! May need to change number there *)
apply (drule eq_singleton_set)
apply (clarsimp)
apply (subst(asm) transform_cslot_ptr_inj, (erule cte_wp_at_cte_at)+)
apply simp
apply (clarsimp simp: gen_obj_refs_Int)
apply (rule context_conjI[rotated])
apply clarsimp
apply (drule final_cap_set_map)
apply (simp+)[6] (* sseefried: Brittle proof! May need to change number there *)
apply (drule eq_singleton_set)
apply (clarsimp simp: gen_obj_refs_Int)
apply (clarsimp simp: gen_obj_refs_Int)
apply (clarsimp|drule_tac x = "(a,b)" in eqset_imp_iff)+
apply (clarsimp simp:cte_wp_at_cases)
apply (case_tac cap)
apply (clarsimp simp:cap_counts_def transform_cap_def gen_obj_refs_Int)+
apply (clarsimp split:arch_cap.splits cap.splits)
done
lemma dcorres_exec_is_final_cap:
assumes c: "\<And>final. dcorres r (P final) P' (f final) f'"
shows "dcorres r (\<lambda>s. P (PageTableUnmap_D.is_final_cap' cap s) s) P' (PageTableUnmap_D.is_final_cap cap >>= f) f'"
unfolding PageTableUnmap_D.is_final_cap_def
apply (rule corres_underlying_gets_pre_lhs)
apply (rule c)
done
lemma set_original_dummy_corres:
"dcorres dc \<top> \<top> (return a) (set_original slot tag)"
apply (clarsimp simp:set_original_def gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:return_def simpler_modify_def corres_underlying_def)
apply (clarsimp simp:transform_def transform_current_thread_def)
done
lemma corres_dummy_set_notification:
"dcorres dc \<top> \<top> (return a) (set_notification epptr b)"
apply (simp add: set_simple_ko_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp: corres_free_fail assert_def a_type_def
split: option.splits Structures_A.kernel_object.splits)
apply (rule corres_free_set_object)
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (subst transform_objects_update_kheap_same_caps)
apply (simp add: transform_objects_update_same)+
done
lemma corres_dummy_set_sync_ep:
"dcorres dc \<top> \<top> (return a) (set_endpoint epptr b)"
apply (simp add: set_simple_ko_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp: corres_free_fail assert_def a_type_def partial_inv_def
split: option.splits Structures_A.kernel_object.splits)
apply (rule corres_free_set_object)
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (subst transform_objects_update_kheap_same_caps)
apply (simp add: transform_objects_update_same)+
done
lemma thread_set_fault_corres:
assumes r: "\<And>t. f (tcb_has_fault (t::Structures_A.tcb)) = (case (ft (tcb_fault t)) of None \<Rightarrow> False | _ \<Rightarrow> True)"
shows "dcorres dc \<top> (tcb_at thread and not_idle_thread thread and valid_etcbs) (update_thread_fault thread f )
(thread_set (tcb_fault_update ft) thread)"
apply (clarsimp simp:thread_set_def update_thread_fault_def)
apply (rule dcorres_gets_the)
apply (simp_all)
apply (clarsimp, drule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp:opt_object_tcb not_idle_thread_def transform_tcb_def)
apply (rule dcorres_set_object_tcb)
apply (clarsimp simp: transform_tcb_def tcb_at_def cong: transform_full_intent_cong
dest!: get_tcb_SomeD get_etcb_SomeD )
apply (cut_tac t = obj' in r)
apply (clarsimp split:option.splits)
apply ((clarsimp simp:opt_object_tcb tcb_at_def get_etcb_def dest!:get_tcb_SomeD get_etcb_SomeD)+)[3]
apply (clarsimp, drule(1) valid_etcbs_get_tcb_get_etcb, clarsimp simp:opt_object_tcb not_idle_thread_def get_etcb_def)
done
lemma get_object_corres:
"ptr = ptr' \<Longrightarrow>
dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv')
\<top> (not_idle_thread ptr' and obj_at (Not o is_tcb) ptr')
(KHeap_D.get_object ptr) (KHeap_A.get_object ptr')"
apply (clarsimp simp: KHeap_A.get_object_def gets_the_def)
apply (rule corres_underlying_split[OF _ _ gets_sp gets_sp, where r'=dc])
apply simp
apply (clarsimp simp: assert_def corres_free_fail split: if_split)
apply (rule_tac F="rv = Some (transform_object undefined 0 etcb' y)" in corres_req)
apply (simp_all add: assert_opt_def)
apply (clarsimp simp: transform_def transform_objects_def
not_idle_thread_def obj_at_def)
apply (clarsimp simp: transform_object_def
split: Structures_A.kernel_object.splits)
done
lemma nat_to_bl_id2:
shows "nat_to_bl (length p) (nat (bl_to_bin p)) = Some p"
unfolding nat_to_bl_def
by (simp add: not_le bl_to_bin_ge0 bl_to_bin_lt2p nat_less_iff del: bin_to_bl_def)
lemma xf_cnode_contents:
"\<lbrakk> well_formed_cnode_n sz cn; cn p = Some cap \<rbrakk> \<Longrightarrow>
transform_cnode_contents sz cn (nat (bl_to_bin p)) = Some (transform_cap cap)"
unfolding transform_cnode_contents_def
apply clarsimp
apply (frule (1) wf_cs_nD [symmetric], simp)
apply (simp add: nat_to_bl_id2 word_bits_conv option_map_join_simps option_map_join_def)
done
lemma transform_cnode_contents_upd:
"\<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow>
(transform_cnode_contents sz cn)(nat (bl_to_bin sl') \<mapsto> transform_cap cap') =
transform_cnode_contents sz (cn(sl' \<mapsto> cap'))"
apply (rule ext)
apply clarsimp
apply (rule conjI)
prefer 2
apply (clarsimp simp: transform_cnode_contents_def option_map_def
option_map_join_def nat_to_bl_to_bin
split: option.splits)
apply (clarsimp simp: transform_cnode_contents_def option_map_def
option_map_join_def
split: option.splits)
apply (frule (1) wf_cs_nD [symmetric])
apply (simp add: nat_to_bl_id2)
done
lemma caps_of_state_cnode_upd:
"\<lbrakk> kheap s p' = Some (CNode sz cn); well_formed_cnode_n sz cn;
cn sl' = Some ocap' \<rbrakk> \<Longrightarrow>
caps_of_state (update_kheap ((kheap s)(p' \<mapsto> CNode sz (cn(sl' \<mapsto> cap')))) s) =
(caps_of_state s) ((p',sl') \<mapsto> cap')"
apply (rule ext)
apply (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases wf_cs_upd)
done
lemma caps_of_state_cnode:
"\<lbrakk> kheap s p = Some (CNode sz cn); well_formed_cnode_n sz cn; cn sl = Some cap \<rbrakk> \<Longrightarrow>
caps_of_state s (p, sl) = Some cap"
by (simp add: caps_of_state_cte_wp_at cte_wp_at_cases)
lemma cdl_objects_tcb:
"\<lbrakk>kheap s' p = Some (TCB tcb); ekheap s' p = Some etcb; p \<noteq> idle_thread s'\<rbrakk>
\<Longrightarrow> cdl_objects (transform s') p =
Some (Tcb \<lparr>cdl_tcb_caps =
[tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb),
tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb),
tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb),
tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb),
tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb),
tcb_pending_op_slot \<mapsto> infer_tcb_pending_op p (tcb_state tcb),
tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)],
cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb),
cdl_tcb_intent = transform_full_intent (machine_state s') p tcb,
cdl_tcb_has_fault = (tcb_has_fault tcb),
cdl_tcb_domain = tcb_domain etcb
\<rparr>)"
apply (simp add: transform_def transform_objects_def)
apply (clarsimp simp: transform_tcb_def)
done
lemma get_ipc_buffer_words_caps_cong:
"\<lbrakk> tcb_ipc_buffer tcb = tcb_ipc_buffer tcb';
is_pg_cap (tcb_ipcframe tcb) = is_pg_cap (tcb_ipcframe tcb');
\<lbrakk> is_pg_cap (tcb_ipcframe tcb); is_pg_cap (tcb_ipcframe tcb') \<rbrakk>
\<Longrightarrow> obj_ref_of (tcb_ipcframe tcb) = obj_ref_of (tcb_ipcframe tcb') \<and>
cap_bits (tcb_ipcframe tcb) = cap_bits (tcb_ipcframe tcb') \<and>
cap_rights (tcb_ipcframe tcb) = cap_rights (tcb_ipcframe tcb')\<rbrakk>
\<Longrightarrow> get_ipc_buffer_words ms tcb ns = get_ipc_buffer_words ms tcb' ns"
apply (clarsimp simp: get_ipc_buffer_words_def is_cap_simps)
by (auto split: cap.splits arch_cap.splits)
lemma transform_full_intent_caps_cong:
"\<lbrakk> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb');
tcb_ipc_buffer tcb = tcb_ipc_buffer tcb';
is_pg_cap (tcb_ipcframe tcb) = is_pg_cap (tcb_ipcframe tcb');
\<lbrakk> is_pg_cap (tcb_ipcframe tcb); is_pg_cap (tcb_ipcframe tcb') \<rbrakk>
\<Longrightarrow> obj_ref_of (tcb_ipcframe tcb) = obj_ref_of (tcb_ipcframe tcb') \<and>
cap_bits (tcb_ipcframe tcb) = cap_bits (tcb_ipcframe tcb') \<and>
cap_rights (tcb_ipcframe tcb) = cap_rights (tcb_ipcframe tcb')
\<rbrakk> \<Longrightarrow>
transform_full_intent ms p tcb = transform_full_intent ms p tcb'"
apply (clarsimp simp: transform_full_intent_def Let_def get_tcb_mrs_def
get_tcb_message_info_def
cong: get_ipc_buffer_words_caps_cong)
done
lemma transform_full_intent_caps_cong_weak:
"\<lbrakk> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb');
tcb_ipc_buffer tcb = tcb_ipc_buffer tcb';
tcb_ipcframe tcb = tcb_ipcframe tcb' \<rbrakk> \<Longrightarrow>
transform_full_intent ms p tcb = transform_full_intent ms p tcb'"
by (rule transform_full_intent_caps_cong) auto
lemma transform_full_intent_same_cap:
"\<lbrakk> transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<rbrakk>
\<Longrightarrow> transform_full_intent ms p' (tcb\<lparr>tcb_ipcframe := cap'\<rparr>) =
transform_full_intent ms p' tcb"
apply (rule transform_full_intent_caps_cong)
apply simp
apply simp
apply (simp add: is_cap_simps)
apply (cases "tcb_ipcframe tcb", simp_all)
by (simp add:transform_cap_def is_cap_simps
split:cap.splits if_split_asm arch_cap.splits)+
lemma set_cap_corres:
assumes "cap = transform_cap cap'" "slot = transform_cslot_ptr slot'"
shows "dcorres dc \<top>
(\<lambda>s. valid_idle s \<and> fst slot' \<noteq> idle_thread s \<and> valid_etcbs s)
(KHeap_D.set_cap slot cap)
(CSpaceAcc_A.set_cap cap' slot')"
proof -
note if_cong[cong]
from assms show ?thesis
apply (case_tac slot')
apply (rename_tac p' sl')
apply (case_tac slot)
apply (rename_tac p sl)
apply (clarsimp simp: KHeap_D.set_cap_def CSpaceAcc_A.set_cap_def)
apply (drule sym)
apply (clarsimp simp:get_object_def gets_the_def bind_assoc gets_def split:if_splits)
apply (clarsimp simp: transform_cslot_ptr_def)
apply (rule dcorres_get)
apply (rename_tac s s')
apply (clarsimp simp: assert_def corres_free_fail)
apply (rename_tac obj')
apply (case_tac obj', simp_all add:corres_free_fail split del: if_split)
\<comment> \<open>cnode or IRQ Node case\<close>
apply (clarsimp simp: corres_free_fail split: if_split)
apply (rename_tac sz cn ocap)
apply (clarsimp simp: corres_underlying_def in_monad set_object_def get_object_def
cte_wp_at_cases caps_of_state_cte_wp_at)
apply (case_tac sz, simp)
apply (frule (1) cdl_objects_irq_node)
apply (clarsimp simp: assert_opt_def has_slots_def)
apply (clarsimp simp: update_slots_def object_slots_def transform_cnode_contents_upd)
apply (clarsimp simp: KHeap_D.set_object_def simpler_modify_def)
apply (clarsimp simp: transform_def transform_current_thread_def)
apply (clarsimp simp: transform_objects_def)
apply (rule ext)
apply clarsimp
apply (simp add: option_map_def restrict_map_def map_add_def split: option.splits)
apply (frule (1) cdl_objects_cnode, simp)
apply (clarsimp simp: assert_opt_def has_slots_def)
apply (clarsimp simp: update_slots_def object_slots_def transform_cnode_contents_upd)
apply (clarsimp simp: KHeap_D.set_object_def simpler_modify_def)
apply (clarsimp simp: transform_def transform_current_thread_def)
apply (clarsimp simp: transform_objects_def)
apply (rule ext)
apply clarsimp
apply (simp add: option_map_def restrict_map_def map_add_def split: option.splits)
\<comment> \<open>tcb case\<close>
apply (drule(1) valid_etcbs_tcb_etcb)
apply (clarsimp simp: cdl_objects_tcb assert_opt_def has_slots_def object_slots_def
update_slots_def
split del: if_split)
apply (case_tac "nat (bl_to_bin sl') = tcb_ipcbuffer_slot")
apply (simp add: tcb_slots)
apply (clarsimp simp: bl_to_bin_tcb_cnode_index|rule conjI)+
apply (rule corres_guard_imp)
apply (rule select_pick_corres)
apply (rule_tac s'=s' in dcorres_set_object_tcb)
apply (clarsimp simp: transform_tcb_def)
apply (rule conjI)
apply (rule ext)
apply (clarsimp simp: transform_tcb_def tcb_slots)
apply (rule refl)
apply assumption
apply simp
apply simp
apply simp
apply clarsimp
apply (rule impI)
apply (rule dcorres_set_object_tcb)
apply (clarsimp simp: transform_tcb_def)
apply (rule conjI)
apply (rule ext)
apply (clarsimp simp: transform_tcb_def tcb_slots)
apply (erule transform_full_intent_same_cap)
apply simp
apply simp
apply ((clarsimp simp: bl_to_bin_tcb_cnode_index corres_free_fail|rule conjI)+)[2] (* sseefried: brittle. Try changing number on end *)
apply (simp add: bl_to_bin_tcb_cnode_index tcb_slot_defs)
apply (rule conjI)
apply (clarsimp simp: bl_to_bin_tcb_cnode_index)
by (rule conjI ext dcorres_set_object_tcb|simp|
clarsimp simp: transform_tcb_def tcb_slot_defs corres_free_fail
cong: transform_full_intent_caps_cong_weak)+
qed
lemma tcb_slot_pending_ipc_neq [simp]:
"tcb_pending_op_slot \<noteq> tcb_ipcbuffer_slot"
by (simp add: tcb_pending_op_slot_def tcb_ipcbuffer_slot_def)
lemma transform_full_intent_update_tcb_state[simp]:
"transform_full_intent m ptr (update_tcb_state st a)
= transform_full_intent m ptr a"
apply (case_tac a)
apply (simp add:transform_full_intent_def Let_def)
apply (simp add:get_tcb_message_info_def
get_tcb_mrs_def get_ipc_buffer_words_def)
done
(*Special set_cap case which is related to thread_state *)
lemma set_pending_cap_corres:
"dcorres dc \<top> (not_idle_thread y and ko_at (TCB obj) y
and K (cap = infer_tcb_pending_op y tcb_st) and valid_etcbs)
(KHeap_D.set_cap (y, tcb_pending_op_slot) cap)
(KHeap_A.set_object y (TCB (update_tcb_state tcb_st obj)))"
apply (simp add: KHeap_D.set_cap_def gets_def gets_the_def bind_assoc not_idle_thread_def)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp: obj_at_def)
apply (drule(1) valid_etcbs_tcb_etcb, clarsimp)
apply (frule opt_object_tcb[rotated, rotated])
apply (fastforce simp: get_tcb_def)
apply (fastforce simp: get_etcb_rev)
apply (clarsimp simp: assert_opt_def has_slots_def transform_tcb_def object_slots_def update_slots_def)
apply (clarsimp simp: corres_underlying_def in_monad set_object_def get_object_def
KHeap_D.set_object_def simpler_modify_def)
apply (simp add: transform_def transform_current_thread_def)
apply (rule ext)
apply (subst transform_objects_update_kheap_same_caps)
apply ((simp add: obj_at_def transform_tcb_def
not_generates_pending_is_null tcb_slots)+)[3]
apply (auto simp: obj_at_def not_generates_pending_is_null transform_tcb_def tcb_slots)
done
lemma transform_scheduler_action_update[simp]: "transform (s\<lparr> scheduler_action := a \<rparr>) = transform s"
by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)
lemma transform_cdt_list_update[simp]: "transform (s\<lparr> cdt_list := a \<rparr>) = transform s"
by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)
lemma transform_ready_queues_update[simp]: "transform (s\<lparr> ready_queues := a \<rparr>) = transform s"
by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)
lemma set_thread_state_ext_dcorres: "dcorres dc P P' (return ()) (set_thread_state_ext y)"
apply (clarsimp simp: set_thread_state_ext_def)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_symb_exec_r)
apply (clarsimp simp: corres_underlying_def when_def set_scheduler_action_def
modify_def bind_def put_def gets_def get_def return_def
split: option.splits)
apply wp+
done
(*Special set_cap case which is related to thread_state *)
lemma set_thread_state_corres:
"dcorres dc \<top> (not_idle_thread y and K (cap = infer_tcb_pending_op y st) and valid_etcbs)
(KHeap_D.set_cap (y, tcb_pending_op_slot) cap)
(KHeap_A.set_thread_state y st)"
apply (simp add:set_thread_state_def)
apply (rule dcorres_absorb_gets_the)
apply (rule dcorres_rhs_noop_below)
apply (rule set_thread_state_ext_dcorres)
apply (rule corres_guard_imp)
apply (rule set_pending_cap_corres)
apply simp
apply (clarsimp dest!:get_tcb_SomeD simp:obj_at_def)
apply (rule hoare_TrueI)+
done
lemma set_cap_null_cap_corres:
"dcorres dc \<top> (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs)
(KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap)
(do set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)"
apply (rule corres_dummy_return_pl)
apply (rule corres_guard_imp)
apply (rule corres_split[where r'="dc"])
apply (rule set_original_dummy_corres)
apply clarsimp
apply (rule set_cap_corres)
apply (clarsimp simp:transform_cap_def)
apply (rule refl)
apply wp+
apply clarsimp
apply (clarsimp simp: cte_wp_at_caps_of_state)
done
lemma mdb_cte_at_cte_wp_at:
"\<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk>
\<Longrightarrow> (cte_wp_at ((\<noteq>) cap.NullCap) slot s)"
apply (clarsimp simp:mdb_cte_at_def)
apply (case_tac slot,case_tac slot')
apply (drule spec)+
apply (auto)
done
lemma mdb_cte_at_cte_wp_at':
"\<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk>
\<Longrightarrow>(cte_wp_at ((\<noteq>) cap.NullCap) slot' s)"
apply (case_tac slot,case_tac slot')
apply (clarsimp simp:mdb_cte_at_def)
done
lemma transform_cdt_slot_inj_on_mdb_cte_at:
"\<lbrakk> mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<rbrakk> \<Longrightarrow>
inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s))"
apply (rule transform_cdt_slot_inj_on_cte_at[where P=P and s=s], simp_all)
apply (safe elim!: ranE)
apply (drule(1) mdb_cte_atD | clarsimp simp: cte_wp_at_caps_of_state)+
done
lemma transform_cdt_none:
"\<lbrakk> cte_at slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s);
(cdt s) slot = None \<rbrakk>
\<Longrightarrow> transform_cdt s (transform_cslot_ptr slot) = None"
apply (case_tac slot)
apply (clarsimp simp: transform_cdt_def map_lift_over_eq_None)
apply (rule ccontr, clarsimp)
apply (subst(asm) transform_cslot_ptr_inj, simp_all)
apply (drule(1) mdb_cte_atD)
apply (clarsimp simp: cte_wp_at_caps_of_state)
done
lemma transform_cdt_some:
"\<lbrakk> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s);
(cdt s) slot = Some slot' \<rbrakk>
\<Longrightarrow> transform_cdt s (transform_cslot_ptr slot)
= Some (transform_cslot_ptr slot')"
apply (case_tac slot)
apply (case_tac slot')
apply (clarsimp simp: transform_cdt_def map_lift_over_eq_Some
transform_cdt_slot_inj_on_mdb_cte_at)
apply auto
done
lemma mdb_cte_transform_cdt_lift:
"\<lbrakk>cte_at slot s; mdb_cte_at (swp (cte_wp_at((\<noteq>) cap.NullCap)) s ) (cdt s) \<rbrakk>
\<Longrightarrow> transform_cdt s (transform_cslot_ptr slot)
= (case ((cdt s) slot ) of
None \<Rightarrow> None
| Some slot' \<Rightarrow> Some (transform_cslot_ptr slot'))"
apply (case_tac "(cdt s) slot")
apply (clarsimp simp:transform_cdt_none transform_cdt_some)+
done
lemma cte_at_to_bl_eq:
"\<lbrakk>bl_to_bin b = uint w; cte_at (a,b) s; cte_at (a,to_bl w) s\<rbrakk>
\<Longrightarrow> to_bl w = b"
apply (subgoal_tac "length b = length (to_bl w)")
apply (simp add:uint_nat[symmetric])
apply (rule to_bl_use_of_bl[THEN iffD2])
apply (clarsimp simp:of_bl_def)
apply (drule iffD1[OF cte_at_cases])+
apply (erule disjE)
apply (clarsimp simp: well_formed_cnode_n_def dom_def)
apply (subgoal_tac "length b = sz")
apply (subgoal_tac "length (to_bl w) = sz")
apply simp
apply (drule_tac x="to_bl w" in eqset_imp_iff)
apply simp
apply (drule_tac x=b in eqset_imp_iff)
apply simp
apply clarsimp
apply (subgoal_tac "(b\<in> dom tcb_cap_cases)")
apply (subgoal_tac "((to_bl w)\<in> dom tcb_cap_cases)")
apply (drule tcb_cap_cases_length)
apply (drule tcb_cap_cases_length)
apply clarsimp
apply (clarsimp simp:dom_def)+
done
lemma transform_cdt_some_rev:
"\<lbrakk> transform_cdt s (transform_cslot_ptr slot_a)
= Some (transform_cslot_ptr slot);
cte_at slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s)(cdt s) \<rbrakk>
\<Longrightarrow>\<exists>slot_b. transform_cslot_ptr slot_b
= transform_cslot_ptr slot_a \<and> (cdt s) slot_b = Some slot"
apply (clarsimp simp: transform_cdt_def map_lift_over_eq_Some)
apply (subst(asm) transform_cslot_ptr_inj, assumption, simp_all)
apply (drule(1) mdb_cte_atD, clarsimp simp: cte_wp_at_caps_of_state)
apply fastforce
done
lemma page_table_not_in_cdt:"\<lbrakk>page_table_at a s;cte_wp_at P (a, ba) s\<rbrakk> \<Longrightarrow> False"
apply (clarsimp simp:obj_at_def a_type_def)
apply (clarsimp split:Structures_A.kernel_object.split_asm if_splits arch_kernel_obj.split_asm)
apply (clarsimp simp:cte_wp_at_cases)
done
lemma page_directory_not_in_cdt:"\<lbrakk>page_directory_at a s;cte_wp_at P (a, ba) s\<rbrakk> \<Longrightarrow> False"
apply (clarsimp simp:obj_at_def a_type_def)
apply (clarsimp split:Structures_A.kernel_object.split_asm if_splits arch_kernel_obj.split_asm)
apply (clarsimp simp:cte_wp_at_cases)
done
lemma asid_pool_not_in_cdt:"\<lbrakk>asid_pool_at a s;cte_wp_at P (a, ba) s\<rbrakk> \<Longrightarrow> False"
apply (clarsimp simp:obj_at_def a_type_def)
apply (clarsimp split:Structures_A.kernel_object.split_asm if_splits arch_kernel_obj.split_asm)
apply (clarsimp simp:cte_wp_at_cases)
done
lemma dummy_remove_cdt_pt_slot:
"dcorres dc \<top> ( (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and page_table_at a)
(remove_parent (a, y)) (return x)"
supply if_cong[cong]
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:remove_parent_def corres_underlying_def return_def simpler_modify_def)
apply (clarsimp simp:remove_parent_def exs_valid_def simpler_modify_def transform_def)
apply (rule ext)
apply (clarsimp simp:transform_cdt_def| rule conjI)+