-
Notifications
You must be signed in to change notification settings - Fork 0
/
CreateObjects_SI.thy
1423 lines (1365 loc) · 78.4 KB
/
CreateObjects_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 CreateObjects_SI
imports
"DSpecProofs.Retype_DP"
ObjectInitialised_SI
RootTask_SI
SysInit_SI
begin
(*********************************************************
* Rewriting the seL4_Untyped_Retype_sep rule to include *
* that it doesn't delete anything from the CDT. *
*********************************************************)
lemma seL4_Untyped_Retype_has_children_wp:
"\<lbrakk>untyped_cptr < 2 ^ si_cnode_size; ncptr < 2 ^ si_cnode_size\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s. (nt\<noteq> UntypedType \<and> default_object nt (unat ts) minBound = Some obj
\<and> free_range\<subseteq> tot_free_range) \<and>
\<guillemotleft>si_tcb_id \<mapsto>f (Tcb tcb)
\<and>* (si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap
\<and>* (cap_object si_cnode_cap \<mapsto>f CNode (empty_cnode si_cnode_size))
\<and>* (si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev obj_range free_range
\<and>* (si_cnode_id, unat ncptr ) \<mapsto>c NullCap
\<and>* (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
\<and>* (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cnode_cap
\<and>* (cap_object si_cnode_cap, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap
\<and>* R\<guillemotright> s \<and>
(\<not> has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> obj_range = free_range) \<and>
has_children parent (kernel_state s)\<rbrace>
seL4_Untyped_Retype untyped_cptr nt ts
seL4_CapInitThreadCNode node_index 0 ncptr 1
\<lbrace>\<lambda>rv s. has_children parent (kernel_state s)\<rbrace>"
apply (clarsimp simp: has_children_def is_cdt_parent_def)
apply (subst ex_conj_increase)+
apply (rule hoare_ex_wp)+
apply (rule hoare_chain)
apply (rule seL4_Untyped_Retype_inc_no_preempt
[where root_size=si_cnode_size and root_cnode_cap=si_cnode_cap and obj = obj
and ncptr = ncptr and free_range = free_range and tot_free_range = tot_free_range
and obj_range = obj_range])
apply ((intro conjI impI | simp
| clarsimp simp: guard_equal_si_cnode_cap offset_slot_si_cnode_size' )+)
apply (clarsimp simp: has_children_def is_cdt_parent_def)
apply fastforce
apply simp
done
lemma seL4_Untyped_Retype_list_all_has_children_index_wp:
"\<lbrakk>untyped_cptr < 2 ^ si_cnode_size; ncptr < 2 ^ si_cnode_size\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s. (nt\<noteq> UntypedType \<and> default_object nt (unat object_size) minBound = Some obj
\<and> free_range\<subseteq> tot_free_range) \<and>
\<guillemotleft>si_tcb_id \<mapsto>f (Tcb tcb)
\<and>* (si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap
\<and>* (cap_object si_cnode_cap \<mapsto>f CNode (empty_cnode si_cnode_size))
\<and>* (si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev obj_range free_range
\<and>* (si_cnode_id, unat ncptr ) \<mapsto>c NullCap
\<and>* (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
\<and>* (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cnode_cap
\<and>* (cap_object si_cnode_cap, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap
\<and>* R\<guillemotright> s \<and>
(\<not> has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> obj_range = free_range) \<and>
list_all (\<lambda>index. has_children (cnode_id, untyped_slots!index) (kernel_state s)) indices\<rbrace>
seL4_Untyped_Retype untyped_cptr nt object_size
seL4_CapInitThreadCNode node_index 0 ncptr 1
\<lbrace>\<lambda>rv s. list_all (\<lambda>index. has_children (cnode_id, untyped_slots!index) (kernel_state s)) indices\<rbrace>"
apply (case_tac "indices=[]", simp_all)
apply (rule hoare_TrueI)
apply (clarsimp simp: Ball_set_list_all[symmetric])
apply (subst Ball_conj_increase, simp)+
apply (rule hoare_vcg_ball_lift)
apply (rule hoare_pre)
apply (rule seL4_Untyped_Retype_has_children_wp[where free_range = free_range
and obj_range = obj_range and tot_free_range = tot_free_range])
by auto
lemma seL4_Untyped_Retype_sep_cdt_inc:
"\<lbrakk>untyped_cptr < 2 ^ si_cnode_size;
ncptr < 2 ^ si_cnode_size\<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. (nt\<noteq> UntypedType \<and> default_object nt (unat ts) minBound = Some obj
\<and> free_range\<subseteq> tot_free_range) \<and>
\<guillemotleft>si_tcb_id \<mapsto>f (Tcb tcb)
\<and>* (si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap
\<and>* (cap_object si_cnode_cap \<mapsto>f CNode (empty_cnode si_cnode_size))
\<and>* (si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev obj_range free_range
\<and>* (si_cnode_id, unat ncptr ) \<mapsto>c NullCap
\<and>* (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
\<and>* (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cnode_cap
\<and>* (cap_object si_cnode_cap, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap
\<and>* R\<guillemotright> s \<and>
(\<not> has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> obj_range = free_range) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots!index) (kernel_state s)) indices\<rbrace>
seL4_Untyped_Retype untyped_cptr nt ts
seL4_CapInitThreadCNode node_index 0
ncptr 1
\<lbrace>\<lambda>r s. (\<not> r \<longrightarrow> (\<exists>oid free_range'. (\<guillemotleft>
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap
\<and>* si_tcb_id \<mapsto>f (Tcb tcb)
\<and>* (si_cnode_id, unat ncptr) \<mapsto>c (default_cap nt {oid} (unat ts) dev)
\<and>* oid \<mapsto>o obj
\<and>* (cap_object si_cnode_cap \<mapsto>f CNode (empty_cnode si_cnode_size))
\<and>* (\<And>* ptr\<in>tot_free_range - {oid}. ptr \<mapsto>o Untyped)
\<and>* (si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev obj_range free_range'
\<and>* (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cnode_cap
\<and>* (cap_object si_cnode_cap, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap
\<and>* R \<guillemotright> s ) \<and> free_range' \<subseteq> free_range - {oid} \<and> oid \<in> free_range)
\<and> has_children (si_cnode_id,unat untyped_cptr) (kernel_state s))
\<and> (r \<longrightarrow> (\<guillemotleft>
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap
\<and>* si_tcb_id \<mapsto>f (Tcb tcb)
\<and>* (cap_object si_cnode_cap \<mapsto>f CNode (empty_cnode si_cnode_size))
\<and>* (si_cnode_id,unat untyped_cptr) \<mapsto>c UntypedCap dev obj_range free_range
\<and>* (si_cnode_id, unat ncptr) \<mapsto>c NullCap
\<and>* (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
\<and>* (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cnode_cap
\<and>* (cap_object si_cnode_cap, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap
\<and>* R \<guillemotright> s )
\<and> (\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> obj_range = free_range)) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots!index) (kernel_state s)) indices \<rbrace>"
apply (rule hoare_chain)
apply (rule hoare_vcg_conj_lift, rule seL4_Untyped_Retype_sep [where
root_cnode=si_cnode_id and
root_cnode_cap=si_cnode_cap and
root_size=si_cnode_size and
ucptr_slot="unat untyped_cptr" and
ncptr=ncptr and
obj_range=obj_range and
tot_free_range=tot_free_range and
free_range=free_range and
obj=obj and
P=R], (simp add: offset_slot' guard_equal_si_cnode_cap)+)
apply (rule seL4_Untyped_Retype_list_all_has_children_index_wp
[where tcb=tcb and
cnode_id=si_cnode_id and
untyped_slots=untyped_slots and
indices=indices and
obj_range=obj_range and
free_range=free_range], simp)
apply clarsimp
apply clarsimp
apply auto
done
(*****************************************************
* End of rewriting the seL4_Untyped_Retype_sep rule *
*****************************************************)
lemma has_children_map_le:
"\<lbrakk>cdl_cdt s \<subseteq>\<^sub>m cdl_cdt s'; has_children cap_ref s\<rbrakk>
\<Longrightarrow> has_children cap_ref s'"
apply (clarsimp simp: has_children_def is_cdt_parent_def)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (clarsimp simp: map_le_def)
by (metis domIff option.distinct(1))
lemma retype_untyped_wp:
"\<lbrakk>default_object type sz minBound = Some new_object;
available_ids \<subseteq> all_available_ids;
free_cptr < 2 ^ si_cnode_size;
untyped_cptr < 2 ^ si_cnode_size;
sz < 2 ^ word_bits;
type \<noteq> UntypedType\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s. \<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> cover_ids = available_ids) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices\<rbrace>
retype_untyped free_cptr untyped_cptr type sz
\<lbrace>\<lambda>rv s. (\<not>rv \<longrightarrow> (\<exists>new_id available_ids'.
new_id \<in> available_ids \<and> available_ids' \<subseteq> available_ids - {new_id} \<and>
\<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids' \<and>*
(\<And>* obj_id \<in> all_available_ids - {new_id}. (obj_id \<mapsto>o Untyped)) \<and>*
new_id \<mapsto>o new_object \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c default_cap type {new_id} sz dev \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R \<guillemotright> s) \<and>
has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices) \<and>
(rv \<longrightarrow>
\<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> cover_ids = available_ids) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices)\<rbrace>"
(* I would like to remove this later by rewritting seL4_Untyped_Retype_sep *)
apply (subgoal_tac "si_cspace_cap=si_cnode_cap", simp)
apply (unfold retype_untyped_def)
apply (rule hoare_chain)
apply (rule seL4_Untyped_Retype_sep_cdt_inc [where free_range = available_ids and
tot_free_range = all_available_ids and
untyped_slots=untyped_slots and
indices=indices and
obj = new_object and
obj_range=cover_ids and
tcb="obj_tcb root_tcb" and R=R],
(assumption|simp add: unat_of_nat32 |rule offset_slot' [symmetric] guard_equal_si_cnode_cap)+)
apply clarsimp
apply sep_solve
apply (case_tac r)
apply clarsimp
apply sep_solve
apply clarsimp
apply (rule_tac x=oid in exI, clarsimp)
apply (rule_tac x=free_range' in exI, clarsimp)
apply (clarsimp simp: unat_of_nat32)
apply sep_solve
apply (clarsimp simp: si_cspace_cap_def si_cnode_cap_def)
done
lemma retype_untyped_wp_success:
"\<lbrakk>default_object type sz minBound= Some new_object;
available_ids \<subseteq> all_available_ids;
free_cptr < 2 ^ si_cnode_size;
untyped_cptr < 2 ^ si_cnode_size;
sz < 2 ^ word_bits;
type \<noteq> UntypedType\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s. \<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> cover_ids = available_ids) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices\<rbrace>
retype_untyped free_cptr untyped_cptr type sz
\<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> (\<exists>new_id available_ids'.
new_id \<in> available_ids \<and> available_ids' \<subseteq> available_ids - {new_id} \<and>
\<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids' \<and>*
(\<And>* obj_id \<in> all_available_ids - {new_id}. (obj_id \<mapsto>o Untyped)) \<and>*
new_id \<mapsto>o new_object \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c default_cap type {new_id} sz dev \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R \<guillemotright> s) \<and>
has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices\<rbrace>"
by (rule hoare_strengthen_post, rule retype_untyped_wp [where R=R], simp+)
lemma retype_untyped_wp_fail:
"\<lbrakk>default_object type sz minBound = Some new_object;
available_ids \<subseteq> all_available_ids;
free_cptr < 2 ^ si_cnode_size;
untyped_cptr < 2 ^ si_cnode_size;
sz < 2 ^ word_bits;
type \<noteq> UntypedType\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s. \<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> cover_ids = available_ids) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices\<rbrace>
retype_untyped free_cptr untyped_cptr type sz
\<lbrace>\<lambda>rv s. rv \<longrightarrow>
\<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R \<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow> cover_ids = available_ids) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices\<rbrace>"
by (rule hoare_strengthen_post, rule retype_untyped_wp [where R=R], simp+)
lemma retype_untyped_bij_success:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some spec_object;
type = object_type spec_object;
sz = of_nat (object_size_bits spec_object);
unat free_cptr = free_slot;
unat untyped_cptr = untyped_slot;
used_ids \<inter> available_ids = {};
free_cptr < 2 ^ si_cnode_size;
untyped_cptr < 2 ^ si_cnode_size;
type \<noteq> UntypedType\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s.
bij_betw_map t used_spec_ids used_ids \<and>
dom t = used_spec_ids \<and>
obj_id \<notin> used_spec_ids \<and>
available_ids \<subseteq> all_available_ids \<and>
\<guillemotleft>(si_cnode_id, untyped_slot) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, free_slot) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,untyped_slot) (kernel_state s) \<longrightarrow>
cover_ids = available_ids) \<and>
si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices\<rbrace>
retype_untyped free_cptr untyped_cptr type sz
\<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> (\<exists>new_id available_ids'.
bij_betw_map (t(obj_id \<mapsto> new_id))
(insert obj_id used_spec_ids)
(insert new_id used_ids) \<and>
dom (t(obj_id \<mapsto> new_id)) = (insert obj_id used_spec_ids) \<and>
obj_id \<notin> used_spec_ids \<and>
new_id \<in> available_ids \<and>
available_ids' \<subseteq> available_ids - {new_id} \<and>
\<guillemotleft>(si_cnode_id, untyped_slot) \<mapsto>c UntypedCap dev cover_ids available_ids' \<and>*
(\<And>* obj_id \<in> all_available_ids - {new_id}. (obj_id \<mapsto>o Untyped)) \<and>*
object_empty spec (t(obj_id \<mapsto> new_id)) obj_id \<and>*
si_cap_at (t(obj_id \<mapsto> new_id)) (si_caps(obj_id \<mapsto> free_cptr))
spec dev obj_id \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,untyped_slot) (kernel_state s) \<longrightarrow>
cover_ids = available_ids - {new_id})) \<and>
si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs) \<and>
list_all (\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s)) indices\<rbrace>"
apply (frule (1) well_formed_object_slots)
apply (frule (1) well_formed_object_domain)
apply (frule (1) well_formed_object_size_bits_word_bits)
apply (subgoal_tac "sz = object_size_bits spec_object")
apply (subgoal_tac "\<exists>new_object. default_object type (object_size_bits spec_object) minBound =
Some new_object")
apply (erule exE)
apply (rule hoare_assume_pre)
apply (frule offset_slot' [where slot=free_cptr, symmetric])
apply (frule offset_slot' [where slot=untyped_cptr, symmetric])
apply (rule hoare_chain, rule retype_untyped_wp_success [where available_ids=available_ids and
all_available_ids=all_available_ids and
cover_ids=cover_ids and R=R],
(assumption|simp|clarsimp|blast)+)
apply (metis lt_word_bits_lt_pow well_formed_object_size_bits_word_bits)
apply assumption
apply force
apply clarsimp
apply (rule_tac x=new_id in exI)
apply clarsimp
apply (rule conjI)
apply (metis IntI bij_betw_map_fun_updI empty_iff non_dom_eval_eq)
apply (rule_tac x=available_ids' in exI)
apply (clarsimp simp: object_empty_def object_initialised_general_def sep_conj_exists)
apply (clarsimp simp: object_default_state_def)
apply (clarsimp simp: si_cap_at_def)
apply (clarsimp)
apply (clarsimp simp: default_object_def split: cdl_object_type.splits)
apply clarsimp
done
lemma si_cap_at_update:
"\<lbrakk>(si_cap_at t si_caps spec dev obj_id) s; obj_id \<noteq> obj_id'\<rbrakk>
\<Longrightarrow> (si_cap_at t (si_caps(obj_id' \<mapsto> cap_ptr)) spec dev obj_id) s"
by (clarsimp simp: si_cap_at_def)
lemma map_si_cap_at_update_old:
"\<lbrakk>distinct obj_ids; obj_id_index < length obj_ids;
obj_id = obj_ids ! obj_id_index;
(\<And>* map (si_cap_at t si_caps spec dev) (take obj_id_index obj_ids)) s\<rbrakk>
\<Longrightarrow> (\<And>* map (si_cap_at t (si_caps(obj_id \<mapsto> cap_ptr)) spec dev)
(take obj_id_index obj_ids)) s"
apply (erule sep_list_conj_map_impl [rotated])
apply (erule si_cap_at_update)
apply clarsimp
apply (erule (2) take_nth_distinct)
done
lemma map_si_cap_at_update': (* Need better tactics. *)
"\<lbrakk>(\<And>* map (si_cap_at t si_caps spec dev) (take obj_id_index obj_ids) \<and>* R) s;
distinct obj_ids; obj_id_index < length obj_ids;
obj_id = obj_ids ! obj_id_index\<rbrakk>
\<Longrightarrow> (\<And>* map (si_cap_at t (si_caps(obj_id \<mapsto> cap_ptr)) spec dev)
(take obj_id_index obj_ids) \<and>* R) s"
by (drule sep_conj_impl, erule map_si_cap_at_update_old, assumption+)
lemma inter_union_empty:
"\<lbrakk>A \<inter> B = {}; A \<inter> C = {}\<rbrakk>
\<Longrightarrow> A \<inter> (B \<union> C) = {}"
by auto
lemma distinct_sets_union_subs:
"\<lbrakk>C \<subseteq> A; distinct_sets [A,B]\<rbrakk> \<Longrightarrow> A \<union> B - C = A - C \<union> B"
by (fastforce simp: distinct_sets_def)
lemma cap_objects_remove_free_ids_Union:
"n < length untyped_caps
\<Longrightarrow> (\<Union>x\<in>set (untyped_caps [n := remove_free_ids (untyped_caps ! n) new_ids]). cap_objects x)
= (\<Union>x\<in>set untyped_caps. cap_objects x)"
apply (erule Union_list_update_id')
apply simp
done
lemma all_available_ids_updates:
"\<lbrakk>distinct_sets (map cap_free_ids untyped_caps);
all_available_ids = (\<Union>x\<in>set untyped_caps. cap_free_ids x);
new_ids \<subseteq> cap_free_ids (untyped_caps ! n);
n < length untyped_caps\<rbrakk>
\<Longrightarrow> all_available_ids - new_ids =
(\<Union>x\<in>set (untyped_caps [n := remove_free_ids (untyped_caps ! n) new_ids]). cap_free_ids x)"
apply clarsimp
apply (subst upd_conv_take_nth_drop, assumption)
apply (subst id_take_nth_drop, assumption)
apply (clarsimp simp: cap_free_ids_remove_free_ids)
apply (rule distinct_sets_union_subs, assumption)
apply (subst (asm) id_take_nth_drop, assumption)
apply clarsimp
apply (rule inter_union_empty)
apply (frule distinct_sets_append_Cons_disjoint)
apply clarsimp
apply (frule distinct_sets_append2)
apply clarsimp
done
lemma untyped_cap_eq:
"is_untyped_cap cap \<Longrightarrow> UntypedCap (is_device_cap cap) (cap_objects cap) (cap_free_ids cap) = cap"
by (clarsimp simp: cap_type_def cap_free_ids_def split: cdl_cap.splits)
lemma retype_untyped_loop_inv_pre:
"\<lbrakk>untyped_index < length untyped_caps;
obj_id_index < length free_slots;
length untyped_caps = length untyped_slots;
list_all is_untyped_cap untyped_caps\<rbrakk> \<Longrightarrow>
\<guillemotleft>\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(zip untyped_slots untyped_caps) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap) (drop obj_id_index free_slots) \<and>*
\<And>* map (object_empty spec t) (take obj_id_index obj_ids) \<and>*
(\<And>* obj_id\<in>all_available_ids. obj_id \<mapsto>o Untyped) \<and>*
\<And>* map (si_cap_at t si_caps spec dev) (take obj_id_index obj_ids) \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>*
R\<guillemotright> s \<and>
list_all
(\<lambda>index. has_children (si_cnode_id, untyped_slots ! index) (kernel_state s))
[index\<leftarrow>[0..<length untyped_caps] . \<not> is_full_untyped_cap (untyped_caps ! index)]
\<Longrightarrow>
\<guillemotleft>(si_cnode_id, untyped_slots ! untyped_index) \<mapsto>c
UntypedCap (is_device_cap (untyped_caps ! untyped_index)) (cap_objects (untyped_caps ! untyped_index))
(cap_free_ids (untyped_caps ! untyped_index)) \<and>*
(\<And>* obj_id\<in>all_available_ids. obj_id \<mapsto>o Untyped) \<and>*
(si_cnode_id, free_slots ! obj_id_index) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>*
\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(take untyped_index (zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(drop (Suc untyped_index) (zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap) (drop (Suc obj_id_index) free_slots) \<and>*
\<And>* map (object_empty spec t) (take obj_id_index obj_ids) \<and>*
\<And>* map (si_cap_at t si_caps spec dev) (take obj_id_index obj_ids) \<and>*
R\<guillemotright> s \<and>
(\<not> has_children (si_cnode_id, untyped_slots ! untyped_index) (kernel_state s) \<longrightarrow>
cap_objects (untyped_caps ! untyped_index) =
cap_free_ids (untyped_caps ! untyped_index))"
apply (subst (asm) id_take_nth_drop [where i=untyped_index and
xs="zip untyped_slots untyped_caps"], simp)
apply (subst (asm) drop_Suc_nth [where xs="free_slots"], assumption)
apply (subst (asm) sep_conj_map_split [symmetric], simp)
apply (clarsimp simp: sep_conj_assoc)
apply (frule list_all_nth, simp)
apply (clarsimp simp: untyped_cap_eq)
apply (rule conjI)
apply sep_solve
apply (clarsimp simp: Ball_set_list_all[symmetric])
apply (erule_tac x=untyped_index in allE)
apply (clarsimp simp: is_full_untyped_cap_simps)
done
declare [[blast_depth_limit = 1000]]
lemma retype_untyped_loop_inv_post:
"\<lbrakk>untyped_index < length untyped_caps;
obj_id_index < length obj_ids;
obj_id = obj_ids ! obj_id_index;
distinct obj_ids;
length untyped_caps = length untyped_slots;
list_all is_untyped_cap untyped_caps;
distinct_sets (map cap_free_ids untyped_caps);
new_id \<in> cap_free_ids (untyped_caps ! untyped_index)\<rbrakk> \<Longrightarrow>
\<guillemotleft>(si_cnode_id, untyped_slots ! untyped_index) \<mapsto>c
remove_free_ids (untyped_caps ! untyped_index)
(cap_free_ids (untyped_caps ! untyped_index) - available_ids') \<and>*
(\<And>* obj_id\<in>all_available_ids - {new_id}. obj_id \<mapsto>o Untyped) \<and>*
object_empty spec t obj_id \<and>*
si_cap_at t
(si_caps(obj_id \<mapsto> of_nat (free_slots ! obj_id_index)))
spec dev obj_id \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>*
\<And>* map (\<lambda>(slot, y). (si_cnode_id, slot) \<mapsto>c y)
(take untyped_index (zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>(slot, y). (si_cnode_id, slot) \<mapsto>c y)
(drop (Suc untyped_index) (zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap)
(drop (Suc obj_id_index) free_slots) \<and>*
\<And>* map (object_empty spec t) (take obj_id_index obj_ids) \<and>*
\<And>* map (si_cap_at t si_caps spec dev) (take obj_id_index obj_ids) \<and>*
R\<guillemotright> s
\<Longrightarrow>
\<guillemotleft>\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(zip untyped_slots (untyped_caps[untyped_index :=
remove_free_ids (untyped_caps ! untyped_index)
(cap_free_ids (untyped_caps ! untyped_index) - available_ids')])) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap) (drop (Suc obj_id_index) free_slots) \<and>*
\<And>* map (object_empty spec t) (take (Suc obj_id_index) obj_ids) \<and>*
(\<And>* obj_id\<in>all_available_ids - {new_id}. obj_id \<mapsto>o Untyped) \<and>*
\<And>* map (si_cap_at t
(si_caps(obj_id \<mapsto> of_nat (free_slots ! obj_id_index)))
spec dev) (take (Suc obj_id_index) obj_ids) \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s"
apply (subst upd_conv_take_nth_drop, simp)
apply (subst sep_conj_zip_take_drop [symmetric], simp+)
apply (clarsimp simp: sep_conj_assoc)
apply (subst sep_map_take_Suc, assumption)
apply (subst sep_map_take_Suc, assumption)
apply (clarsimp simp: sep_conj_assoc)
apply (sep_drule map_si_cap_at_update' [where
obj_ids = obj_ids and
obj_id = "obj_ids ! obj_id_index" and
cap_ptr = "of_nat (free_slots ! obj_id_index)"])
apply (assumption)+
apply (rule refl)
apply (clarsimp simp: remove_free_ids_def)
apply (fold remove_free_ids_def)
apply (drule list_all_nth, simp)
apply sep_solve
done
lemma sep_map_conj_f_update:
assumes l: "i < length xs"
assumes d: "distinct xs"
assumes u: "\<And>x xs i. xs ! i \<noteq> x \<Longrightarrow> f (t(xs ! i \<mapsto> a')) x = f t x"
shows
"\<And>* map (f (t(xs ! i \<mapsto> a')) ) (take i xs) = \<And>* map (f t) (take i xs)"
apply (insert l d)
apply (rule sym)
apply (induct xs arbitrary: i)
apply clarsimp
apply clarsimp
apply (case_tac i)
apply fastforce
apply clarsimp
apply (subst u)
apply (clarsimp)
apply simp
done
lemma map_object_empty_update:
"\<lbrakk>i < length obj_ids; distinct obj_ids\<rbrakk>
\<Longrightarrow> \<And>* map (object_empty spec (t(obj_ids ! i \<mapsto> obj_id'))) (take i obj_ids)
= \<And>* map (object_empty spec t) (take i obj_ids)"
apply (erule (1) sep_map_conj_f_update)
apply (clarsimp simp: object_empty_def object_initialised_general_def)
done
lemma map_si_cap_at_update:
"\<lbrakk>i < length obj_ids; distinct obj_ids\<rbrakk>
\<Longrightarrow> \<And>* map (si_cap_at (t(obj_ids ! i \<mapsto> obj_id')) si_caps spec dev) (take i obj_ids)
= \<And>* map (si_cap_at t si_caps spec dev) (take i obj_ids)"
apply (erule (1) sep_map_conj_f_update)
apply (clarsimp simp: si_cap_at_def)
done
lemma nth_map':
"\<lbrakk>map f xs = ys; i < length xs\<rbrakk> \<Longrightarrow> f (xs ! i) = ys ! i"
by (metis nth_map)
lemma bij_betw_map_fun_updI2:
"\<lbrakk>x \<notin> A; y \<notin> B; bij_betw_map f A B\<rbrakk> \<Longrightarrow> \<exists>B'. bij_betw_map (f(x \<mapsto> y)) (insert x A) B'"
apply (drule (2) bij_betw_map_fun_updI)
apply fastforce
done
lemma ran_insert_new:
"\<lbrakk>a \<notin> dom m; b \<notin> ran m\<rbrakk> \<Longrightarrow> ran (m(a \<mapsto> b)) = insert b (ran m)"
by auto
lemma remove_free_ids_is_device[simp]:
"is_untyped_cap a \<Longrightarrow> is_device_cap (remove_free_ids a b) = is_device_cap a"
by (simp add: remove_free_ids_def split:cdl_cap.splits)
lemma list_all_conj:
"(list_all P xs \<and> list_all Q xs) = list_all (P and Q) xs"
by (induct xs) auto
lemmas list_all_conjI = list_all_conj[THEN iffD1,unfolded pred_conj_def,OF conjI]
lemma subset_diff_weaken: "A \<subseteq> B - C \<Longrightarrow> A \<subseteq> B"
by blast
lemma disjoint_diff: "(A = A - B) = (A \<inter> B = {})"
by blast
lemma retype_untyped_loop_inv_success:
"\<lbrakk>well_formed spec;
distinct obj_ids;
cdl_objects spec obj_id = Some object;
obj_id_index < length obj_ids;
untyped_index < length untyped_slots;
obj_id_index < length free_slots;
map of_nat untyped_slots = untyped_cptrs;
map of_nat free_slots = free_cptrs;
obj_id = obj_ids ! obj_id_index;
free_cptr = free_cptrs ! obj_id_index;
untyped_cptr = untyped_cptrs ! untyped_index;
type = object_type object;
object_size = of_nat (object_at_pointer_size_bits spec obj_id)\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s. \<exists>untyped_caps t all_available_ids.
\<guillemotleft>\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(zip untyped_slots untyped_caps) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap) (drop obj_id_index free_slots) \<and>*
\<And>* map (object_empty spec t) (take obj_id_index obj_ids) \<and>*
(\<And>* obj_id\<in>all_available_ids. obj_id \<mapsto>o Untyped) \<and>*
\<And>* map (si_cap_at t si_caps spec dev) (take obj_id_index obj_ids) \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
length untyped_slots = length untyped_caps \<and>
list_all is_untyped_cap untyped_caps \<and>
list_all (\<lambda>c. is_device_cap c = dev) untyped_caps \<and>
list_all well_formed_untyped_cap untyped_caps \<and>
list_all (\<lambda>n. n < 2 ^ si_cnode_size) untyped_slots \<and>
list_all (\<lambda>n. n < 2 ^ si_cnode_size) free_slots \<and>
distinct_sets (map cap_free_ids untyped_caps) \<and>
(\<Union>x\<in>set untyped_caps. cap_free_ids x) \<subseteq> all_available_ids \<and>
bij_betw_map t (set (take obj_id_index obj_ids)) (ran t) \<and>
dom t = set (take obj_id_index obj_ids) \<and>
ran t \<subseteq> ((\<Union>x\<in>set untyped_caps. cap_objects x) - (\<Union>x\<in>set untyped_caps. cap_free_ids x)) \<and>
list_all (\<lambda>index. \<not>has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \<longrightarrow>
is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots] \<and>
si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs)\<rbrace>
retype_untyped free_cptr untyped_cptr type object_size
\<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> (\<exists>untyped_caps t all_available_ids.
\<guillemotleft>\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(zip untyped_slots untyped_caps) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap) (drop (Suc obj_id_index) free_slots) \<and>*
\<And>* map (object_empty spec t)
(take (Suc obj_id_index) obj_ids) \<and>*
(\<And>* obj_id\<in>all_available_ids. obj_id \<mapsto>o Untyped) \<and>*
\<And>* map (si_cap_at t (si_caps(obj_id \<mapsto> free_cptr)) spec dev)
(take (Suc obj_id_index) obj_ids) \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
length untyped_slots = length untyped_caps \<and>
list_all is_untyped_cap untyped_caps \<and>
list_all (\<lambda>c. is_device_cap c = dev) untyped_caps \<and>
list_all well_formed_untyped_cap untyped_caps \<and>
distinct_sets (map cap_free_ids untyped_caps) \<and>
(\<Union>x\<in>set untyped_caps. cap_free_ids x) \<subseteq> all_available_ids \<and>
bij_betw_map t (set (take (Suc obj_id_index) obj_ids)) (ran t) \<and>
dom t = set (take (Suc obj_id_index) obj_ids) \<and>
ran t \<subseteq> ((\<Union>x\<in>set untyped_caps. cap_objects x) - (\<Union>x\<in>set untyped_caps. cap_free_ids x)) \<and>
list_all (\<lambda>index. \<not>has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \<longrightarrow>
is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots] \<and>
si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs))\<rbrace>"
apply (subst list_all_imp_filter2)+
apply (rule hoare_ex_pre hoare_ex_pre_conj)+
apply (rule hoare_grab_asm2)+
apply (rule hoare_chain)
apply (rule_tac used_spec_ids = "set (take obj_id_index obj_ids)" and
available_ids = "cap_free_ids (untyped_caps ! untyped_index)" and
all_available_ids = all_available_ids and
used_ids = "ran t" and
cover_ids = "cap_objects (untyped_caps ! untyped_index)" and
obj_id = "obj_ids ! obj_id_index" and
free_slot = "free_slots ! obj_id_index" and
untyped_slot = "untyped_slots ! untyped_index" and
si_caps = si_caps and
spec = spec and
spec_object = "the (cdl_objects spec (obj_ids ! obj_id_index))" and
R = "\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(take untyped_index (zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(drop (Suc untyped_index)
(zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap)
(drop (Suc obj_id_index) free_slots) \<and>*
\<And>* map (object_empty spec t)
(take obj_id_index obj_ids) \<and>*
\<And>* map (si_cap_at t si_caps spec dev)
(take obj_id_index obj_ids) \<and>* R" and
indices = "[index\<leftarrow>[0..<length untyped_slots].
\<not> is_full_untyped_cap (untyped_caps ! index)]" and
untyped_slots = untyped_slots and
free_cptrs=free_cptrs and t=t and
obj_id_index=obj_id_index and obj_ids=obj_ids
in retype_untyped_bij_success,
(assumption|simp|clarsimp)+)
apply (drule list_all_nth [where xs=free_slots], simp)
apply (metis of_nat_less_pow_32 offset_slot_si_cnode_size
offset_slot' si_cnode_size_less_than_word_size)
apply simp
apply (drule list_all_nth [where xs=untyped_slots], simp)
apply (metis (mono_tags) le_unat_uoi less_or_eq_imp_le nth_map
si_cnode_size_less_than_word_size unat_power_lower32)
apply force
apply (drule list_all_nth [where xs=free_slots], simp)
apply (metis nth_map' of_nat_less_pow_32 si_cnode_size_less_than_word_size)
apply (drule list_all_nth [where xs=untyped_slots], simp)
apply (metis nth_map' of_nat_less_pow_32 si_cnode_size_less_than_word_size)
apply (frule (1) well_formed_object_untyped, simp)
apply (clarsimp)
apply (rule conjI)
apply clarsimp
apply (erule (2) take_nth_distinct)
apply (rule conjI)
apply (metis UN_subset_iff nth_mem)
apply (rule retype_untyped_loop_inv_pre, simp+)
apply (clarsimp)
apply (rule_tac x="untyped_caps[untyped_index :=
remove_free_ids (untyped_caps ! untyped_index)
((cap_free_ids (untyped_caps ! untyped_index)) - available_ids')]" in exI)
apply (rule_tac x="t(obj_ids ! obj_id_index \<mapsto> new_id)" in exI)
apply (rule_tac x="all_available_ids - {new_id}" in exI)
apply (rule conjI)
apply (rule retype_untyped_loop_inv_post, simp+)
apply (subst map_object_empty_update, assumption+)
apply (subst map_si_cap_at_update, assumption+)
apply (subst remove_free_ids_simps)
apply (rule list_all_nth, assumption, assumption)
apply fast
apply (drule list_all_nth [where P = "\<lambda>c. is_device_cap c = dev"], simp)
apply simp
apply (rule conjI)
apply (subst length_list_update, rule refl)
apply (subst (asm) take_insert_nth, assumption)
apply (subst conj_assoc[symmetric])
apply (subst list_all_conj)
apply (rule conjI)
apply (rule list_all_update,simp)
apply (rule list_all_conjI,simp+)
apply (rule conjI)
apply (erule (1) list_all_update)
apply (erule well_formed_untyped_cap_remove_free_ids)
apply (rule conjI)
apply (erule (1) distinct_sets_map_update)
apply (subst cap_free_ids_remove_free_ids)
apply clarsimp
apply (rule conjI)
apply (subst all_available_ids_updates [symmetric], (assumption|rule refl|clarsimp)+)
apply fast
apply (rule conjI)
apply (subst ran_insert_new, simp, force)
apply clarsimp
apply (rule conjI)
apply (rule take_insert_nth)
apply clarsimp
apply (rule conjI)
apply (subst all_available_ids_updates [symmetric], (assumption|rule refl)+)
apply fast
apply simp
apply (subst cap_objects_remove_free_ids_Union [where n=untyped_index], assumption)
apply clarsimp
apply (drule list_all_nth [where P = well_formed_untyped_cap], simp)
apply (drule list_all_nth [where P = is_untyped_cap], simp)
apply (subst (asm) well_formed_untyped_cap_simps, assumption)
apply (subst (asm) ran_insert_new, simp, force)
apply (rule conjI)
apply auto[1]
apply blast
apply (clarsimp simp: Ball_set_list_all[symmetric])
apply (erule_tac x=x in allE)
apply (case_tac "x=untyped_index", simp_all)
apply (clarsimp simp: is_full_untyped_cap_simps disjoint_diff)
done
lemma retype_untyped_bij_fail:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some spec_object;
type = object_type spec_object;
sz = of_nat (object_size_bits spec_object);
free_cptr < 2 ^ si_cnode_size;
untyped_cptr < 2 ^ si_cnode_size;
used_ids \<inter> available_ids = {}\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s.
bij_betw_map t used_spec_ids used_ids \<and> obj_id \<notin> used_spec_ids \<and>
available_ids \<subseteq> all_available_ids \<and>
\<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow>
cover_ids = available_ids) \<and>
list_all (\<lambda>index. \<not>has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \<longrightarrow>
is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots]\<rbrace>
retype_untyped free_cptr untyped_cptr type sz
\<lbrace>\<lambda>rv s. rv \<longrightarrow>
(bij_betw_map t used_spec_ids used_ids \<and> obj_id \<notin> used_spec_ids \<and>
available_ids \<subseteq> all_available_ids \<and>
\<guillemotleft>(si_cnode_id, unat untyped_cptr) \<mapsto>c UntypedCap dev cover_ids available_ids \<and>*
(\<And>* obj_id \<in> all_available_ids. (obj_id \<mapsto>o Untyped)) \<and>*
(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
(\<not>has_children (si_cnode_id,unat untyped_cptr) (kernel_state s) \<longrightarrow>
cover_ids = available_ids) \<and>
list_all (\<lambda>index. \<not>has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \<longrightarrow>
is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots])\<rbrace>"
apply (subgoal_tac "sz = object_size_bits spec_object")
apply (subgoal_tac "\<exists>new_object. default_object type (object_size_bits spec_object) minBound =
Some new_object")
apply (erule exE)
apply (rule hoare_grab_asm)+
apply (rule hoare_weaken_pre)
apply simp
apply (frule offset_slot' [where slot=untyped_cptr, symmetric])
apply (frule offset_slot' [where slot=free_cptr, symmetric])
apply (rule hoare_strengthen_post)
apply (rule retype_untyped_wp_fail
[where available_ids=available_ids and
all_available_ids=all_available_ids and
cover_ids=cover_ids and
untyped_slots=untyped_slots and
indices = "[index\<leftarrow>[0..<length untyped_slots].
\<not> is_full_untyped_cap (untyped_caps ! index)]" and
R=R], simp+)
apply (metis lt_word_bits_lt_pow well_formed_object_size_bits_word_bits)
apply (frule (1) well_formed_object_untyped, simp)
apply clarsimp
apply (subst list_all_imp_filter2, simp)
apply clarsimp
apply (subst (asm) list_all_imp_filter2, simp)
apply (clarsimp simp: default_object_def split: cdl_object_type.splits)
apply clarsimp
done
lemma conjI2:
"\<lbrakk>P \<and> Q; R\<rbrakk> \<Longrightarrow> P \<and> Q \<and> R"
by fast
lemma retype_untyped_loop_inv_fail:
"\<lbrakk>well_formed spec;
distinct obj_ids;
cdl_objects spec obj_id = Some object;
obj_id_index < length obj_ids;
untyped_index < length untyped_slots;
obj_id_index < length free_slots;
map of_nat untyped_slots = untyped_cptrs;
map of_nat free_slots = free_cptrs;
obj_id = obj_ids ! obj_id_index;
free_cptr = free_cptrs ! obj_id_index;
untyped_cptr = untyped_cptrs ! untyped_index;
type = object_type object;
object_size = of_nat (object_at_pointer_size_bits spec obj_id)\<rbrakk>
\<Longrightarrow>
\<lbrace>\<lambda>s. \<exists>untyped_caps t all_available_ids.
\<guillemotleft>\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(zip untyped_slots untyped_caps) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap) (drop obj_id_index free_slots) \<and>*
\<And>* map (object_empty spec t) (take obj_id_index obj_ids) \<and>*
(\<And>* obj_id \<in> all_available_ids. obj_id \<mapsto>o Untyped) \<and>*
\<And>* map (si_cap_at t si_caps spec dev) (take obj_id_index obj_ids) \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
length untyped_slots = length untyped_caps \<and>
list_all is_untyped_cap untyped_caps \<and>
list_all (\<lambda>c. is_device_cap c = dev) untyped_caps \<and>
list_all well_formed_untyped_cap untyped_caps \<and>
list_all (\<lambda>n. n < 2 ^ si_cnode_size) untyped_slots \<and>
list_all (\<lambda>n. n < 2 ^ si_cnode_size) free_slots \<and>
distinct_sets (map cap_free_ids untyped_caps) \<and>
(\<Union>x\<in>set untyped_caps. cap_free_ids x) \<subseteq> all_available_ids \<and>
bij_betw_map t (set (take obj_id_index obj_ids)) (ran t) \<and>
dom t = set (take obj_id_index obj_ids) \<and>
ran t \<subseteq> ((\<Union>x\<in>set untyped_caps. cap_objects x) - (\<Union>x\<in>set untyped_caps. cap_free_ids x)) \<and>
list_all (\<lambda>index. \<not>has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \<longrightarrow>
is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots] \<and>
si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs)\<rbrace>
retype_untyped free_cptr untyped_cptr type object_size
\<lbrace>\<lambda>rv s. rv \<longrightarrow> (\<exists>untyped_caps t all_available_ids.
\<guillemotleft>\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(zip untyped_slots untyped_caps) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap) (drop obj_id_index free_slots) \<and>*
\<And>* map (object_empty spec t)
(take obj_id_index obj_ids) \<and>*
(\<And>* obj_id \<in> all_available_ids. obj_id \<mapsto>o Untyped) \<and>*
\<And>* map (si_cap_at t si_caps spec dev)
(take obj_id_index obj_ids) \<and>*
si_tcb_id \<mapsto>f root_tcb \<and>*
(si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* R\<guillemotright> s \<and>
length untyped_slots = length untyped_caps \<and>
list_all is_untyped_cap untyped_caps \<and>
list_all (\<lambda>c. is_device_cap c = dev) untyped_caps \<and>
list_all well_formed_untyped_cap untyped_caps \<and>
distinct_sets (map cap_free_ids untyped_caps) \<and>
(\<Union>x\<in>set untyped_caps. cap_free_ids x) \<subseteq> all_available_ids \<and>
bij_betw_map t (set (take obj_id_index obj_ids)) (ran t) \<and>
dom t = set (take obj_id_index obj_ids) \<and>
ran t \<subseteq> ((\<Union>x\<in>set untyped_caps. cap_objects x) - (\<Union>x\<in>set untyped_caps. cap_free_ids x)) \<and>
list_all (\<lambda>index. \<not>has_children (si_cnode_id,untyped_slots!index) (kernel_state s) \<longrightarrow>
is_full_untyped_cap (untyped_caps!index)) [0 ..< length untyped_slots] \<and>
si_caps = map_of (zip (take obj_id_index obj_ids) free_cptrs))\<rbrace>"
apply (subst list_all_imp_filter2)+
apply (rule valid_imp_ex)+
apply (rule hoare_ex_pre hoare_ex_pre_conj)+
apply (rule hoare_grab_asm2)+
apply (rule hoare_chain)
apply (rule_tac used_spec_ids1 = "set (take obj_id_index obj_ids)" and
available_ids1 = "cap_free_ids (untyped_caps ! untyped_index)" and
all_available_ids1 = all_available_ids and
used_ids1 = "ran t" and
cover_ids1 = "cap_objects (untyped_caps ! untyped_index)" and
free_cptr1 = free_cptr and
untyped_cptr1 = untyped_cptr and
t1 = t and
R1 = "\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(take untyped_index (zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>(slot, cap). (si_cnode_id, slot) \<mapsto>c cap)
(drop (Suc untyped_index) (zip untyped_slots untyped_caps)) \<and>*
\<And>* map (\<lambda>slot. (si_cnode_id, slot) \<mapsto>c NullCap)
(drop (Suc obj_id_index) free_slots) \<and>*
\<And>* map (object_empty spec t)
(take obj_id_index obj_ids) \<and>*
\<And>* map (si_cap_at t si_caps spec dev)
(take obj_id_index obj_ids) \<and>* R" and
untyped_slots1 = untyped_slots and
untyped_caps1 = untyped_caps and
P' = "\<lambda>s. si_caps = map_of (zip (take obj_id_index obj_ids)
free_cptrs)" and
Q' = "\<lambda>rv s. si_caps = map_of (zip (take obj_id_index obj_ids)
free_cptrs)"
in hoare_vcg_conj_lift [OF retype_untyped_bij_fail],
(assumption|simp|clarsimp)+)
apply (drule list_all_nth [where xs=free_slots], simp)
apply (metis of_nat_less_pow_32 si_cnode_size_less_than_word_size)
apply (drule list_all_nth [where xs=untyped_slots], simp)
apply (metis nth_map' of_nat_less_pow_32 si_cnode_size_less_than_word_size)
apply clarsimp
apply (drule list_all_nth [where xs=free_slots], simp)
apply (metis (hide_lams, no_types) Diff_disjoint Int_commute UN_nth_mem disjoint_subset2)
apply simp
apply wp
apply (clarsimp)
apply (rule conjI)
apply (metis take_nth_distinct)
apply (rule conjI)