-
Notifications
You must be signed in to change notification settings - Fork 0
/
Untyped_DR.thy
1887 lines (1784 loc) · 87 KB
/
Untyped_DR.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory Untyped_DR
imports CNode_DR
begin
context begin interpretation Arch . (*FIXME: arch_split*)
lemma detype_dcorres:
"S = {ptr..ptr + 2 ^ sz - 1}
\<Longrightarrow> dcorres dc \<top> (\<lambda>s. invs s \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) cref s) \<and> valid_etcbs s)
(modify (Untyped_D.detype S))
(modify (Retype_A.detype S))"
apply (rule corres_modify)
apply (clarsimp simp: transform_def Untyped_D.detype_def
transform_cdt_def
split del: if_split
simp del: untyped_range.simps)
apply (simp add: Untyped_D.detype_def transform_def
transform_current_thread_def Retype_A.detype_def transform_asid_table_def
detype_ext_def wrap_ext_det_ext_ext_def)
apply (rule ext)
apply (clarsimp simp: map_option_case restrict_map_def transform_objects_def
map_add_def cte_wp_at_caps_of_state
split: option.split)
apply (drule valid_global_refsD2)
apply clarsimp
apply (clarsimp simp: global_refs_def transform_object_def detype_ext_def)
done
(* FIXME: move *)
lemma evalMonad_loadWords:
"evalMonad (mapM loadWord xs) ms =
(if (\<forall>x\<in>set xs. is_aligned x 2) then
Some (map (\<lambda>x. word_rcat [underlying_memory ms (x + 3),
underlying_memory ms (x + 2),
underlying_memory ms (x + 1),
underlying_memory ms x]) xs)
else None)"
proof (induct xs)
case Nil thus ?case
by (simp add: evalMonad_def mapM_simps return_def)
next
note mapM_simps[simp]
(* FIXME: could be generalized. *)
have evalMonad_bind_return:
"\<And>f g s. \<forall>x\<in>fst (f s). snd x = s \<Longrightarrow> \<exists>r. \<forall>x\<in>fst (f s). fst x = r \<Longrightarrow>
\<exists>r. \<forall>x\<in>fst (g s). fst x = r \<Longrightarrow>
evalMonad (do r \<leftarrow> f; rs \<leftarrow> g; return (r#rs) od) s =
(case evalMonad f s of None \<Rightarrow> None
| Some r \<Rightarrow> (case evalMonad g s of None \<Rightarrow> None
| Some rs \<Rightarrow> Some (r#rs)))"
apply (simp add: evalMonad_def bind_def split_def return_def)
apply safe
apply auto[2]
apply (rule sym)
apply (rule someI2_ex, fastforce)
apply (clarsimp split: if_split_asm)
apply (rule conjI)
apply (rule someI2_ex, fastforce+)+
done
have loadWord_const:
"\<And>a s. \<forall>x\<in>fst (loadWord a s). snd x = s"
apply (case_tac "is_aligned a 2")
apply (simp add: loadWord_def is_aligned_mask exec_gets)
apply (simp add: return_def)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask)
done
have loadWord_atMostOneResult:
"\<And>a s. \<exists>r. \<forall>x\<in>fst (loadWord a s). fst x = r"
apply (case_tac "is_aligned a 2")
apply (simp add: loadWord_def is_aligned_mask exec_gets)
apply (simp add: return_def)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask)
done
have mapM_loadWord_atMostOneResult[rule_format]:
"\<And>as s. \<exists>rs. \<forall>x\<in>fst (mapM loadWord as s). fst x = rs"
apply (induct_tac as)
apply (simp add: return_def)
using loadWord_const loadWord_atMostOneResult
by (fastforce simp: bind_def split_def return_def)
case Cons thus ?case
by (simp add: evalMonad_bind_return[OF loadWord_const
loadWord_atMostOneResult mapM_loadWord_atMostOneResult]
evalMonad_loadWord is_aligned_mask
split: option.splits)
qed
(* FIXME: change definition! *)
lemma get_ipc_buffer_words_def2:
"get_ipc_buffer_words ms tcb ns \<equiv>
(case tcb_ipcframe tcb of
cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata) \<Rightarrow>
if AllowRead \<in> rights then
(if ns = Nil \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then
map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3),
underlying_memory ms (x + 2),
underlying_memory ms (x + 1),
underlying_memory ms x]) \<circ>
(\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) +
of_nat n * of_nat word_size))
ns
else the None)
else []
| _ \<Rightarrow> [])"
proof -
(* FIXME: extract *)
have mask_eq:
"\<And>p q m n. m\<ge>n \<Longrightarrow> p + (q && mask m) && mask n = p + q && mask n"
by (subst mask_eqs(2)[of p "q && mask m" for p q m, symmetric])
(simp add: mask_twice min_def mask_eqs)
have eq: "\<And>x p b sz. is_aligned (p + (b && mask (pageBitsForSize sz)) +
of_nat x * of_nat word_size) 2
\<longleftrightarrow> is_aligned (p + b) 2"
apply (rule iffI)
apply (drule is_aligned_addD2)
apply (simp add: word_size_def is_aligned_mult_triv2[where n=2,
simplified word_bits_def, simplified])
apply (simp add: is_aligned_mask mask_eq)
apply (rule is_aligned_add)
apply (simp add: is_aligned_mask mask_eq)
apply (simp add: word_size_def is_aligned_mult_triv2[where n=2,
simplified word_bits_def, simplified])
done
show "PROP ?thesis"
apply (rule eq_reflection)
apply (auto simp: get_ipc_buffer_words_def evalMonad_loadWords eq
split: cap.splits arch_cap.splits)
done
qed
lemma is_arch_page_cap_def2:
"is_arch_page_cap cap \<longleftrightarrow>
(\<exists>dev buf rights sz mapdata.
cap = cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata))"
by (simp add: is_arch_page_cap_def split: cap.splits arch_cap.splits)
lemma transform_full_intent_machine_state_eq:
assumes 3: "tcb_ipcframe tcb =
cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz opt)"
assumes 4: "is_aligned buf (pageBitsForSize sz)"
assumes 1: "is_aligned (tcb_ipc_buffer tcb) msg_align_bits"
assumes 5: "(\<forall>p. buf = (p && ~~ mask (pageBitsForSize sz)) \<longrightarrow>
underlying_memory ms' p = underlying_memory ms p)"
shows "transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb"
proof -
have 2: "valid_message_info (get_tcb_message_info tcb)"
by (simp add: get_tcb_message_info_def data_to_message_info_valid)
let ?p = "%x. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) +
of_nat x * of_nat word_size"
have word_rcat_eq:
"\<And>x. x<128 \<Longrightarrow>
word_rcat [underlying_memory ms (?p x + 3),
underlying_memory ms (?p x + 2),
underlying_memory ms (?p x + 1),
underlying_memory ms (?p x)] =
word_rcat [underlying_memory ms'(?p x + 3),
underlying_memory ms'(?p x + 2),
underlying_memory ms'(?p x + 1),
underlying_memory ms'(?p x)]"
proof -
fix x :: nat
assume x: "x<128"
have y: "!!y. y<4 \<Longrightarrow> ?p x + y && ~~ mask (pageBitsForSize sz) = buf"
apply (simp add: add.assoc)
apply (rule is_aligned_add_helper[OF 4, THEN conjunct2])
apply (rule_tac n=msg_align_bits in is_aligned_add_less_t2n)
apply (rule is_aligned_andI1[OF 1])
apply (rule_tac n=2 in is_aligned_add_less_t2n)
apply (simp add: word_size_def)
apply (rule is_aligned_mult_triv2[where n=2, simplified])
apply simp
apply (simp add: msg_align_bits)
apply (simp add: word_size_def)
apply (rule word_less_power_trans_ofnat[where k=2, simplified],
simp_all add: x msg_align_bits word_bits_def)[1]
apply (case_tac sz, simp_all add: msg_align_bits)[1]
apply (rule and_mask_less_size)
apply (case_tac sz, simp_all add: word_size)[1]
done
note 6 = 5[rule_format, OF y[symmetric]]
show "?thesis x"
apply (rule arg_cong[where f=word_rcat])
using 6[of 3] 6[of 2] 6[of 1] 6[of 0]
by simp
qed
show ?thesis
apply (clarsimp simp: transform_full_intent_def Let_def get_tcb_mrs_def
get_ipc_buffer_words_def2 3
Suc_leI[OF msg_registers_lt_msg_max_length]
simp del: upt_Suc
split del: if_split)
apply (case_tac "AllowRead \<in> rights",
simp_all del: upt_Suc split del: if_split)
apply (cut_tac y=2 in is_aligned_weaken[OF 1])
apply (simp add: msg_align_bits)
apply (cut_tac y=2 in is_aligned_weaken[OF 4])
apply (case_tac sz, simp_all)[1]
apply (frule (1) is_aligned_add[of buf 2 "tcb_ipc_buffer tcb"])
apply (simp add: o_def del: upt_Suc)
apply (intro conjI)
apply (rule arg_cong2[where f=transform_intent, OF refl])
apply (rule arg_cong2[where f="(@)", OF refl])
apply (rule arg_cong2[where f=take, OF refl])
apply (rule map_cong[OF refl])
apply (rule word_rcat_eq)
apply (clarsimp simp: atLeastAtMost_upt[symmetric] msg_max_length_def
simp del: upt_Suc)
apply clarsimp
apply (rule word_rcat_eq)
using 2
apply (clarsimp simp: buffer_cptr_index_def msg_max_length_def
valid_message_info_def msg_max_extra_caps_def word_le_nat_alt)
apply (rule arg_cong2[where f="case_list None", OF refl])
apply (rule map_cong[OF refl])
apply (rule word_rcat_eq)
apply (clarsimp simp: atLeastAtMost_upt[symmetric] simp del: upt_Suc)
apply (simp add: msg_max_length_def msg_max_extra_caps_def)
done
qed
lemma valid_page_cap_imp_valid_buf:
"s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False buf rights sz mapdata) \<Longrightarrow>
is_aligned buf (pageBitsForSize sz) \<and> typ_at (AArch (AUserData sz)) buf s"
by (clarsimp simp add: valid_cap_simps cap_aligned_def)
lemma freeMemory_dcorres:
"is_aligned ptr bits \<Longrightarrow> 2 \<le> bits \<Longrightarrow> bits < word_bits \<Longrightarrow>
dcorres dc (\<lambda>_. True)
(pspace_no_overlap_range_cover ptr bits and valid_objs and valid_etcbs)
(return rv) (do_machine_op (freeMemory ptr bits))"
apply (clarsimp simp add: corres_underlying_def split_def return_def)
apply (rename_tac s t)
apply (drule_tac P="(=) s" and
Q="%_ u. (\<exists>ms. u=s\<lparr>machine_state := ms\<rparr>) \<and>
(\<forall>p\<in>UNIV-{ptr..ptr + 2 ^ bits - 1}.
underlying_memory (machine_state s) p =
underlying_memory (machine_state u) p)"
in use_valid)
apply (simp add: do_machine_op_def split_def)
apply wp
apply (clarsimp simp: freeMemory_def mapM_x_storeWord_step[simplified word_size_bits_def]
intvl_range_conv')
apply (rule conjI, fastforce)
apply clarsimp
apply (erule use_valid[where P=P and Q="%_. P" for P])
apply wp
apply (clarsimp simp: is_aligned_no_wrap' of_nat_less_pow_32 word_bits_def
x_power_minus_1 word_plus_mono_right)
apply (rule refl)
apply (rule refl)
apply (clarsimp simp: transform_def transform_current_thread_def)
apply (rule ext)
apply (clarsimp simp: transform_objects_def map_add_def)
apply (clarsimp simp: option_map_def split: option.splits)
apply (clarsimp simp: transform_object_def transform_tcb_def
split: Structures_A.kernel_object.split option.splits)
apply (rename_tac s ms tref etcb tcb)
apply (clarsimp simp: restrict_map_def split: if_split_asm)
apply (frule(1) valid_etcbs_tcb_etcb)
apply (case_tac "\<not> is_arch_page_cap (tcb_ipcframe tcb)")
apply (erule transform_full_intent_no_ipc_buffer)
apply (clarsimp simp: is_arch_page_cap_def2)
apply (simp add: valid_objs_def)
apply (drule_tac x=tref in bspec, clarsimp+)
apply (clarsimp simp: valid_obj_def valid_tcb_def)
(* FIXME: extract a sensible lemma for that *)
apply (drule_tac x="(tcb_ipcframe, tcb_ipcframe_update,
\<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap)" in bspec)
apply (simp add: ran_tcb_cap_cases)
apply clarsimp
apply (thin_tac "case_option x y z" for x y z)
apply (clarsimp simp add: valid_ipc_buffer_cap_def is_nondevice_page_cap_def split: bool.split_asm)
apply (drule valid_page_cap_imp_valid_buf)
apply (frule_tac transform_full_intent_machine_state_eq, simp_all)
apply clarsimp
apply (erule_tac x=p in bspec)
apply (frule is_aligned_no_overflow')
apply (clarsimp simp: pspace_no_overlap_def typ_at_eq_kheap_obj obj_at_def
mask_2pm1[symmetric])
apply (erule_tac x="(p && ~~ mask (pageBitsForSize sz))" in allE)
apply clarsimp
apply (thin_tac "length xs = y" for xs y)
apply (erule impE)
apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help)
apply (erule order_trans[OF word_and_le2])
apply (erule impE)
apply (rule_tac y = p in order_trans)
apply simp
apply (cut_tac ptr = p and n = "pageBitsForSize sz" in word_neg_and_le)
apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help)
apply (thin_tac "x\<noteq>y" for x y)
apply (erule notE)+
apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask])
apply (rule le_refl)
apply (simp add:mask_def not_le pbfs_less_wb'[unfolded word_bits_def, simplified])
done
declare wrap_ext_det_ext_ext_def[simp]
(* Strictly speaking, we would not need ct_active, here. Proving that,
however, requires a stronger version of lemma detype_invariants. *)
lemma delete_objects_dcorres:
notes order_class.Icc_eq_Icc [simp del]
is_aligned_neg_mask_eq[simp del]
is_aligned_neg_mask_weaken[simp del]
assumes S: "S = {ptr..ptr + 2 ^ bits - 1}"
shows "dcorres dc \<top>
(\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>cref dev idx.
cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) cref s
\<and> descendants_range (cap.UntypedCap dev ptr bits idx) cref s) \<and> valid_etcbs s)
(modify (Untyped_D.detype S))
(delete_objects ptr bits)"
apply (clarsimp simp: S)
apply (unfold delete_objects_def2 K_bind_def)
apply (rule corres_bind_return)
apply (rule_tac F="is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits"
in corres_req)
apply clarsimp
apply (drule cte_wp_valid_cap, clarsimp)
apply (simp add: valid_cap_def cap_aligned_def untyped_min_bits_def)
apply (rule corres_name_pre, clarify)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ detype_dcorres])
apply (rule freeMemory_dcorres, simp+)
apply wp
apply clarsimp
apply (rule TrueI)?
apply clarsimp
apply (rule conjI)
apply fastforce
apply (frule cte_wp_valid_cap, clarsimp)
apply (intro conjI)
apply (erule pspace_no_overlap_detype)
apply clarsimp+
apply (frule invs_untyped_children)
apply (drule_tac detype_invariants, simp_all)
apply (clarsimp simp: empty_descendants_range_in descendants_range_def2 invs_def valid_state_def
valid_pspace_def detype_clear_um_independent valid_etcbs_def)
apply (simp add: invs_def valid_state_def valid_pspace_def detype_clear_um_independent valid_etcbs_def
is_etcb_at_def detype_def detype_ext_def st_tcb_at_kh_def obj_at_kh_def obj_at_def)
done
lemma unat_ptr_range_end:
"\<lbrakk> is_aligned (ptr :: 'a :: len word) sz; sz < len_of TYPE('a)\<rbrakk>
\<Longrightarrow> unat (ptr + 2 ^ sz - 1) = unat ptr + 2 ^ sz - 1"
apply (simp only: add_diff_eq[symmetric])
apply (subst unat_plus_simple[THEN iffD1])
apply (simp add: add_diff_eq)
apply (subst unat_minus_one)
apply simp_all
done
definition
translate_object_type :: "Structures_A.apiobject_type \<Rightarrow> cdl_object_type"
where
"translate_object_type type \<equiv> case type of
Structures_A.Untyped \<Rightarrow> UntypedType
| Structures_A.TCBObject \<Rightarrow> TcbType
| Structures_A.EndpointObject \<Rightarrow> EndpointType
| Structures_A.NotificationObject \<Rightarrow> NotificationType
| Structures_A.CapTableObject \<Rightarrow> CNodeType
| ArchObject SmallPageObj \<Rightarrow> FrameType 12
| ArchObject LargePageObj \<Rightarrow> FrameType 16
| ArchObject SectionObj \<Rightarrow> FrameType 20
| ArchObject SuperSectionObj \<Rightarrow> FrameType 24
| ArchObject PageTableObj \<Rightarrow> PageTableType
| ArchObject PageDirectoryObj \<Rightarrow> PageDirectoryType
| ArchObject ASIDPoolObj \<Rightarrow> AsidPoolType"
definition
translate_untyped_invocation :: "Invocations_A.untyped_invocation \<Rightarrow> cdl_untyped_invocation"
where
"translate_untyped_invocation x \<equiv>
case x of Invocations_A.Retype cref reset ptr_base ptr tp us slots dev
\<Rightarrow> cdl_untyped_invocation.Retype
(transform_cslot_ptr cref )
(translate_object_type tp)
us
(map transform_cslot_ptr slots)
(\<not> reset) (length slots)"
definition
"retype_transform_obj_ref type sz ptr
\<equiv> if type = Structures_A.Untyped then {ptr .. ptr + 2^sz - 1}
else {ptr}"
lemma transform_empty_cnode:
"transform_cnode_contents o_bits (empty_cnode o_bits) = empty_cap_map o_bits"
apply (simp add: transform_cnode_contents_def dom_empty_cnode)
apply (rule ext, simp add: option_map_join_def empty_cap_map_def
nat_to_bl_def len_bin_to_bl_aux empty_cnode_def)
done
lemma transform_default_tcb:
"transform_tcb ms x default_tcb (default_etcb\<lparr>tcb_domain := domain\<rparr>)
= Tcb (Types_D.default_tcb domain)"
apply (simp add: transform_tcb_def default_tcb_def Types_D.default_tcb_def default_arch_tcb_def)
apply (simp add: transform_full_intent_def Let_def new_context_def cap_register_def capRegister_def
get_tcb_mrs_def Suc_le_eq get_tcb_message_info_def msg_info_register_def
msgInfoRegister_def data_to_message_info_def arch_tcb_context_get_def
get_ipc_buffer_words_def)
apply (simp add: transform_intent_def invocation_type_def fromEnum_def enum_invocation_label
enum_gen_invocation_labels toEnum_def)
apply (simp add: fun_eq_iff tcb_slot_defs infer_tcb_pending_op_def infer_tcb_bound_notification_def
guess_error_def default_etcb_def default_domain_def)
done
lemma transform_unat_map_empty:
"unat_map (\<lambda>_ :: ('a :: len) word. Some cdl_cap.NullCap)
= empty_cap_map (len_of TYPE('a))"
by (rule ext, simp add: unat_map_def empty_cap_map_def)
lemma transform_default_object:
"\<lbrakk>type \<noteq> Structures_A.Untyped; type = Structures_A.CapTableObject \<longrightarrow> 0 < o_bits\<rbrakk> \<Longrightarrow>
transform_object ms word (default_ext type domain) (Retype_A.default_object type dev o_bits)
= the (Types_D.default_object (translate_object_type type) o_bits domain)"
by (cases type, simp_all add: translate_object_type_def default_object_def
Types_D.default_object_def transform_default_tcb default_ext_def
transform_unat_map_empty transform_empty_cnode
Types_D.empty_cnode_def dom_empty_cnode
transform_object_def default_arch_object_def
transform_page_table_contents_def o_def transform_pte_def
transform_page_directory_contents_def transform_pde_def kernel_pde_mask_def
transform_asid_pool_contents_def transform_asid_pool_entry_def asid_low_bits_def
split: aobject_type.split nat.splits)
lemma obj_bits_bound32:
"\<lbrakk>type = Structures_A.Untyped \<longrightarrow> us < 32; type = Structures_A.CapTableObject \<longrightarrow> us < 28\<rbrakk>
\<Longrightarrow> obj_bits_api type us < word_bits"
apply (case_tac type; simp add: obj_bits_api_def word_bits_def slot_bits_def)
apply (rename_tac aobject_type)
apply (case_tac aobject_type; simp add: arch_kobj_size_def default_arch_object_def pageBits_def)
done
lemma obj_bits_bound4:
"\<lbrakk>type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us\<rbrakk> \<Longrightarrow>
untyped_min_bits \<le> obj_bits_api type us"
apply (case_tac type; simp add: obj_bits_api_def word_bits_def slot_bits_def untyped_min_bits_def)
apply (rename_tac aobject_type)
apply (case_tac aobject_type; simp add:arch_kobj_size_def default_arch_object_def pageBits_def)
done
lemma distinct_retype_addrs:
"\<lbrakk>type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us;
range_cover ptr sz (obj_bits_api type us) n\<rbrakk>
\<Longrightarrow> distinct (retype_addrs ptr type n us)"
supply untyped_min_bits_def[simp]
apply (clarsimp simp:retype_addrs_def distinct_map ptr_add_def inj_on_def)
apply (simp only: shiftl_t2n[symmetric, simplified field_simps, simplified])
apply (drule shiftl_inj_if)
apply (rule shiftl_shiftr_id)
apply (simp add:range_cover_def)
apply (rule word_of_nat_less)
apply (subst unat_power_lower)
apply (rule diff_less)
apply (cut_tac obj_bits_bound4[where us = us and type = type])
apply simp
apply simp
apply (simp add:word_bits_def)
apply (erule Retype_AI.range_cover.range_cover_le_n_less(2))
apply simp
apply (rule shiftl_shiftr_id)
apply (simp add:range_cover_def)
apply (rule word_of_nat_less)
apply (subst unat_power_lower)
apply (rule diff_less)
apply (cut_tac obj_bits_bound4[where us = us and type = type])
apply simp
apply simp
apply (simp add:word_bits_def)
apply (erule Retype_AI.range_cover.range_cover_le_n_less(2))
apply simp
apply (rule of_nat_inj[where 'a=32, THEN iffD1])
apply (simp add:range_cover.range_cover_le_n_less[where 'a=32, simplified])+
done
lemma length_retype_addrs[simp]:
"length (retype_addrs ptr type n us) = n"
by (simp add:retype_addrs_def)
lemma retype_transform_obj_ref_ut:
"(p \<in> (retype_transform_obj_ref Structures_A.Untyped sz ptr)) = (p \<in> {ptr .. ptr + 2^sz - 1})"
by (clarsimp simp:retype_transform_obj_ref_def)
lemma transform_none_to_untyped:
"\<lbrakk>valid_idle s'; kheap s' obj_id = None\<rbrakk>
\<Longrightarrow> cdl_objects (transform s') obj_id = Some Types_D.Untyped"
apply (clarsimp simp: transform_def restrict_map_def map_add_def transform_objects_def)
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
done
lemma retype_transform_obj_ref_available:
"\<lbrakk>pspace_no_overlap_range_cover ptr sz s'; s = transform s'; valid_pspace s'; valid_idle s';
range_cover ptr sz (obj_bits_api ty us) n;
y \<in> set (retype_addrs ptr ty n us)\<rbrakk>
\<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq>
(cdl_objects s) -` {Some Types_D.Untyped}"
apply (clarsimp simp:retype_transform_obj_ref_def | rule conjI)+
apply (rule transform_none_to_untyped, simp)
apply (rule ccontr, clarsimp)
apply (drule(1) retype_addrs_range_subset[where p = y])
apply (drule(1) pspace_no_overlap_obj_range)
apply (simp only: field_simps)
apply (drule(1) disjoint_subset2)
apply (clarsimp simp:obj_bits_api_def)
apply (drule p_in_obj_range)
apply clarsimp+
apply auto[1]
apply (drule(2) pspace_no_overlap_into_Int_none)
apply (clarsimp simp: transform_def restrict_map_def map_add_def transform_objects_def
split: if_splits option.splits)
apply (fastforce simp: valid_idle_def pred_tcb_at_def obj_at_def)
done
lemma retype_transform_obj_ref_pick_id:
"type \<noteq> Structures_A.Untyped
\<Longrightarrow> map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref type us) xs)
= map (retype_transform_obj_ref type us) xs"
by (simp add:retype_transform_obj_ref_def)
lemma translate_object_type_not_untyped:
"type \<noteq> Structures_A.Untyped
\<Longrightarrow> Some (the (Types_D.default_object (translate_object_type type) us current_domain))
= Types_D.default_object (translate_object_type type) us current_domain"
by (clarsimp simp:translate_object_type_def Types_D.default_object_def
split:Structures_A.apiobject_type.splits aobject_type.splits)
lemma retype_transform_obj_ref_not_untyped:
"\<lbrakk>type \<noteq> Structures_A.Untyped\<rbrakk>
\<Longrightarrow>
{x} \<in> retype_transform_obj_ref type us ` set xs = (x \<in> set xs)"
apply (rule iffI)
apply (clarsimp simp:retype_transform_obj_ref_def)+
done
lemma retype_transform_obj_ref_in_untyped_range:
notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff
shows "\<lbrakk>y \<in> set (retype_addrs ptr type n us);
range_cover ptr sz (obj_bits_api type us) n\<rbrakk>
\<Longrightarrow> retype_transform_obj_ref type us y \<subseteq>
{ptr &&~~ mask sz ..(ptr && ~~ mask sz) + (2 ^ sz - 1)}"
apply (frule retype_addrs_subset_ptr_bits)
apply (clarsimp simp:retype_transform_obj_ref_def)
apply (rule conjI)
apply (drule(1) set_mp)
apply clarsimp
apply (erule set_mp[rotated])
apply (frule(1) retype_addrs_range_subset)
apply (simp add:obj_bits_api_def)
apply (erule subset_trans)
apply (clarsimp simp: atLeastatMost_subset_iff field_simps)
apply (rule word_and_le2)
apply clarsimp
apply (erule set_mp[rotated])
apply (erule subset_trans)
apply (clarsimp simp: atLeastatMost_subset_iff field_simps)
apply (rule word_and_le2)
done
lemma retype_region_dcorres:
"dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv'
\<and> rv' = retype_addrs ptr type n us)
\<top>
(\<lambda>s. pspace_no_overlap_range_cover ptr sz s \<and> invs s
\<and> range_cover ptr sz (obj_bits_api type us) n
\<and> (type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us)
\<and> (type = Structures_A.CapTableObject \<longrightarrow> us \<noteq> 0))
(Untyped_D.retype_region
us (translate_object_type type) (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)))
(Retype_A.retype_region ptr n us type dev)"
supply if_cong[cong]
apply (simp add: retype_region_def Untyped_D.retype_region_def
split del: if_split)
apply (clarsimp simp:when_def generate_object_ids_def bind_assoc
split del:if_split)
apply (simp add:retype_addrs_fold split del:if_split)
apply (case_tac "type = Structures_A.Untyped")
apply (rule corres_guard_imp)
apply (simp add:translate_object_type_def)
apply (intro conjI impI ballI | simp)+
apply (simp add:gets_fold_into_modify retype_addrs_fold retype_region_ext_def modify_modify
create_objects_def)
apply (rule dcorres_expand_pfx)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_split)
apply (rule corres_trivial)
apply simp
apply (rule_tac r = dc and Q = \<top> and Q' = "(=) s'" in corres_guard_imp)
apply (clarsimp simp: transform_def bind_def simpler_modify_def corres_underlying_def
transform_current_thread_def transform_cdt_def transform_asid_table_def)
apply (rule ext)
apply (clarsimp simp:foldr_upd_app_if foldr_fun_upd_value restrict_map_def map_add_def
transform_objects_def retype_transform_obj_ref_def image_def)
apply (subgoal_tac "idle_thread s' \<notin> set (retype_addrs ptr type n us)")
apply (subgoal_tac "type = Structures_A.CapTableObject \<longrightarrow> us \<noteq> 0")
apply (clarsimp simp:transform_default_object translate_object_type_not_untyped)
defer
apply clarsimp
apply (frule invs_valid_idle,clarsimp simp:valid_idle_def pred_tcb_at_def obj_at_def)
apply (erule(3) pspace_no_overlapC)
apply clarsimp
apply simp
apply assumption
apply wp+
apply fastforce
apply simp
apply (case_tac type, simp_all add:translate_object_type_def)
apply (rename_tac aobject_type)
apply (case_tac aobject_type,simp_all)
done
lemma page_objects_default_object:
"ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj}
\<Longrightarrow> \<exists>vmsz. (default_object ty dev us = ArchObj (DataPage dev vmsz) \<and> pageBitsForSize vmsz = obj_bits_api ty us)"
by (auto simp: default_object_def default_arch_object_def obj_bits_api_def pageBitsForSize_def)
lemma clearMemory_unused_corres_noop:
"\<lbrakk> ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj};
range_cover ptr sz (obj_bits_api ty us) n;
p \<in> set (retype_addrs ptr ty n us)\<rbrakk>
\<Longrightarrow> dcorres dc \<top>
(\<lambda>s. (\<forall>x \<in> set (retype_addrs ptr ty n us).
obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s
\<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> (obj_refs cap)))
\<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s)
(return ())
(do_machine_op (clearMemory p (2 ^ (obj_bits_api ty us))))"
(is "\<lbrakk> ?def; ?szv; ?in \<rbrakk> \<Longrightarrow> dcorres dc \<top> ?P ?f ?g")
apply (drule page_objects_default_object[where us=us and dev = dev], clarsimp)
apply (rename_tac pgsz)
apply (simp add: clearMemory_def do_machine_op_bind
cleanCacheRange_PoU_def ef_storeWord
mapM_x_mapM dom_mapM)
apply (subst do_machine_op_bind)
apply (clarsimp simp: ef_storeWord
mapM_x_mapM dom_mapM cleanCacheRange_PoU_def cleanByVA_PoU_def)+
apply (rule corres_guard_imp, rule corres_split_noop_rhs)
apply (rule dcorres_machine_op_noop, wp)
apply (rule corres_mapM_to_mapM_x)
apply (rule_tac P=\<top> and P'="?P"
and S="Id \<inter> ({p .. p + 2 ^ (obj_bits_api ty us) - 1} \<times> UNIV)"
in corres_mapM_x[where f="\<lambda>_. return ()", OF _ _ _ refl,
simplified mapM_x_return])
apply clarsimp
apply (rule stronger_corres_guard_imp,
rule_tac sz=pgsz in dcorres_store_word_safe[where dev = dev])
apply (simp add: within_page_def)
apply simp
apply (clarsimp simp: obj_at_def)
apply (subgoal_tac "y && ~~ mask (obj_bits_api ty us) = p")
apply (clarsimp simp: ipc_frame_wp_at_def obj_at_def ran_null_filter
split: cap.split_asm arch_cap.split_asm)
apply (cut_tac t="(t, tcb_cnode_index 4)" and P="(=) cap" for t cap
in cte_wp_at_tcbI, simp, fastforce, simp)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (drule(1) bspec)
apply clarsimp
apply (drule(1) bspec[OF _ ranI])
apply simp
apply (drule(2) retype_addrs_aligned
[OF _ range_cover.aligned range_cover_sz'
[where 'a=32, folded word_bits_def] le_refl])
apply (simp add:mask_in_range)
apply wp
apply (simp | wp hoare_vcg_ball_lift)+
apply (simp add:zip_same_conv_map)
apply (rule conjI)
apply clarsimp
apply (clarsimp simp: word_size_def)
apply (drule subsetD[OF upto_enum_step_subset])
apply simp
apply (wp | simp)+
done
lemma init_arch_objects_corres_noop:
notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff
shows
"\<lbrakk> \<forall>x \<in> set refs. is_aligned x (obj_bits_api ty obj_sz);
range_cover ptr sz (obj_bits_api ty obj_sz) n; 0 < n \<rbrakk>
\<Longrightarrow> dcorres dc \<top>
(\<lambda>s. (ty \<noteq> Structures_A.Untyped \<longrightarrow>
(\<forall>x\<in>set (retype_addrs ptr ty n obj_sz).
obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev obj_sz) x s))
\<and> (\<forall>cap \<in> ran (null_filter (caps_of_state s)).
obj_refs cap \<inter> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} = {})
\<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s)
(return ())
(init_arch_objects ty ptr n obj_sz refs)"
apply (simp add: init_arch_objects_def
split: Structures_A.apiobject_type.split aobject_type.split)
apply (simp add: dcorres_machine_op_noop[THEN corres_guard_imp]
cleanCacheRange_PoU_def machine_op_lift)
apply safe
apply (simp add:mapM_x_mapM)
apply (rule corres_guard_imp)
apply (rule corres_split_noop_rhs)
apply (rule corres_noop[where P=\<top> and P'=valid_idle])
apply (simp add: clearMemory_def do_machine_op_bind
cleanCacheRange_PoU_def ef_storeWord
mapM_x_mapM dom_mapM)
apply (wp mapM_wp' dmo_dwp | simp)+
apply (rule corres_noop[where P=\<top> and P'=valid_idle])
apply simp
apply (rule hoare_strengthen_post, rule mapM_wp')
apply (subst eq_commute, wp copy_global_mappings_dwp)
apply (simp add: obj_bits_api_def arch_kobj_size_def
default_arch_object_def pd_bits_def pageBits_def)
apply (wp mapM_wp' dmo_dwp | simp)+
done
lemma monad_commute_set_cap_cdt:
"monad_commute \<top> (KHeap_D.set_cap ptr cap) (modify (\<lambda>s. s\<lparr>cdl_cdt := cdl_cdt s(ptr2 \<mapsto> ptr3)\<rparr>))"
apply (clarsimp simp:monad_commute_def)
apply (rule sym)
apply (subst bind_assoc[symmetric])
apply (subst oblivious_modify_swap)
apply (simp add: KHeap_D.set_cap_def split_def gets_the_def
KHeap_D.set_object_def)
apply (intro oblivious_bind oblivious_assert impI conjI allI oblivious_select |
simp split: cdl_object.split)+
apply (clarsimp simp:bind_assoc)
done
lemma monad_commute_set_cap_assert:
"monad_commute \<top> (KHeap_D.set_cap ptr cap) (assert F)"
apply (simp add: monad_commute_def
assert_def fail_def bind_def return_def)
apply (subgoal_tac "empty_fail (KHeap_D.set_cap ptr cap)")
apply (clarsimp simp:empty_fail_def)
apply fastforce
apply (simp add:KHeap_D.set_cap_def split_def)
apply (wp|wpc|clarsimp split:cdl_object.splits)+
apply (simp add:KHeap_D.set_object_def)
done
lemma monad_commute_set_cap_gets_cdt:
"monad_commute \<top> (KHeap_D.set_cap ptr cap) (gets cdl_cdt)"
apply (simp add: monad_commute_def gets_def get_def
assert_def fail_def bind_def return_def)
apply auto[1]
apply (rule bexI[rotated])
apply simp
apply simp
apply (drule use_valid)
apply (rule KHeap_D_set_cap_cdl_cdt)
prefer 2
apply (fastforce +)[2]
apply (rule bexI[rotated])
apply simp
apply simp
apply (drule use_valid)
apply (rule KHeap_D_set_cap_cdl_cdt)
prefer 2
apply (fastforce +)[2]
done
lemma set_cap_set_parent_swap:
"do _ \<leftarrow> KHeap_D.set_cap ptr cap; set_parent ptr2 ptr3 od
= do _ \<leftarrow> set_parent ptr2 ptr3; KHeap_D.set_cap ptr cap od"
apply (rule bind_return_eq)
apply (subst bind_assoc)+
apply (rule ext)
apply (subst monad_commute_simple)
apply (simp add:set_parent_def)
apply (rule monad_commute_split)+
apply (rule monad_commute_set_cap_cdt)
apply (rule monad_commute_set_cap_assert)
apply wp
apply (rule monad_commute_set_cap_gets_cdt)
apply clarsimp
apply fastforce
apply fastforce
done
lemma transform_default_cap:
"transform_cap (default_cap type ptr sz dev)
= Types_D.default_cap (translate_object_type type)
(retype_transform_obj_ref type sz ptr) sz dev"
by (cases type,
simp_all add: translate_object_type_def Types_D.default_cap_def
free_range_of_untyped_def
transform_cap_def arch_default_cap_def transform_mapping_def
retype_transform_obj_ref_def vm_read_write_def Nitpick.The_psimp
transform_asid_def asid_high_bits_of_def asid_low_bits_def
split: aobject_type.split)
crunch valid_etcbs[wp]: create_cap_ext valid_etcbs
lemma create_cap_dcorres:
"dcorres dc \<top> (cte_at parent and cte_wp_at ((=) cap.NullCap) slot
and not_idle_thread (fst slot) and valid_idle and valid_etcbs
and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)))
(Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev
(transform_cslot_ptr slot, retype_transform_obj_ref type sz ptr))
(Retype_A.create_cap type sz parent dev (slot, ptr))"
supply if_cong[cong]
apply (simp add: Untyped_D.create_cap_def Retype_A.create_cap_def)
apply (rule stronger_corres_guard_imp)
apply (rule corres_gets_the_bind)
apply (rule corres_underlying_gets_pre_lhs)
apply (rule corres_assert_lhs)
apply (simp add: set_cap_set_parent_swap bind_assoc[symmetric])
apply (rule corres_split_nor)
apply (fold dc_def)
apply (rule set_cap_corres, simp_all add: transform_default_cap)[1]
apply (simp add: bind_assoc set_original_def create_cap_ext_def
set_cdt_modify gets_fold_into_modify update_cdt_list_def
modify_modify set_cdt_list_modify)
apply (rule dcorres_set_parent_helper)
apply (rule_tac P'="\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s)
\<and> cte_at parent s \<and> cte_at slot s"
in corres_modify[where P=\<top>])
apply (clarsimp simp: transform_def transform_current_thread_def
transform_asid_table_def transform_objects_def)
apply (simp add: transform_cdt_def fun_upd_def[symmetric])
apply (subst map_lift_over_upd)
apply (rule_tac P=\<top> and s=s' in transform_cdt_slot_inj_on_cte_at)
apply (auto dest: mdb_cte_atD[rotated] elim!: ranE)[1]
apply simp
apply (wp|simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap not_idle_thread_def)
apply (clarsimp simp: swp_def not_idle_thread_def cte_wp_at_caps_of_state)
apply (drule mdb_cte_at_cdt_null)
apply (clarsimp simp:cte_wp_at_caps_of_state swp_def)
apply (fastforce simp:mdb_cte_at_def)
done
lemma set_cap_default_not_none:
"\<lbrace>\<lambda>s. cte_wp_at (\<lambda>x. slot \<noteq> ptr \<longrightarrow> x \<noteq> cap.NullCap) slot s\<rbrace> CSpaceAcc_A.set_cap (Retype_A.default_cap type a b dev) ptr
\<lbrace>\<lambda>rv s. cte_wp_at ((\<noteq>) cap.NullCap) slot s\<rbrace>"
apply (clarsimp simp:cte_wp_at_caps_of_state valid_def)
apply (drule set_cap_caps_of_state_monad)
apply clarsimp
done
lemma create_cap_mdb_cte_at:
"\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s) (cdt s)
\<and> cte_wp_at ((\<noteq>)cap.NullCap) parent s \<and> cte_at (fst tup) s\<rbrace>
create_cap type sz parent dev tup \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s) (cdt s)\<rbrace>"
apply (simp add: create_cap_def split_def mdb_cte_at_def)
apply (wp hoare_vcg_all_lift set_cap_default_not_none set_cdt_cte_wp_at static_imp_wp dxo_wp_weak
| simp | wps)+
apply (fastforce simp: cte_wp_at_caps_of_state)
done
lemma neg_mask_add_2p_helper:
"\<lbrakk>is_aligned (b::word32) us;us < 32\<rbrakk> \<Longrightarrow> b + 2 ^ us - 1 && ~~ mask us = b"
apply (simp add:p_assoc_help)
apply (rule is_aligned_add_helper[THEN conjunct2]; simp add:less_1_helper)
done
lemma retype_transform_ref_subseteq_strong:
"\<lbrakk>p \<in> set (retype_addrs ptr ty n us);range_cover ptr sz (obj_bits_api ty us) n \<rbrakk>
\<Longrightarrow> retype_transform_obj_ref ty us p \<subseteq> {ptr..ptr + of_nat n * (2::word32) ^ obj_bits_api ty us - 1}"
apply (subgoal_tac "{p .. p + 2 ^ obj_bits_api ty us - 1}
\<subseteq> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}")
apply (erule subset_trans[rotated])
apply (clarsimp simp:retype_transform_obj_ref_def)
apply (rule conjI)
apply (clarsimp simp:obj_bits_api_def)
apply clarsimp
apply (rule is_aligned_no_overflow)
apply (erule retype_addrs_aligned)
apply (erule range_cover.aligned)
apply (drule range_cover.sz,simp add:word_bits_def)
apply (erule range_cover.sz)
apply (case_tac "n = 0")
apply (clarsimp simp:retype_addrs_def)
apply (frule(1) retype_addrs_range_subset)
apply clarsimp
proof -
assume cover:"range_cover ptr sz (obj_bits_api ty us) n"
and mem_p:"p \<in> set (retype_addrs ptr ty n us)"
and not_0:"0 < n"
note n_less = range_cover.range_cover_n_less[OF cover]
have unat_of_nat_m1: "unat (of_nat n - (1::word32)) < n"
using not_0 n_less
by (simp add:unat_of_nat_minus_1)
have decomp:"of_nat n * 2 ^ obj_bits_api ty us = of_nat (n - 1) * 2 ^ obj_bits_api ty us
+ (2 :: word32) ^ obj_bits_api ty us"
apply (simp add:distrib_right[where b = "1::'a::len word",simplified,symmetric])
using not_0 n_less
apply (simp add:unat_of_nat_minus_1 obj_bits_api_def3)
done
show "p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + of_nat n * 2 ^ obj_bits_api ty us - 1"
apply (subst decomp)
apply (simp add:add.assoc[symmetric])
apply (simp add:p_assoc_help)
apply (rule order_trans[OF word_plus_mono_left word_plus_mono_right])
using mem_p not_0
apply (clarsimp simp:retype_addrs_def ptr_add_def shiftl_t2n)
apply (rule word_plus_mono_right)
apply (rule word_mult_le_mono1[OF word_of_nat_le])
using n_less not_0
apply (subst unat_of_nat_minus_1)
apply simp
apply simp
apply (simp add:Set_Interval.ord_class.atLeastLessThan_def)
apply (rule p2_gt_0[THEN iffD2])
using cover
apply (simp add:word_bits_def range_cover_def)
apply (simp only: word_bits_def[symmetric])
using not_0 n_less
apply (clarsimp simp: unat_of_nat_minus_1)
apply (subst unat_power_lower)
using cover
apply (simp add:range_cover_def)
apply (rule nat_less_power_trans2[OF range_cover.range_cover_le_n_less(2),OF cover, folded word_bits_def])
apply (simp add:unat_of_nat_m1 less_imp_le)
using cover
apply (simp add:range_cover_def word_bits_def)
apply (rule machine_word_plus_mono_right_split[where sz = sz])
using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"]
apply (clarsimp simp:unat_of_nat_m1)
using cover
apply (simp add:range_cover_def word_bits_def)
apply (rule olen_add_eqv[THEN iffD2])
apply (subst add.commute[where a = "2^(obj_bits_api ty us) - 1"])
apply (subst p_assoc_help[symmetric])
apply (rule is_aligned_no_overflow)
apply (insert cover)
apply (clarsimp simp:range_cover_def)
apply (erule aligned_add_aligned[OF _ is_aligned_mult_triv2])
apply (simp add:range_cover_def)+
done
qed
lemma generate_object_ids_exec:
notes [simp del] = order_class.Icc_eq_Icc
shows
"dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g
\<Longrightarrow> dcorres r P
(K ((ty = Structures_A.Untyped \<longrightarrow> (untyped_min_bits \<le> us))
\<and> range_cover ptr sz (obj_bits_api ty us) n
\<and> is_aligned ptr (obj_bits_api ty us)
\<and> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range )
and (pspace_no_overlap_range_cover ptr sz) and valid_pspace and valid_idle and P')
(do
t \<leftarrow> generate_object_ids n (translate_object_type ty) free_range;
f t
od) g"
apply (clarsimp simp: generate_object_ids_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (rule corres_guard_imp)
apply (rule_tac x = "(map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))"
in select_pick_corres_asm[rotated])
apply (rule corres_symb_exec_l)
apply (rule_tac F = "rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)"
in corres_gen_asm)
apply clarify
apply assumption
apply (clarsimp simp:return_def exs_valid_def)
apply (rule hoare_vcg_if_split)
apply (wp|simp)+
apply (intro conjI impI)
apply (clarsimp simp:distinct_map distinct_retype_addrs)
apply (clarsimp simp:inj_on_def)
apply (clarsimp simp:retype_transform_obj_ref_def split: if_split_asm)
apply (frule range_cover.sz(1))
apply (drule(1) retype_addrs_aligned[where sz = sz])
apply (clarsimp simp:word_bits_def)
apply (erule range_cover.sz)
apply (drule(1) retype_addrs_aligned[where sz = sz])
apply (clarsimp simp:word_bits_def)
apply (erule range_cover.sz)
apply (subst (asm) range_eq)
apply (clarsimp simp: obj_bits_api_def)
apply simp
apply (clarsimp simp:retype_transform_obj_ref_def split:if_splits)
apply (frule range_cover.sz(1))
apply (drule(1) retype_addrs_aligned[where sz = sz])
apply (clarsimp simp:word_bits_def)
apply (erule range_cover.sz)
apply (drule(1) retype_addrs_aligned[where sz = sz])
apply (clarsimp simp:word_bits_def)
apply (erule range_cover.sz)
apply (clarsimp simp:obj_bits_api_def order_class.Icc_eq_Icc)
apply (drule_tac x = b in neg_mask_mono_le[where n = us])
apply (drule_tac x = a in neg_mask_mono_le[where n = us])
apply (clarsimp simp: neg_mask_add_2p_helper dest!: range_cover_sz')
apply (clarsimp)
apply (intro conjI)
apply (clarsimp simp:retype_transform_obj_ref_def)