-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathInitCSpace_SI.thy
1800 lines (1679 loc) · 91.2 KB
/
InitCSpace_SI.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 InitCSpace_SI
imports
"DSpecProofs.CNode_DP"
ObjectInitialised_SI
RootTask_SI
SysInit_SI
Mapped_Separating_Conjunction
begin
(****************************
* Move me
*****************************)
lemma sum_less:
"\<lbrakk>(a::nat) \<le> a'; a' + b \<le> c\<rbrakk> \<Longrightarrow> a + b \<le> c"
by auto
lemma mask_smaller:
"((x::word32) && mask n) \<le> x"
by (metis word_and_le2)
(* Not used by might be useful someday *)
lemma map_of_zip_is_Some2:
"\<lbrakk>length xs = length ys; distinct xs\<rbrakk>
\<Longrightarrow> (y \<in> set ys) = (\<exists>x. map_of (zip xs ys) x = Some y)"
apply (subst ran_map_of_zip [symmetric, where xs=xs and ys=ys], simp+)
apply (rule)
apply (metis map_of_SomeD ranE)
apply (clarsimp simp: ran_def)
done
(* Not used by might be useful someday *)
lemma map_of_zip_is_Some2':
"\<lbrakk>length xs \<le> length ys; distinct xs; map_of (zip xs ys) x = Some y\<rbrakk> \<Longrightarrow> y \<in> set ys"
apply (subst (asm) zip_take_length[symmetric])
apply (drule iffD2 [OF map_of_zip_is_Some2, rotated], fast)
apply (clarsimp simp: min_def)
by (rule in_set_takeD)
(*********************
Moved to capDL somewhere.
*)
lemma object_slot_spec2s:
"object_slots obj slot = object_slots obj' slot
\<Longrightarrow> object_slots (spec2s t obj) slot =
object_slots (spec2s t obj') slot"
apply (case_tac "has_slots obj")
apply (case_tac "has_slots obj'")
apply (clarsimp simp: spec2s_def)+
apply (case_tac obj')
apply (simp_all add:object_slots_def update_slots_def)
done
lemma irqhandler_cap_cap_irq [simp]:
"is_irqhandler_cap cap \<Longrightarrow> IrqHandlerCap (cap_irq cap) = cap"
by (clarsimp simp: cap_type_def cap_irq_def split: cdl_cap.splits)
lemma InitThreadCNode_guard_equal[simp]:
"guard_equal si_cspace_cap seL4_CapInitThreadCNode word_bits"
apply (clarsimp simp:seL4_CapInitThreadCNode_def word_bits_def)
apply (rule guard_equal_si_cspace_cap)
apply (simp add:si_cnode_size_def)
done
lemma default_cap_has_type:
"cap_type cap = Some type
\<Longrightarrow> cap_has_type (default_cap type ids sz dev)"
by (fastforce simp: default_cap_def cap_type_def
split: cdl_cap.splits)
lemma cap_has_type_update_cap_object[simp]:
"cap_has_type (update_cap_object client_object_id spec_cap)
= cap_has_type spec_cap"
apply (case_tac spec_cap,
(fastforce simp: cap_type_def update_cap_object_def)+)
done
lemma ep_related_cap_badge_of_default:
"\<lbrakk>ep_related_cap spec_cap; cap_type spec_cap = Some type\<rbrakk>
\<Longrightarrow> cap_badge (default_cap type {client_object_id} sz dev) = 0"
by (clarsimp simp: ep_related_cap_def cap_type_def
default_cap_def cap_badge_def safe_for_derive_def
split: cdl_cap.splits)
lemma valid_src_cap_cnode_cap_size_le_32:
"valid_src_cap spec_cap (cap_data spec_cap) \<Longrightarrow>
cnode_cap_size spec_cap \<le> 32"
apply (case_tac "is_cnode_cap spec_cap")
apply (clarsimp simp: valid_src_cap_def word_bits_def)
apply (clarsimp simp: cnode_cap_size_def split: cdl_cap.splits)
done
lemma si_spec_irq_null_cap_at_si_spec_irq_cap_at_has_type:
"\<lbrakk>opt_cap (obj_id, slot) spec = Some spec_cap; cap_type spec_cap = Some type; type \<noteq> IRQNodeType\<rbrakk>
\<Longrightarrow> si_spec_irq_null_cap_at irq_caps spec obj_id slot
= si_spec_irq_cap_at irq_caps spec obj_id slot"
by (clarsimp simp: si_spec_irq_cap_at_def si_spec_irq_null_cap_at_def cap_at_def)
lemma cnode_at_not_tcb_at:
"\<lbrakk>cnode_at obj_id spec \<rbrakk>\<Longrightarrow> \<not>tcb_at obj_id spec"
apply (clarsimp simp: object_at_def is_cnode_def is_tcb_def)
apply (case_tac object, simp_all)
done
lemma guard_size_well_formed:
"\<lbrakk>guard_size < guard_bits; (g::word32) < 2 ^ guard_size\<rbrakk> \<Longrightarrow>
g < 2 ^ (size g - 8)"
apply (frule (1) guard_less_guard_bits)
apply (erule less_le_trans)
apply (rule two_power_increasing)
apply (clarsimp simp: word_bits_size word_bits_def guard_bits_def)
apply (clarsimp simp: word_bits_size word_bits_def)
done
lemma well_formed_cap_valid_src_cap:
"well_formed_cap cap \<Longrightarrow> valid_src_cap cap (cap_data cap)"
apply (clarsimp simp: valid_src_cap_def)
apply (clarsimp simp: cap_data_def cnode_cap_size_def)
apply (clarsimp simp: well_formed_cap_def cap_type_def guard_as_rawdata_def split: cdl_cap.splits)
apply (rename_tac guard guard_size size_bits)
apply (subst is_aligned_add_or [where n=8])
apply (rule is_aligned_shift)
apply (rule shiftl_less_t2n)
apply (rule word_of_nat_less)
apply (clarsimp simp: guard_bits_def)
apply clarsimp
apply (clarsimp simp: shiftr_over_or_dist)
apply (subst shiftl_shiftr_id, simp+)
apply (rule word_of_nat_less)
apply (clarsimp simp: guard_bits_def)
apply (subst shiftl_shiftr1, simp)
apply clarsimp
apply (subst less_mask_eq, erule (1) guard_size_well_formed)
apply (subst word_ao_dist)
apply (subst shiftl_mask_is_0, simp)
apply (clarsimp simp: word_bits_size word_bits_def)
apply (rule_tac a'="guard_size" in sum_less)
apply (cut_tac x="of_nat guard_size" and n=5 in mask_smaller)
apply (erule word_unat_less_le)
apply simp
done
lemma well_formed_cap_has_object_has_type [simp]:
"\<lbrakk>well_formed_cap cap; cap_has_object cap\<rbrakk> \<Longrightarrow> cap_has_type cap"
by (clarsimp simp: cap_has_object_def well_formed_cap_def cap_type_def
split: cdl_cap.splits)
(* Needed? *)
lemma si_spec_irq_cap_at_empty_cap_has_object:
"cap_at cap_has_object (obj_id, slot) spec
\<Longrightarrow> si_spec_irq_cap_at irq_caps spec obj_id slot = \<box>"
by (clarsimp simp: si_spec_irq_cap_at_def cap_at_def)
(* Needed? *)
lemma si_obj_cap_at_empty_cap_has_object:
"irqhandler_cap_at (obj_id, slot) spec
\<Longrightarrow> si_obj_cap_at t orig_caps spec False obj_id slot = \<box>"
by (clarsimp simp: si_obj_cap_at_def cap_at_def)
(* MOVEME *)
lemma well_formed_cap_no_object_irqhandler_cap:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap;
\<not> cap_at cap_has_object (obj_id, slot) spec\<rbrakk>
\<Longrightarrow> cap_at is_irqhandler_cap (obj_id, slot) spec"
apply (clarsimp simp: cap_at_def)
apply (frule opt_cap_cdl_objects, clarsimp)
apply (frule (1) object_slots_opt_capI)
apply (drule (3) well_formed_well_formed_cap)
apply (clarsimp simp: well_formed_cap_def cap_has_object_def
split: cdl_cap.splits)
done
(**********************************************************************
* Helper lemmas about CNodes, and when they are halfway initialised. *
**********************************************************************)
lemma valid_src_cap_if_cnode:
"\<lbrakk>cap_type spec_cap = Some type;
is_cnode_cap spec_cap \<longrightarrow> sz = cnode_cap_size spec_cap;
valid_src_cap spec_cap data\<rbrakk>
\<Longrightarrow> valid_src_cap (default_cap type {client_object_id} sz dev) data"
apply (clarsimp simp: valid_src_cap_def)
apply (clarsimp simp: cnode_cap_size_def cap_type_def default_cap_def)
done
lemma default_cap_data_if_cnode:
"\<lbrakk>cap_type spec_cap = Some type;
is_cnode_cap spec_cap \<longrightarrow> sz = cnode_cap_size spec_cap\<rbrakk>
\<Longrightarrow> (default_cap type m sz dev)
= (default_cap type m (cnode_cap_size spec_cap) dev)"
by (case_tac spec_cap,
(clarsimp simp: default_cap_def cap_type_def is_cnode_cap_simps)+)
(************************************************************
* A CNode slot that is half done is either done, or empty. *
************************************************************)
lemma object_slots_cnode_half:
"\<lbrakk>\<not>original_cap_at (obj_id, slot) spec\<rbrakk>
\<Longrightarrow> object_slots (cnode_half spec obj_id obj) slot =
object_slots obj slot"
apply (case_tac "has_slots obj")
apply (clarsimp simp: cnode_half_def restrict_map_def)
apply (clarsimp simp: cnode_half_def)
done
lemma cnode_slot_half_initialised_not_original_slot:
"\<not>original_cap_at (obj_id, slot) spec
\<Longrightarrow> cnode_slot_half_initialised spec t obj_id slot
= object_slot_initialised spec t obj_id slot"
apply (clarsimp simp: cnode_slot_half_initialised_def object_slot_initialised_def)
apply (clarsimp simp: object_initialised_general_def)
apply (rule ext, rule iffI)
apply (clarsimp simp: sep_map_s_def sep_map_general_def)
apply (rule ext)
apply (clarsimp simp: object_to_sep_state_def object_project_def
object_slots_object_clean
split: option.splits)
apply (cut_tac obj = "cnode_half spec obj_id spec_object" and
obj' = spec_object and slot=slot and t=t in object_slot_spec2s)
apply (erule object_slots_cnode_half)
apply clarsimp
apply (clarsimp simp: sep_map_s_def sep_map_general_def)
apply (rule ext)
apply (clarsimp simp: object_to_sep_state_def object_project_def
object_slots_object_clean
split: option.splits)
apply (cut_tac obj = "cnode_half spec obj_id spec_object" and
obj' = spec_object and slot=slot and t=t in object_slot_spec2s)
apply (erule object_slots_cnode_half)
apply clarsimp
done
lemma slots_empty_cnode1:
"slot < 2 ^ sz
\<Longrightarrow> object_slots (CNode (empty_cnode sz)) slot = Some NullCap"
by (fastforce simp: object_slots_def empty_cnode_def empty_cap_map_def
restrict_map_def cdl_cnode.splits)
lemma slots_empty_cnode2:
"\<not> slot < 2 ^ sz
\<Longrightarrow> object_slots (CNode (empty_cnode sz)) slot = None"
by (fastforce simp: object_slots_def empty_cnode_def empty_cap_map_def
restrict_map_def cdl_cnode.splits)
lemma slots_spec2s_cnode_half1:
"\<lbrakk>slot < 2 ^ sz; original_cap_at (obj_id, slot) spec; (cdl_cnode_caps cnode slot) \<noteq> None\<rbrakk>
\<Longrightarrow> object_slots (spec2s t (cnode_half spec obj_id (CNode cnode))) slot
= Some NullCap"
by (fastforce simp: object_slots_def cnode_half_def spec2s_def update_slots_def)
lemma slots_spec2s_cnode_half2:
"\<lbrakk>\<not> slot < 2 ^ sz; original_cap_at (obj_id, slot) spec; (cdl_cnode_caps cnode slot) = None\<rbrakk>
\<Longrightarrow> object_slots (spec2s t (cnode_half spec obj_id (CNode cnode))) slot
= None"
by (fastforce simp: object_slots_def cnode_half_def spec2s_def update_slots_def
restrict_map_def)
lemma object_slots_spec2s_cnode_half_object_default_state:
"\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec;
cdl_objects spec obj_id = Some spec_object; is_cnode spec_object\<rbrakk>
\<Longrightarrow> object_slots (spec2s t (cnode_half spec obj_id spec_object)) slot =
object_slots (object_default_state spec_object) slot"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply (clarsimp split: option.splits)
apply (clarsimp simp: object_default_state_def2 is_cnode_def
split: cdl_object.splits)
apply (rename_tac cnode)
apply (case_tac "slot < 2 ^ cdl_cnode_size_bits cnode")
apply (frule slots_empty_cnode1)
apply (frule_tac cnode=cnode and t=t in slots_spec2s_cnode_half1, assumption)
apply (clarsimp simp: object_slots_def dom_def empty_cnode_def empty_cap_map_def)
apply fastforce
apply (clarsimp simp: update_slots_def empty_cnode_def spec2s_def cnode_half_def)
apply (frule slots_empty_cnode2)
apply (frule_tac cnode=cnode and t=t in slots_spec2s_cnode_half2, assumption)
apply (fastforce simp: object_slots_def dom_def empty_cnode_def empty_cap_map_def)
apply clarsimp
done
lemma cnode_slot_half_initialised_original_slot:
"\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec; cnode_at obj_id spec\<rbrakk>
\<Longrightarrow> cnode_slot_half_initialised spec t obj_id slot
= object_slot_empty spec t obj_id slot"
apply (clarsimp simp: object_at_def)
apply (frule (1) well_formed_object_slots)
apply (clarsimp simp: cnode_slot_half_initialised_def object_slot_empty_def)
apply (clarsimp simp: object_initialised_general_def)
apply (rule ext, rule iffI)
apply (clarsimp simp: sep_map_s_def sep_map_general_def)
apply (rule ext, clarsimp simp:object_to_sep_state_def
object_project_def object_slots_object_clean)
apply (subst object_slots_spec2s_cnode_half_object_default_state)
apply simp+
apply (clarsimp simp: object_at_def)+
apply (clarsimp simp: sep_map_s_def sep_map_general_def)
apply (rule ext)
apply (clarsimp simp:object_to_sep_state_def object_project_def object_slots_object_clean)
apply (subst object_slots_spec2s_cnode_half_object_default_state, simp+)
apply (clarsimp split: option.splits)
done
(**************************
**************************
* init_cspace proof *
**************************
**************************)
lemma default_cap_cnode_dev:
"default_cap CNodeType a b dev = CNodeCap (pick a) 0 0 b"
by (simp add:default_cap_def)
lemma mint_pre:
"\<lbrakk>well_formed spec; cnode_at obj_id spec;
cdl_objects spec obj_id = Some spec_obj;
opt_cap (obj_id, slot) spec = Some spec_cap;
spec_cap \<noteq> NullCap;
cap_has_object spec_cap;
cap_type spec_cap = Some type;
is_device_cap spec_cap = dev;
data = cap_badge spec_cap;
Some dest_root = dup_caps obj_id;
dest_index = of_nat slot;
(dest_depth::word32) = of_nat (object_size_bits spec_obj);
src_root = seL4_CapInitThreadCNode;
Some src_index = orig_caps (cap_object spec_cap);
src_index < 2 ^ si_cnode_size;
src_depth = (32::word32);
rights = cap_rights spec_cap;
\<guillemotleft>object_slot_empty spec t obj_id slot \<and>*
si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s;
cdl_objects spec (cap_object spec_cap) = Some spec_cap_object;
dest_root_slot = offset dest_root si_cnode_size;
cnode_cap_slot = offset src_root si_cnode_size;
src_slot = offset src_index si_cnode_size;
t obj_id = Some dest_id;
default_cap CNodeType {dest_id} dest_size False = dest_root_cap;
object_size_bits spec_obj = dest_size;
dest_slot = offset dest_index dest_size;
t (cap_object spec_cap) = Some client_object_id;
default_cap type {client_object_id} (object_size_bits spec_cap_object) = src_cap\<rbrakk>
\<Longrightarrow>
\<guillemotleft>si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
\<comment> \<open>Root CNode.\<close>
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
\<comment> \<open>Client cnode.\<close>
dest_id \<mapsto>f CNode (empty_cnode dest_size) \<and>*
\<comment> \<open>Cap to the root CNode.\<close>
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
\<comment> \<open>Cap to the client CNode.\<close>
(si_cnode_id, dest_root_slot) \<mapsto>c dest_root_cap \<and>*
\<comment> \<open>Cap that the root task has to its own CNode.\<close>
(si_cnode_id, cnode_cap_slot) \<mapsto>c si_cnode_cap \<and>*
\<comment> \<open>Cap to be copied, in the root CNode.\<close>
(si_cnode_id, src_slot) \<mapsto>c src_cap dev \<and>*
\<comment> \<open>Where to copy the cap (in the client CNode).\<close>
(dest_id, dest_slot) \<mapsto>c NullCap \<and>*
\<comment> \<open>IRQ control cap\<close>
(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>*
\<comment> \<open>ASID caps.\<close>
si_asid \<and>*
R\<guillemotright> s \<and>
\<comment> \<open>Cap slots match their cptrs.\<close>
one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
one_lvl_lookup si_cspace_cap (unat src_depth) si_cnode_size \<and>
one_lvl_lookup dest_root_cap (unat dest_depth) dest_size \<and>
unat src_depth \<le> word_bits \<and>
0 < unat src_depth \<and>
unat dest_depth \<le> word_bits \<and>
0 < unat dest_depth \<and>
is_tcb root_tcb \<and>
is_cnode_cap dest_root_cap \<and>
is_cnode_cap si_cspace_cap \<and>
guard_equal si_cspace_cap src_index (unat src_depth) \<and>
guard_equal dest_root_cap dest_index (unat dest_depth) \<and>
Some dest_root = dup_caps obj_id \<and>
Some src_index = orig_caps (cap_object spec_cap)"
apply clarsimp
apply (frule (3) well_formed_types_match)
apply (frule (3) well_formed_slot_object_size_bits)
apply (frule (2) well_formed_cnode_object_size_bits)
apply (clarsimp simp: object_slot_empty_def object_fields_empty_def object_initialised_general_def)
apply (clarsimp simp: si_objects_def)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (clarsimp simp: si_cap_at_def sep_conj_assoc sep_conj_exists)
apply (clarsimp simp: object_at_def)
apply (clarsimp simp: object_type_is_object)
apply (rule conjI)
apply (sep_drule sep_map_c_sep_map_s)
apply (erule object_slots_object_default_state_NullCap [where obj_id=obj_id])
apply (fastforce simp: object_at_def object_type_is_object)
apply assumption
apply assumption
apply (subst offset_slot, assumption, simp)
apply (subst offset_slot', assumption)
apply (subst offset_slot', assumption)
apply (subst empty_cnode_object_size_bits, simp add: object_type_is_object)
apply (frule (1) well_formed_object_size_bits)
apply (cut_tac obj_id=dest_id and obj'=spec_obj in
sep_map_f_object_size_bits_cnode, (simp add: object_type_is_object)+)
apply (simp add: default_cap_cnode_dev)
apply (sep_solve add: sep_any_imp )
apply (clarsimp simp: one_lvl_lookup_def)
apply (drule guard_equal_si_cspace_cap)
apply (clarsimp simp: default_cap_def object_type_is_object)
apply (cut_tac x="object_size_bits spec_obj" in unat_of_nat32)
apply (insert n_less_equal_power_2 [where n=word_bits])
apply (frule (1) well_formed_object_size_bits_word_bits)
apply (metis lt_word_bits_lt_pow)
apply (frule (1) well_formed_object_size_bits_word_bits)
apply (drule guard_equal_si_cspace_cap)+
apply clarsimp
apply (clarsimp simp: word_bits_def guard_equal_def Let_unfold)
apply (drule (1) well_formed_object_size_bits_word_bits)
apply (simp add: word_bits_def)
done
lemma move_pre_irq_handler:
"\<lbrakk>well_formed spec; cnode_at obj_id spec;
cdl_objects spec obj_id = Some spec_obj;
opt_cap (obj_id, slot) spec = Some spec_cap;
is_irqhandler_cap spec_cap;
Some dest_root = dup_caps obj_id;
dest_index = of_nat slot;
(dest_depth::word32) = of_nat (object_size_bits spec_obj);
src_root = seL4_CapInitThreadCNode;
Some src_index = irq_caps (cap_irq spec_cap);
src_index < 2 ^ si_cnode_size;
src_depth = (32::word32);
rights = cap_rights spec_cap;
\<guillemotleft>object_slot_empty spec t obj_id slot \<and>*
si_irq_cap_at irq_caps spec (cap_irq spec_cap) \<and>*
si_cap_at t dup_caps spec False obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s;
dest_root_slot = offset dest_root si_cnode_size;
cnode_cap_slot = offset src_root si_cnode_size;
src_slot = offset src_index si_cnode_size;
t obj_id = Some dest_id;
default_cap CNodeType {dest_id} dest_size False = dest_root_cap;
object_size_bits spec_obj = dest_size;
dest_slot = offset dest_index dest_size\<rbrakk>
\<Longrightarrow>
\<guillemotleft>si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
\<comment> \<open>Root CNode.\<close>
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
\<comment> \<open>Client cnode.\<close>
dest_id \<mapsto>f CNode (empty_cnode dest_size) \<and>*
\<comment> \<open>Cap to the root CNode.\<close>
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
\<comment> \<open>Cap to the client CNode.\<close>
(si_cnode_id, dest_root_slot) \<mapsto>c dest_root_cap \<and>*
\<comment> \<open>Cap that the root task has to its own CNode.\<close>
(si_cnode_id, cnode_cap_slot) \<mapsto>c si_cnode_cap \<and>*
\<comment> \<open>Cap to be copied, in the root CNode.\<close>
(si_cnode_id, src_slot) \<mapsto>c spec_cap \<and>*
\<comment> \<open>Where to copy the cap (in the client CNode).\<close>
(dest_id, dest_slot) \<mapsto>c NullCap \<and>*
\<comment> \<open>IRQ control cap\<close>
(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>*
\<comment> \<open>ASID caps.\<close>
si_asid \<and>*
R\<guillemotright> s \<and>
\<comment> \<open>Cap slots match their cptrs.\<close>
one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
one_lvl_lookup si_cspace_cap 32 si_cnode_size \<and>
one_lvl_lookup si_cspace_cap (unat src_depth) si_cnode_size \<and>
one_lvl_lookup dest_root_cap (unat dest_depth) dest_size \<and>
unat src_depth \<le> word_bits \<and>
0 < unat src_depth \<and>
unat dest_depth \<le> word_bits \<and>
0 < unat dest_depth \<and>
is_tcb root_tcb \<and>
is_cnode_cap dest_root_cap \<and>
is_cnode_cap si_cspace_cap \<and>
guard_equal si_cspace_cap src_index (unat src_depth) \<and>
guard_equal dest_root_cap dest_index (unat dest_depth) \<and>
Some dest_root = dup_caps obj_id \<and>
Some src_index = irq_caps (cap_irq spec_cap)"
apply clarsimp
apply (frule (3) well_formed_slot_object_size_bits)
apply (frule (2) well_formed_cnode_object_size_bits)
apply (clarsimp simp: object_slot_empty_def object_fields_empty_def object_initialised_general_def)
apply (clarsimp simp: si_objects_def)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (clarsimp simp: si_cap_at_def si_irq_cap_at_def sep_conj_assoc sep_conj_exists)
apply (clarsimp simp: object_at_def)
apply (clarsimp simp: object_type_is_object)
apply (rule conjI)
apply (sep_drule sep_map_c_sep_map_s)
apply (erule object_slots_object_default_state_NullCap [where obj_id=obj_id])
apply (fastforce simp: object_at_def object_type_is_object)
apply assumption
apply assumption
apply (simp add:default_cap_cnode_dev)
apply (subst offset_slot, assumption, simp)
apply (subst offset_slot', assumption)
apply (subst offset_slot', assumption)
apply (subst empty_cnode_object_size_bits, simp add: object_type_is_object)
apply (frule (1) well_formed_object_size_bits)
apply (cut_tac obj_id=dest_id and obj'=spec_obj in
sep_map_f_object_size_bits_cnode, (simp add: object_type_is_object)+)
apply sep_solve
apply (clarsimp simp: one_lvl_lookup_def)
apply (drule guard_equal_si_cspace_cap)
apply (clarsimp simp: default_cap_def object_type_is_object)
apply (cut_tac x="object_size_bits spec_obj" in unat_of_nat32)
apply (insert n_less_equal_power_2 [where n=word_bits])
apply (frule (1) well_formed_object_size_bits_word_bits)
apply (metis lt_word_bits_lt_pow)
apply (frule (1) well_formed_object_size_bits_word_bits)
apply (drule guard_equal_si_cspace_cap)+
apply clarsimp
apply (clarsimp simp: word_bits_def guard_equal_def Let_unfold)
apply (drule (1) well_formed_object_size_bits_word_bits)
apply (simp add: word_bits_def)
done
lemma mint_post:
"\<lbrakk>well_formed spec;
t obj_id = Some dest_id;
cdl_objects spec obj_id = Some spec_obj;
opt_cap (obj_id, slot) spec = Some spec_cap;
cap_has_object spec_cap;
cap_type spec_cap = Some type;
is_device_cap spec_cap = dev;
dup_caps obj_id = Some dest_root;
orig_caps (cap_object spec_cap) = Some src_index;
cdl_objects spec (cap_object spec_cap) = Some spec_cap_object;
t (cap_object spec_cap) = Some client_object_id;
data = cap_data spec_cap;
cnode_at obj_id spec;
src_index < 2 ^ si_cnode_size;
dest_root < 2 ^ si_cnode_size;
\<comment> \<open>Remove me.\<close>
\<not> is_untyped_cap spec_cap;
spec_cap \<noteq> NullCap;
\<guillemotleft>si_tcb_id \<mapsto>f root_tcb \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
dest_id \<mapsto>f CNode (empty_cnode (object_size_bits spec_obj)) \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_cnode_id, offset dest_root si_cnode_size) \<mapsto>c default_cap CNodeType {dest_id} (object_size_bits spec_obj) False \<and>*
(si_cnode_id, offset seL4_CapInitThreadCNode si_cnode_size) \<mapsto>c si_cnode_cap \<and>*
(si_cnode_id, offset src_index si_cnode_size) \<mapsto>c default_cap type {client_object_id} (object_size_bits spec_cap_object) dev \<and>*
(dest_id, offset (of_nat slot) (object_size_bits spec_obj)) \<mapsto>c
derived_cap (update_cap_data_det data
(update_cap_rights (cap_rights (default_cap type {client_object_id} (object_size_bits spec_cap_object) dev) \<inter> cap_rights spec_cap)
(default_cap type {client_object_id} (cnode_cap_size spec_cap) (is_device_cap spec_cap)))) \<and>*
(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>*
si_asid \<and>* R\<guillemotright> s\<rbrakk>
\<Longrightarrow>
\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s"
apply (frule (3) well_formed_types_match)
apply (frule (3) well_formed_slot_object_size_bits)
apply (frule (1) well_formed_object_slots, simp)
apply (clarsimp simp: object_slot_initialised_def object_fields_empty_def object_initialised_general_def)
apply (clarsimp simp: si_objects_def)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (clarsimp simp: si_cap_at_def sep_conj_assoc sep_conj_exists)
apply (clarsimp simp: object_at_def object_type_is_object)
apply (frule_tac obj_id=dest_id in empty_cnode_object_size_bits, clarsimp)
apply (cut_tac slot=slot in offset_slot, assumption, simp, simp)
apply (subst sep_map_s_sep_map_c_eq [where cap="update_cap_object client_object_id spec_cap"])
apply (rule object_slots_spec2s, (clarsimp simp: opt_cap_def slots_of_def)+)
apply (frule (2) well_formed_well_formed_cap, clarsimp simp: cap_has_object_def)
apply (frule (2) well_formed_vm_cap_has_asid)
apply (frule (1) well_formed_is_fake_vm_cap,
(assumption|simp add: object_type_is_object)+)
apply (clarsimp simp: cap_rights_inter_default_cap_rights)
apply (subst (asm) update_cap_rights_and_data,(assumption|clarsimp)+)
apply (subst (asm) offset_slot', assumption)+
apply (clarsimp simp: default_cap_cnode_dev)
apply sep_solve
done
lemma mutate_post:
"\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec;
t obj_id = Some dest_id;
cdl_objects spec obj_id = Some spec_obj;
opt_cap (obj_id, slot) spec = Some spec_cap;
cap_has_object spec_cap;
cap_type spec_cap = Some type;
is_device_cap spec_cap = dev;
dup_caps obj_id = Some dest_root;
orig_caps (cap_object spec_cap) = Some src_index;
cdl_objects spec (cap_object spec_cap) = Some spec_cap_object;
t (cap_object spec_cap) = Some client_object_id;
data = cap_data spec_cap;
cnode_at obj_id spec;
src_index < 2 ^ si_cnode_size;
dest_root < 2 ^ si_cnode_size;
\<not> is_untyped_cap spec_cap;
spec_cap \<noteq> NullCap;
\<guillemotleft>si_tcb_id \<mapsto>f root_tcb \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
dest_id \<mapsto>f CNode (empty_cnode (object_size_bits spec_obj)) \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_cnode_id, offset dest_root si_cnode_size) \<mapsto>c default_cap CNodeType {dest_id} (object_size_bits spec_obj) False \<and>*
(si_cnode_id, offset seL4_CapInitThreadCNode si_cnode_size) \<mapsto>c si_cnode_cap \<and>*
(si_cnode_id, offset src_index si_cnode_size) \<mapsto>c NullCap \<and>*
(dest_id, offset (of_nat slot) (object_size_bits spec_obj)) \<mapsto>c
update_cap_data_det data (default_cap type {client_object_id} (cnode_cap_size spec_cap) dev) \<and>*
(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>*
si_asid \<and>* R\<guillemotright> s\<rbrakk>
\<Longrightarrow>
\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s"
apply (frule (3) well_formed_types_match)
apply (frule (3) well_formed_slot_object_size_bits)
apply (frule (1) well_formed_object_slots, simp)
apply (clarsimp simp: object_slot_initialised_def object_fields_empty_def object_initialised_general_def)
apply (clarsimp simp: si_objects_def)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (clarsimp simp: si_null_cap_at_def si_cap_at_def sep_conj_assoc sep_conj_exists)
apply (clarsimp simp: object_at_def object_type_is_object)
apply (frule_tac obj_id=dest_id in empty_cnode_object_size_bits, clarsimp)
apply (cut_tac slot=slot in offset_slot, assumption, simp, simp)
apply (subst sep_map_s_sep_map_c_eq [where cap="update_cap_object client_object_id spec_cap"])
apply (rule object_slots_spec2s, (clarsimp simp: opt_cap_def slots_of_def)+)
apply (frule (2) well_formed_well_formed_cap, clarsimp simp: cap_has_object_def)
apply (frule (2) well_formed_vm_cap_has_asid)
apply (frule (1) well_formed_is_fake_vm_cap,
(assumption|simp add: object_type_is_object)+)
apply (subst update_cap_data [symmetric], simp+)
apply (clarsimp simp: cap_has_object_not_irqhandler_cap)
apply (erule well_formed_orig_caps, (simp add: slots_of_def)+)
apply (subst (asm) offset_slot', assumption)+
apply (clarsimp simp: default_cap_cnode_dev)
apply sep_solve
done
lemma move_post:
"\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec;
t obj_id = Some dest_id;
cdl_objects spec obj_id = Some spec_obj;
opt_cap (obj_id, slot) spec = Some spec_cap;
dup_caps obj_id = Some dest_root;
orig_caps (cap_object spec_cap) = Some src_index;
cdl_objects spec (cap_object spec_cap) = Some spec_cap_object;
t (cap_object spec_cap) = Some client_object_id;
cap_has_object spec_cap;
data = cap_data spec_cap;
spec_cap \<noteq> NullCap;
cnode_at obj_id spec;
src_index < 2 ^ si_cnode_size;
dest_root < 2 ^ si_cnode_size;
\<not> is_untyped_cap spec_cap;
\<guillemotleft>si_tcb_id \<mapsto>f root_tcb \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
dest_id \<mapsto>f CNode (empty_cnode (object_size_bits spec_obj)) \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_cnode_id, offset dest_root si_cnode_size) \<mapsto>c default_cap CNodeType {dest_id} (object_size_bits spec_obj) False \<and>*
(si_cnode_id, offset seL4_CapInitThreadCNode si_cnode_size) \<mapsto>c si_cnode_cap \<and>*
(si_cnode_id, offset src_index si_cnode_size) \<mapsto>c NullCap \<and>*
(dest_id, offset (of_nat slot) (object_size_bits spec_obj)) \<mapsto>c
update_cap_object client_object_id spec_cap \<and>*
(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>*
si_asid \<and>* R\<guillemotright> s\<rbrakk>
\<Longrightarrow>
\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s"
apply (frule (3) well_formed_types_match)
apply (frule (3) well_formed_slot_object_size_bits)
apply (frule (1) well_formed_object_slots, simp)
apply (clarsimp simp: object_slot_initialised_def object_fields_empty_def object_initialised_general_def)
apply (clarsimp simp: si_objects_def)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (clarsimp simp: si_null_cap_at_def si_cap_at_def sep_conj_assoc sep_conj_exists)
apply (clarsimp simp: object_at_def object_type_is_object)
apply (frule_tac obj_id=dest_id in empty_cnode_object_size_bits, clarsimp)
apply (cut_tac slot=slot in offset_slot, assumption, simp, simp)
apply (subst sep_map_s_sep_map_c_eq [where cap="update_cap_object client_object_id spec_cap"])
apply (rule object_slots_spec2s, (clarsimp simp: opt_cap_def slots_of_def)+)
apply (subst (asm) offset_slot', assumption)+
apply (clarsimp simp: default_cap_cnode_dev)
apply sep_solve
done
lemma move_post_irq_handler:
"\<lbrakk>well_formed spec;
t obj_id = Some dest_id;
cdl_objects spec obj_id = Some spec_obj;
opt_cap (obj_id, slot) spec = Some spec_cap;
dup_caps obj_id = Some dest_root;
irq_caps (cap_irq spec_cap) = Some src_index;
is_irqhandler_cap spec_cap;
cnode_at obj_id spec;
src_index < 2 ^ si_cnode_size;
dest_root < 2 ^ si_cnode_size;
\<guillemotleft>si_tcb_id \<mapsto>f root_tcb \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
dest_id \<mapsto>f CNode (empty_cnode (object_size_bits spec_obj)) \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_cnode_id, offset dest_root si_cnode_size) \<mapsto>c default_cap CNodeType {dest_id} (object_size_bits spec_obj) False \<and>*
(si_cnode_id, offset seL4_CapInitThreadCNode si_cnode_size) \<mapsto>c si_cnode_cap \<and>*
(si_cnode_id, offset src_index si_cnode_size) \<mapsto>c NullCap \<and>*
(dest_id, offset (of_nat slot) (object_size_bits spec_obj)) \<mapsto>c spec_cap \<and>*
(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>*
si_asid \<and>* R\<guillemotright> s\<rbrakk>
\<Longrightarrow>
\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_null_irq_cap_at irq_caps spec (cap_irq spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s"
apply (frule (3) well_formed_slot_object_size_bits)
apply (frule (1) well_formed_object_slots, simp)
apply (clarsimp simp: object_slot_initialised_def object_fields_empty_def object_initialised_general_def)
apply (clarsimp simp: si_objects_def)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (clarsimp simp: si_null_cap_at_def si_cap_at_def si_null_irq_cap_at_def
sep_conj_assoc sep_conj_exists)
apply (clarsimp simp: object_at_def object_type_is_object)
apply (frule_tac obj_id=dest_id in empty_cnode_object_size_bits, clarsimp)
apply (cut_tac slot=slot in offset_slot, assumption, simp, simp)
apply (subst sep_map_s_sep_map_c_eq [where cap=spec_cap],
(clarsimp simp: opt_cap_def slots_of_def)+)
apply (subst (asm) offset_slot', assumption)+
apply (clarsimp simp: default_cap_cnode_dev)
apply sep_solve
done
lemma seL4_CNode_Mutate_object_slot_initialised_sep_helper:
"\<lbrakk>well_formed spec;
cdl_objects spec obj_id = Some spec_obj;
cnode_at obj_id spec;
opt_cap (obj_id, slot) spec = Some spec_cap;
spec_cap \<noteq> NullCap;
original_cap_at (obj_id, slot) spec;
valid_src_cap spec_cap data;
cap_has_object spec_cap;
cap_type spec_cap = Some type;
is_device_cap spec_cap = dev;
\<not> ep_related_cap spec_cap;
\<not> is_untyped_cap spec_cap;
data = cap_data spec_cap;
cdl_objects spec (cap_object spec_cap) = Some spec_cap_obj;
is_cnode_cap spec_cap \<longrightarrow> object_size_bits spec_cap_obj = cnode_cap_size spec_cap;
t obj_id = Some dest_id;
t (cap_object spec_cap) = Some client_object_id;
src_index < 2 ^ si_cnode_size;
dest_root < 2 ^ si_cnode_size;
Some dest_root = dup_caps obj_id;
Some src_index = orig_caps (cap_object spec_cap)\<rbrakk> \<Longrightarrow>
\<lbrace>\<guillemotleft>object_slot_empty spec t obj_id slot \<and>*
si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> \<rbrace>
seL4_CNode_Mutate dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
seL4_CapInitThreadCNode src_index 32 data
\<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_chain)
apply (rule_tac cnode_cap = si_cspace_cap
and cnode_cap' = si_cnode_cap
and dest_root_cap = "default_cap CNodeType {dest_id} (object_size_bits spec_obj) False"
and root_size=si_cnode_size
and src_root=seL4_CapInitThreadCNode
and src_depth=32
and tcb=root_tcb
and src_cap = "default_cap type {client_object_id} (object_size_bits spec_cap_obj) dev"
in seL4_CNode_Mutate_sep[where
R = "(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>* si_asid \<and>* R"])
apply (assumption|simp add: ep_related_cap_default_cap
default_cap_has_type valid_src_cap_if_cnode
get_index_def)+
apply (frule_tac s=s and dup_caps=dup_caps and
t=t and orig_caps=orig_caps
in mint_pre,(assumption|rule refl|simp)+)
apply (elim conjE)
apply clarsimp
apply (intro conjI,
simp_all add: has_type_default_not_non ep_related_cap_default_cap)
apply (thin_tac "\<guillemotleft>P \<and>* Q \<guillemotright>s" for P Q)
apply sep_solve
apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
dest!: guard_equal_si_cspace_cap |
rule is_cnode_cap_si_cnode_cap)+)[2]
(* it works because si_cnode_cap = si_cspace_cap *)
apply (drule_tac s=s and dest_root=dest_root and src_index=src_index and R=R
in mutate_post, (assumption|simp|fastforce)+)[1]
apply (subst(asm) default_cap_data_if_cnode, fastforce+)
done
lemma seL4_CNode_Move_object_slot_initialised_cap_has_object_sep_helper:
"\<lbrakk>well_formed spec;
cdl_objects spec obj_id = Some spec_obj;
cnode_at obj_id spec;
opt_cap (obj_id, slot) spec = Some spec_cap;
spec_cap \<noteq> NullCap;
original_cap_at (obj_id, slot) spec;
is_default_cap spec_cap;
valid_src_cap spec_cap data;
cap_has_object spec_cap;
cap_type spec_cap = Some type;
is_device_cap spec_cap = dev;
\<not> is_untyped_cap spec_cap;
\<not> is_asidpool_cap spec_cap;
data = cap_data spec_cap;
cdl_objects spec (cap_object spec_cap) = Some spec_cap_obj;
is_cnode_cap spec_cap \<longrightarrow> object_size_bits spec_cap_obj = cnode_cap_size spec_cap;
t obj_id = Some dest_id;
t (cap_object spec_cap) = Some client_object_id;
src_index < 2 ^ si_cnode_size;
dest_root < 2 ^ si_cnode_size;
Some dest_root = dup_caps obj_id;
Some src_index = orig_caps (cap_object spec_cap)\<rbrakk> \<Longrightarrow>
\<lbrace>\<guillemotleft>object_slot_empty spec t obj_id slot \<and>*
si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> \<rbrace>
seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
seL4_CapInitThreadCNode src_index 32
\<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_chain)
apply (rule_tac cnode_cap = si_cspace_cap
and cnode_cap' = si_cnode_cap
and dest_root_cap = "default_cap CNodeType {dest_id} (object_size_bits spec_obj) False"
and root_size=si_cnode_size
and src_root=seL4_CapInitThreadCNode
and src_depth=32
and tcb=root_tcb
and src_cap = "default_cap type {client_object_id} (object_size_bits spec_cap_obj) dev"
in seL4_CNode_Move_sep[where
R = "(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>* si_asid \<and>* R"],
(assumption|simp add: ep_related_cap_default_cap
default_cap_has_type
get_index_def)+)
apply (frule_tac s=s and t=t and dup_caps=dup_caps and orig_caps=orig_caps
in mint_pre,(assumption|rule refl|simp)+)
apply (elim conjE)
apply clarsimp
apply (intro conjI,
simp_all add:has_type_default_not_non ep_related_cap_default_cap)
apply (thin_tac "\<guillemotleft>P \<and>* Q \<guillemotright>s" for P Q)
apply sep_solve
apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
dest!: guard_equal_si_cspace_cap |
rule is_cnode_cap_si_cnode_cap)+)[2]
(* it works because si_cnode_cap = si_cspace_cap *)
apply (drule_tac s=s and dest_root=dest_root and src_index=src_index and R=R
in move_post, (assumption|simp)+)
apply sep_cancel+
apply (drule cap_has_object_not_irqhandler_cap)
apply (subst(asm) default_cap_data_if_cnode,simp+)
apply clarsimp
apply (subst(asm) default_cap_update_cap_object,
(simp add: valid_src_cap_cnode_cap_size_le_32)+)
done
lemma seL4_CNode_Move_object_slot_initialised_irqhandler_cap_sep_helper:
"\<lbrakk>well_formed spec;
cdl_objects spec obj_id = Some spec_obj;
cnode_at obj_id spec;
opt_cap (obj_id, slot) spec = Some spec_cap;
is_irqhandler_cap spec_cap;
t obj_id = Some dest_id;
src_index < 2 ^ si_cnode_size;
dest_root < 2 ^ si_cnode_size;
Some dest_root = dup_caps obj_id;
Some src_index = irq_caps (cap_irq spec_cap)\<rbrakk> \<Longrightarrow>
\<lbrace>\<guillemotleft>object_slot_empty spec t obj_id slot \<and>*
si_irq_cap_at irq_caps spec (cap_irq spec_cap) \<and>*
si_cap_at t dup_caps spec False obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> \<rbrace>
seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
seL4_CapInitThreadCNode src_index 32
\<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_null_irq_cap_at irq_caps spec (cap_irq spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_chain)
apply (rule_tac cnode_cap = si_cspace_cap
and cnode_cap' = si_cnode_cap
and dest_root_cap = "default_cap CNodeType {dest_id} (object_size_bits spec_obj) False"
and root_size=si_cnode_size
and src_root=seL4_CapInitThreadCNode
and src_depth=32
and tcb=root_tcb
and src_cap = " IrqHandlerCap (cap_irq spec_cap)"
in seL4_CNode_Move_sep[where
R = "(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>* si_asid \<and>* R"],
(assumption|simp add: ep_related_cap_default_cap
default_cap_has_type
get_index_def)+)
apply (frule_tac s=s and t=t and dup_caps=dup_caps and irq_caps=irq_caps
in move_pre_irq_handler,(assumption|rule refl|simp)+)
apply (elim conjE)
apply (intro conjI,
simp_all add:has_type_default_not_non ep_related_cap_default_cap)
apply (thin_tac "\<guillemotleft>P \<and>* Q \<guillemotright>s" for P Q)
apply (sep_solve add: sep_any_imp)
apply ((clarsimp simp: si_cnode_cap_def word_bits_def si_cspace_cap_def
dest!: guard_equal_si_cspace_cap |
rule is_cnode_cap_si_cnode_cap)+)[2]
(* it works because si_cnode_cap = si_cspace_cap *)
apply (drule_tac s=s and dest_root=dest_root and src_index=src_index and R=R
in move_post_irq_handler, (assumption|simp)+)
done
lemma seL4_CNode_Move_object_slot_initialised_cap_has_object_sep:
"\<lbrace>\<lambda>s. well_formed spec \<and> original_cap_at (obj_id, slot) spec \<and>
data = cap_data spec_cap \<and>
cap_has_object spec_cap \<and>
cnode_at obj_id spec \<and> cdl_objects spec obj_id = Some spec_obj \<and>
opt_cap (obj_id, slot) spec = Some spec_cap \<and> spec_cap \<noteq> NullCap \<and>
cap_has_type spec_cap \<and> valid_src_cap spec_cap data \<and> (is_device_cap spec_cap = dev) \<and>
\<not>is_untyped_cap spec_cap \<and> is_default_cap spec_cap \<and> \<not> is_asidpool_cap spec_cap \<and>
cdl_objects spec (cap_object spec_cap) = Some spec_cap_obj \<and>
(is_cnode_cap spec_cap \<longrightarrow> object_size_bits spec_cap_obj = cnode_cap_size spec_cap) \<and>
Some dest_root = dup_caps obj_id \<and>
Some src_index = orig_caps (cap_object spec_cap) \<and>
\<guillemotleft>object_slot_empty spec t obj_id slot \<and>*
si_cap_at t orig_caps spec dev (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright> s\<rbrace>
seL4_CNode_Move dest_root (of_nat slot) (of_nat (object_size_bits spec_obj))
seL4_CapInitThreadCNode src_index 32
\<lbrace>\<lambda>_.\<guillemotleft>object_slot_initialised spec t obj_id slot \<and>*
si_null_cap_at t orig_caps spec (cap_object spec_cap) \<and>*
si_cap_at t dup_caps spec dev obj_id \<and>*
object_fields_empty spec t obj_id \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_assume_pre)
apply (elim conjE)
apply (rule hoare_weaken_pre)
apply clarsimp
apply (rule_tac dest_id="the(t obj_id)" and client_object_id="the(t (cap_object spec_cap))"
in seL4_CNode_Move_object_slot_initialised_cap_has_object_sep_helper, (assumption|simp)+)
apply (clarsimp simp: si_cap_at_def sep_conj_exists)
apply (clarsimp simp: si_cap_at_def sep_conj_exists)
apply (sep_drule (direct) si_cap_at_less_si_cnode_size [where cap_ptr = src_index
and R="object_slot_empty spec t obj_id slot \<and>* si_cap_at t dup_caps spec (is_device_cap spec_cap) obj_id \<and>* object_fields_empty spec t obj_id \<and>* si_objects \<and>* R"])
apply (fastforce simp: sep_conj_ac)
apply clarsimp
apply (sep_drule (direct) si_cap_at_less_si_cnode_size [where cap_ptr = dest_root and t=t and spec=spec
and R="object_slot_empty spec t obj_id slot \<and>* si_cap_at t orig_caps spec (is_device_cap spec_cap) (cap_object spec_cap) \<and>* object_fields_empty spec t obj_id \<and>* si_objects \<and>* R"])
apply (fastforce simp: sep_conj_ac)
apply clarsimp+
done