-
Notifications
You must be signed in to change notification settings - Fork 0
/
CSpace_C.thy
4149 lines (3676 loc) · 181 KB
/
CSpace_C.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
theory CSpace_C
imports CSpaceAcc_C Machine_C
begin
context kernel_m
begin
lemma maskCapRights_cap_cases:
"return (maskCapRights R c) =
(case c of
ArchObjectCap ac \<Rightarrow> return (ArchRetypeDecls_H.maskCapRights R ac)
| EndpointCap _ _ _ _ _ \<Rightarrow>
return (capEPCanGrant_update
(\<lambda>_. capEPCanGrant c \<and> capAllowGrant R)
(capEPCanReceive_update
(\<lambda>_. capEPCanReceive c \<and> capAllowRead R)
(capEPCanSend_update
(\<lambda>_. capEPCanSend c \<and> capAllowWrite R) c)))
| AsyncEndpointCap _ _ _ _ \<Rightarrow>
return (capAEPCanReceive_update
(\<lambda>_. capAEPCanReceive c \<and> capAllowRead R)
(capAEPCanSend_update
(\<lambda>_. capAEPCanSend c \<and> capAllowWrite R) c))
| _ \<Rightarrow> return c)"
apply (simp add: maskCapRights_def Let_def split del: split_if)
apply (cases c, simp_all add: isCap_simps split del: split_if)
done
lemma imp_ignore: "B \<Longrightarrow> A \<longrightarrow> B" by blast
lemma wordFromVMRights_spec:
"\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromVMRights_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>vm_rights\<rbrace>"
by vcg simp?
lemma vmRightsFromWord_spec:
"\<forall>s. \<Gamma> \<turnstile> {s} Call vmRightsFromWord_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>w\<rbrace>"
by vcg simp?
lemmas vmrights_defs =
Kernel_C.VMNoAccess_def
Kernel_C.VMReadOnly_def
Kernel_C.VMKernelOnly_def
Kernel_C.VMReadWrite_def
lemma maskVMRights_spec:
"\<forall>s. \<Gamma> \<turnstile> ({s} \<inter>
\<lbrace> \<acute>vm_rights && mask 2 = \<acute>vm_rights \<rbrace>)
Call maskVMRights_'proc
\<lbrace> vmrights_to_H \<acute>ret__unsigned_long =
maskVMRights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) (cap_rights_to_H (cap_rights_lift \<^bsup>s\<^esup>cap_rights_mask)) \<and>
\<acute>ret__unsigned_long && mask 2 = \<acute>ret__unsigned_long \<rbrace>"
apply vcg
apply clarsimp
apply (rule conjI)
apply (auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs
split: bool.split)[1]
apply clarsimp
apply (subgoal_tac "vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3")
apply (auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs
cap_rights_to_H_def cap_rights_lift_def
to_bool_def mask_def
split: bool.splits)[1]
apply (subst(asm) mask_eq_iff_w2p)
apply (simp add: word_size)
apply (rule ccontr, clarsimp)
apply (drule inc_le, simp, drule(1) order_le_neq_trans [OF _ not_sym])+
apply (drule inc_le, simp)
done
lemma small_frame_cap_rights [simp]:
"cap_get_tag cap = scast cap_small_frame_cap
\<Longrightarrow> cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) && mask 2 =
cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap)"
apply (simp add: cap_small_frame_cap_lift_def)
apply (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs)
done
lemma frame_cap_rights [simp]:
"cap_get_tag cap = scast cap_frame_cap
\<Longrightarrow> cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) && mask 2 =
cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)"
apply (simp add: cap_frame_cap_lift_def)
apply (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs)
done
lemma Arch_maskCapRights_ccorres [corres]:
"ccorres ccap_relation ret__struct_cap_C_'
\<top>
(UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap arch_cap) \<acute>cap\<rbrace> \<inter>
\<lbrace>ccap_rights_relation R \<acute>cap_rights_mask\<rbrace>)
[]
(return (ArchRetypeDecls_H.maskCapRights R arch_cap))
(Call Arch_maskCapRights_'proc)"
apply (cinit' (trace) lift: cap_' cap_rights_mask_')
apply csymbr
apply (unfold ArchRetype_H.maskCapRights_def)
apply (simp only: Let_def)
apply (case_tac "cap_get_tag cap = scast cap_small_frame_cap")
apply (clarsimp simp add: ccorres_cond_iffs cap_get_tag_isCap isCap_simps)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: cap_get_tag_isCap isCap_simps)
apply (clarsimp simp: return_def)
apply (unfold ccap_relation_def)[1]
apply (simp add: cap_small_frame_cap_lift [THEN iffD1])
apply (clarsimp simp: cap_to_H_def)
apply (simp add: map_option_case split: option.splits)
apply (clarsimp simp add: cap_to_H_def Let_def split: cap_CL.splits split_if_asm)
apply (simp add: cap_small_frame_cap_lift_def)
apply (simp add: ccap_rights_relation_def)
apply (simp add: cap_small_frame_cap_lift_def)
apply (simp add: ccap_rights_relation_def)
apply (simp add: pageSize_def)
apply (simp add: pageSize_def)
apply (clarsimp simp add: cap_get_tag_isCap isCap_simps)
apply (rule conjI, clarsimp)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_guard_imp)
apply (csymbr)
apply (case_tac "cap_get_tag cap = scast cap_frame_cap")
apply (clarsimp simp add: ccorres_cond_iffs cap_get_tag_isCap isCap_simps)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: cap_get_tag_isCap isCap_simps)
apply (clarsimp simp: return_def)
apply (unfold ccap_relation_def)[1]
apply (simp add: cap_frame_cap_lift [THEN iffD1])
apply (clarsimp simp: cap_to_H_def)
apply (simp add: map_option_case split: option.splits)
apply (clarsimp simp add: isCap_simps pageSize_def cap_to_H_def Let_def
split: cap_CL.splits split_if_asm)
apply (simp add: cap_frame_cap_lift_def)
apply (simp add: ccap_rights_relation_def)
apply (simp add: c_valid_cap_def cl_valid_cap_def cap_lift_frame_cap)
apply (simp add: cap_frame_cap_lift_def)
apply (simp add: ccap_rights_relation_def)
apply (simp add: c_valid_cap_def cl_valid_cap_def cap_lift_frame_cap)
apply (clarsimp simp add: cap_get_tag_isCap isCap_simps)
apply (rule conjI, clarsimp)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp add: return_def)
apply (cases arch_cap, simp_all)[1]
apply simp
apply clarsimp
apply clarsimp
done
lemma to_bool_mask_to_bool_bf:
"to_bool (x && mask (Suc 0)) = to_bool_bf (x::word32)"
apply (simp add: to_bool_bf_def to_bool_def)
apply (rule iffI)
prefer 2
apply simp
apply (subgoal_tac "x && mask (Suc 0) < 2^(Suc 0)")
apply simp
apply (drule word_less_cases [where y=2])
apply auto[1]
apply (rule and_mask_less')
apply simp
done
lemma to_bool_cap_rights_bf:
"to_bool (capAllowRead_CL (cap_rights_lift R)) =
to_bool_bf (capAllowRead_CL (cap_rights_lift R))"
"to_bool (capAllowWrite_CL (cap_rights_lift R)) =
to_bool_bf (capAllowWrite_CL (cap_rights_lift R))"
"to_bool (capAllowGrant_CL (cap_rights_lift R)) =
to_bool_bf (capAllowGrant_CL (cap_rights_lift R))"
by (subst to_bool_bf_to_bool_mask,
simp add: cap_rights_lift_def mask_def word_bw_assocs, simp)+
lemma to_bool_aep_cap_bf:
"cap_lift c = Some (Cap_async_endpoint_cap cap) \<Longrightarrow>
to_bool (capAEPCanSend_CL cap) = to_bool_bf (capAEPCanSend_CL cap) \<and>
to_bool (capAEPCanReceive_CL cap) = to_bool_bf (capAEPCanReceive_CL cap)"
apply (simp add:cap_lift_def Let_def split: split_if_asm)
apply (subst to_bool_bf_to_bool_mask,
clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+
apply simp
done
lemma to_bool_ep_cap_bf:
"cap_lift c = Some (Cap_endpoint_cap cap) \<Longrightarrow>
to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \<and>
to_bool (capCanReceive_CL cap) = to_bool_bf (capCanReceive_CL cap) \<and>
to_bool (capCanGrant_CL cap) = to_bool_bf (capCanGrant_CL cap)"
apply (simp add:cap_lift_def Let_def split: split_if_asm)
apply (subst to_bool_bf_to_bool_mask,
clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+
apply simp
done
lemma isArchCap_spec:
"\<forall>s. \<Gamma>\<turnstile> {s} Call isArchCap_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag (cap_' s)))\<rbrace>"
apply vcg
apply (clarsimp simp: from_bool_def isArchCap_tag_def bool.split)
apply (clarsimp simp: word_mod_2p_is_mask[where n=1, simplified] mask_def)
apply word_bitwise
done
lemma maskCapRights_ccorres [corres]:
"ccorres ccap_relation ret__struct_cap_C_'
\<top>
(UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>ccap_rights_relation R \<acute>cap_rights\<rbrace>)
[]
(return (RetypeDecls_H.maskCapRights R cap)) (Call maskCapRights_'proc)"
apply (cinit' lift: cap_' cap_rights_')
apply csymbr
apply (simp add: maskCapRights_cap_cases cap_get_tag_isCap del: Collect_const)
apply wpc
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply (simp add: cap_get_tag_isCap isCap_simps return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply (simp add: cap_get_tag_isCap isCap_simps return_def)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply clarsimp
apply (unfold ccap_relation_def)[1]
apply (simp add: cap_async_endpoint_cap_lift [THEN iffD1])
apply (clarsimp simp: cap_to_H_def)
apply (simp add: map_option_case split: option.splits)
apply (clarsimp simp add: cap_to_H_def Let_def
split: cap_CL.splits split_if_asm)
apply (simp add: cap_async_endpoint_cap_lift_def)
apply (simp add: ccap_rights_relation_def cap_rights_to_H_def
to_bool_aep_cap_bf
to_bool_mask_to_bool_bf to_bool_cap_rights_bf)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: cap_get_tag_isCap isCap_simps return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply (simp add: cap_get_tag_isCap isCap_simps return_def)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply (rule imp_ignore)
apply clarsimp
apply (unfold ccap_relation_def)[1]
apply (simp add: cap_endpoint_cap_lift [THEN iffD1])
apply (clarsimp simp: cap_to_H_def)
apply (simp add: map_option_case split: option.splits)
apply (clarsimp simp add: cap_to_H_def Let_def
split: cap_CL.splits split_if_asm)
apply (simp add: cap_endpoint_cap_lift_def)
apply (simp add: ccap_rights_relation_def cap_rights_to_H_def
to_bool_ep_cap_bf
to_bool_mask_to_bool_bf to_bool_cap_rights_bf)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: cap_get_tag_isCap isCap_simps return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply (subst bind_return [symmetric])
apply (rule ccorres_split_throws)
apply ctac
apply (rule_tac P=\<top> and P'="\<lbrace>\<acute>ret__struct_cap_C = ret__struct_cap_C\<rbrace>" in ccorres_inst)
apply (rule ccorres_from_vcg_throws)
apply (clarsimp simp: return_def)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply wp
apply vcg
apply vcg
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply (simp add: cap_get_tag_isCap isCap_simps return_def)
apply (simp add: Collect_const_mem from_bool_def)
apply csymbr
apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: return_def)
apply clarsimp
done
abbreviation
"lookupCap_xf \<equiv> liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_'"
lemma ccorres_return_cte_cteCap [corres]:
fixes ptr' :: "cstate \<Rightarrow> cte_C ptr"
assumes r1: "\<And>s s' g. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu g s') \<in> rf_sr"
and xf_xfu: "\<And>s g. xf (xfu g s) = g s"
shows "ccorres ccap_relation xf
(\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs
(return (cteCap cte))
(Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s)))
(Ptr &(ptr' s \<rightarrow>[''cap_C'']))) s))"
apply (rule ccorres_return)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: xf_xfu ccap_relation_def)
apply rule
apply (erule r1)
apply (drule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp: typ_heap_simps)
apply (simp add: c_valid_cte_def)
done
lemma ccorres_return_cte_mdbnode [corres]:
fixes ptr' :: "cstate \<Rightarrow> cte_C ptr"
assumes r1: "\<And>s s' g. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu g s') \<in> rf_sr"
and xf_xfu: "\<And>s g. xf (xfu g s) = g s"
shows "ccorres cmdbnode_relation xf
(\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs
(return (cteMDBNode cte))
(Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s)))
(Ptr &(ptr' s \<rightarrow>[''cteMDBNode_C'']))) s))"
apply (rule ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp add: return_def xf_xfu)
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp: typ_heap_simps)
apply (erule r1)
done
(* FIXME: MOVE *)
lemma heap_update_field_ext:
"\<lbrakk>field_ti TYPE('a :: packed_type) f = Some t; c_guard p;
export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))\<rbrakk>
\<Longrightarrow> heap_update (Ptr &(p\<rightarrow>f) :: 'b ptr) =
(\<lambda>v hp. heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp)"
apply (rule ext, rule ext)
apply (erule (2) heap_update_field)
done
lemma ccorres_updateCap [corres]:
fixes ptr :: "cstate \<Rightarrow> cte_C ptr" and val :: "cstate \<Rightarrow> cap_C"
shows "ccorres dc xfdc \<top>
({s. ccap_relation cap (val s)} \<inter> {s. ptr s = Ptr dest}) hs
(updateCap dest cap)
(Basic
(\<lambda>s. globals_update
(t_hrs_'_update
(hrs_mem_update (heap_update (Ptr &(ptr s\<rightarrow>[''cap_C''])) (val s)))) s))"
unfolding updateCap_def
apply (cinitlift ptr)
apply (erule ssubst)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE)
apply (rule_tac P = "\<lambda>s. ctes_of s dest = Some rva" in
ccorres_from_vcg [where P' = "{s. ccap_relation cap (val s)}"])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption)
apply (erule bexI [rotated])
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp add: rf_sr_def cstate_relation_def
Let_def cpspace_relation_def)
apply (simp add:typ_heap_simps)
apply (rule conjI)
apply (erule (3) cpspace_cte_relation_upd_capI)
apply (erule_tac t = s' in ssubst)
apply (simp add: heap_to_page_data_def)
apply (rule conjI)
apply (erule (1) setCTE_tcb_case)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps)
apply clarsimp
done
lemma ccorres_updateMDB_const [corres]:
fixes ptr :: "cstate \<Rightarrow> cte_C ptr" and val :: "cstate \<Rightarrow> mdb_node_C"
shows "ccorres dc xfdc (\<lambda>_. dest \<noteq> 0)
({s. cmdbnode_relation m (val s)} \<inter> {s. ptr s = Ptr dest}) hs
(updateMDB dest (const m))
(Basic
(\<lambda>s. globals_update
(t_hrs_'_update
(hrs_mem_update (heap_update (Ptr &(ptr s\<rightarrow>[''cteMDBNode_C''])) (val s)))) s))"
unfolding updateMDB_def
apply (cinitlift ptr)
apply (erule ssubst)
apply (rule ccorres_gen_asm [where G = \<top>, simplified])
apply (simp only: Let_def)
apply simp
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE)
apply (rule_tac P = "\<lambda>s. ctes_of s dest = Some cte" in ccorres_from_vcg [where P' = "{s. cmdbnode_relation m (val s)}"])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption )
apply (erule bexI [rotated])
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps
Let_def cpspace_relation_def)
apply (rule conjI)
apply (erule (3) cspace_cte_relation_upd_mdbI)
apply (erule_tac t = s' in ssubst)
apply (simp add: heap_to_page_data_def)
apply (rule conjI)
apply (erule (1) setCTE_tcb_case)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps)
apply (clarsimp)
done
lemma cap_lift_capAEPBadge_mask_eq:
"cap_lift cap = Some (Cap_async_endpoint_cap ec)
\<Longrightarrow> capAEPBadge_CL ec && mask 28 = capAEPBadge_CL ec"
unfolding cap_lift_def
by (fastforce simp: Let_def mask_def word_bw_assocs split: split_if_asm)
lemma cap_lift_capEPBadge_mask_eq:
"cap_lift cap = Some (Cap_endpoint_cap ec)
\<Longrightarrow> capEPBadge_CL ec && mask 28 = capEPBadge_CL ec"
unfolding cap_lift_def
by (fastforce simp: Let_def mask_def word_bw_assocs split: split_if_asm)
lemma revokable_ccorres:
"\<lbrakk>ccap_relation cap newCap; cmdbnode_relation rva srcMDB;
ccap_relation rvb srcCap; ret__unsigned_long = cap_get_tag newCap \<rbrakk> \<Longrightarrow>
ccorres (\<lambda>a c. from_bool a = c) newCapIsRevocable_'
(\<lambda>_. capMasterCap cap = capMasterCap rvb \<or> is_simple_cap' cap) UNIV hs
(return (revokable' rvb cap))
(IF ret__unsigned_long = scast cap_endpoint_cap THEN
\<acute>ret__unsigned_long :== CALL cap_endpoint_cap_get_capEPBadge(newCap);;
\<acute>unsigned_long_eret_2 :== CALL cap_endpoint_cap_get_capEPBadge(srcCap);;
\<acute>newCapIsRevocable :==
(if \<acute>ret__unsigned_long \<noteq> \<acute>unsigned_long_eret_2 then 1
else 0)
ELSE
IF ret__unsigned_long = scast cap_async_endpoint_cap THEN
\<acute>ret__unsigned_long :== CALL cap_async_endpoint_cap_get_capAEPBadge(newCap);;
\<acute>unsigned_long_eret_2 :== CALL cap_async_endpoint_cap_get_capAEPBadge(srcCap);;
\<acute>newCapIsRevocable :==
(if \<acute>ret__unsigned_long \<noteq> \<acute>unsigned_long_eret_2 then 1
else 0)
ELSE
IF ret__unsigned_long = scast cap_irq_handler_cap THEN
\<acute>ret__unsigned_long :== CALL cap_get_capType(srcCap);;
\<acute>newCapIsRevocable :==
(if \<acute>ret__unsigned_long = scast cap_irq_control_cap then 1
else 0)
ELSE
IF ret__unsigned_long = scast cap_untyped_cap THEN
\<acute>newCapIsRevocable :== scast true
ELSE
IF True THEN
\<acute>newCapIsRevocable :== scast false
FI
FI
FI
FI
FI)"
unfolding revokable'_fold
apply (rule ccorres_gen_asm [where G = \<top>, simplified])
apply (cases cap)
apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def,
rule ccorres_return, vcg, fastforce simp: cap_get_tag_isCap isCap_simps)
apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def,
rule ccorres_return, vcg, fastforce simp: cap_get_tag_isCap isCap_simps)
apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def)
apply (rule ccorres_return, vcg)
apply (frule cap_get_tag_AsyncEndpointCap [where cap' = srcCap, THEN iffD1])
apply (clarsimp simp: cap_get_tag_isCap isCap_simps is_simple_cap'_def)
apply (frule cap_get_tag_AsyncEndpointCap [where cap' = newCap, THEN iffD1])
apply (clarsimp simp: cap_get_tag_isCap isCap_simps)
apply (fastforce simp: cap_get_tag_isCap isCap_simps)
apply (clarsimp simp: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def,
rule ccorres_return, vcg, fastforce simp: cap_get_tag_isCap isCap_simps)
apply (clarsimp simp: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def)
apply (rule ccorres_return, vcg)
apply (frule cap_get_tag_EndpointCap [where cap' = srcCap, THEN iffD1])
apply (clarsimp simp: cap_get_tag_isCap isCap_simps is_simple_cap'_def)
apply (frule cap_get_tag_EndpointCap [where cap' = newCap, THEN iffD1])
apply (clarsimp simp: cap_get_tag_isCap isCap_simps is_simple_cap'_def)
apply (fastforce simp: cap_get_tag_isCap isCap_simps)
apply (clarsimp simp: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def,
rule ccorres_return, vcg, fastforce simp: cap_get_tag_isCap isCap_simps)+
done
lemma from_bool_mask_simp [simp]:
"((from_bool r) :: word32) && mask (Suc 0) = from_bool r"
unfolding from_bool_def
apply (rule less_mask_eq)
apply (clarsimp split: bool.splits)
done
lemma cteInsert_ccorres_mdb_helper:
"\<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = (newCapIsRevocable :: word32); srcSlot = Ptr src\<rbrakk>
\<Longrightarrow> ccorres cmdbnode_relation newMDB_' (K (is_aligned src 3))
UNIV hs
(return
(mdbFirstBadged_update (\<lambda>_. rvc)
(mdbRevocable_update (\<lambda>_. rvc)
(mdbPrev_update (\<lambda>_. src) rva))))
(\<acute>newMDB :== CALL mdb_node_set_mdbPrev(srcMDB,
ptr_val srcSlot);;
\<acute>newMDB :== CALL mdb_node_set_mdbRevocable(\<acute>newMDB,
newCapIsRevocable);;
\<acute>newMDB :== CALL mdb_node_set_mdbFirstBadged(\<acute>newMDB,
newCapIsRevocable))"
apply (rule ccorres_from_vcg)
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: return_def)
apply (simp add: cmdbnode_relation_def)
done
lemma ccorres_updateMDB_set_mdbNext [corres]:
"src=src' \<Longrightarrow>
ccorres dc xfdc ((\<lambda>_. src \<noteq> 0 \<and> (dest\<noteq>0 \<longrightarrow> is_aligned dest 3)))
({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])} \<inter>
{s. v_' s = dest}) []
(updateMDB src (mdbNext_update (\<lambda>_. dest)))
(Call mdb_node_ptr_set_mdbNext_'proc)"
unfolding updateMDB_def
apply (hypsubst)
apply (rule ccorres_gen_asm [where G = \<top>, simplified])
apply (simp only: Let_def)
apply simp
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE [where P = "\<lambda>cte s. ctes_of s src' = Some cte" and
P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v = dest\<rbrace>)"])
apply (rule ccorres_from_spec_modifies_heap)
apply (rule mdb_node_ptr_set_mdbNext_spec)
apply (rule mdb_node_ptr_set_mdbNext_modifies)
apply simp
apply clarsimp
apply (rule rf_sr_cte_at_valid)
apply simp
apply (erule ctes_of_cte_at)
apply assumption
apply clarsimp
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp: typ_heap_simps)
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption)
apply (erule bexI [rotated])
apply (clarsimp simp add: rf_sr_def cstate_relation_def
Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_page_data_def)
apply (rule conjI)
apply (erule (2) cspace_cte_relation_upd_mdbI)
apply (simp add: cmdbnode_relation_def)
apply (case_tac "v_' s' = 0", simp+)[1]
apply (erule_tac t = s'a in ssubst)
apply simp
apply (rule conjI)
apply (erule (1) setCTE_tcb_case)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps h_t_valid_clift_Some_iff)
apply clarsimp
done
lemma ccorres_updateMDB_set_mdbPrev [corres]:
"src=src' \<Longrightarrow>
ccorres dc xfdc ((\<lambda>_. src \<noteq> 0 \<and> (dest\<noteq>0 \<longrightarrow>is_aligned dest 3)) )
({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])} \<inter>
{s. v_' s = dest}) []
(updateMDB src (mdbPrev_update (\<lambda>_. dest)))
(Call mdb_node_ptr_set_mdbPrev_'proc)"
unfolding updateMDB_def
apply (hypsubst)
apply (rule ccorres_gen_asm [where G = \<top>, simplified])
apply (simp only: Let_def)
apply simp
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE [where P = "\<lambda>cte s. ctes_of s src' = Some cte" and
P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v = dest\<rbrace>)"])
apply (rule ccorres_from_spec_modifies_heap)
apply (rule mdb_node_ptr_set_mdbPrev_spec)
apply (rule mdb_node_ptr_set_mdbPrev_modifies)
apply simp
apply clarsimp
apply (rule rf_sr_cte_at_valid)
apply simp
apply (erule ctes_of_cte_at)
apply assumption
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp: typ_heap_simps)
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption)
apply (erule bexI [rotated])
apply (clarsimp simp add: rf_sr_def cstate_relation_def
Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_page_data_def)
apply (rule conjI)
apply (erule (2) cspace_cte_relation_upd_mdbI)
apply (simp add: cmdbnode_relation_def)
apply (case_tac "v_' s' = 0", simp+)[1]
apply (erule_tac t = s'a in ssubst)
apply (simp add: carch_state_relation_def cmachine_state_relation_def h_t_valid_clift_Some_iff)
apply (erule (1) setCTE_tcb_case)
apply clarsimp
done
lemma ccorres_updateMDB_skip:
"ccorres dc xfdc (\<top> and (\<lambda>_. n = 0)) UNIV hs (updateMDB n f) SKIP"
unfolding updateMDB_def
apply (rule ccorres_gen_asm)
apply simp
apply (rule ccorres_return)
apply simp
apply vcg
done
definition
"is_simple_cap_tag (tag :: word32) \<equiv>
tag \<noteq> scast cap_null_cap \<and> tag \<noteq> scast cap_irq_control_cap
\<and> tag \<noteq> scast cap_untyped_cap \<and> tag \<noteq> scast cap_reply_cap
\<and> tag \<noteq> scast cap_endpoint_cap \<and> tag \<noteq> scast cap_async_endpoint_cap
\<and> tag \<noteq> scast cap_thread_cap \<and> tag \<noteq> scast cap_cnode_cap
\<and> tag \<noteq> scast cap_zombie_cap \<and> tag \<noteq> scast cap_small_frame_cap
\<and> tag \<noteq> scast cap_frame_cap"
definition
"cteInsert_newCapIsRevocable_if newCap srcCap \<equiv> (if (cap_get_tag newCap = scast cap_endpoint_cap)
then (if (capEPBadge_CL (cap_endpoint_cap_lift newCap) = capEPBadge_CL (cap_endpoint_cap_lift srcCap))
then 0 else 1)
else if (cap_get_tag newCap = scast cap_async_endpoint_cap)
then (if (capAEPBadge_CL (cap_async_endpoint_cap_lift newCap) = capAEPBadge_CL (cap_async_endpoint_cap_lift srcCap))
then 0 else 1)
else if (cap_get_tag newCap = scast cap_irq_handler_cap)
then (if cap_get_tag srcCap = scast cap_irq_control_cap then 1 else 0)
else if (cap_get_tag newCap = scast cap_untyped_cap) then 1 else 0)"
lemma cteInsert_if_helper:
assumes cgt: "rv = cap_get_tag newCap"
and rul: "\<And>s g. (s \<in> Q) = (s\<lparr> ret__unsigned_long_' := undefined,
unsigned_long_eret_2_':= undefined \<rparr> \<in> Q')"
shows "\<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s. (cap_get_tag srcCap = cap_get_tag newCap
\<or> is_simple_cap_tag (cap_get_tag newCap)) \<and>
(s\<lparr>newCapIsRevocable_' := cteInsert_newCapIsRevocable_if newCap srcCap\<rparr> \<in> Q)}
(IF rv = scast cap_endpoint_cap THEN
\<acute>ret__unsigned_long :== CALL cap_endpoint_cap_get_capEPBadge(newCap);;
\<acute>unsigned_long_eret_2 :== CALL cap_endpoint_cap_get_capEPBadge(srcCap);;
\<acute>newCapIsRevocable :== (if \<acute>ret__unsigned_long \<noteq> \<acute>unsigned_long_eret_2 then 1 else 0)
ELSE
IF rv = scast cap_async_endpoint_cap THEN
\<acute>ret__unsigned_long :== CALL cap_async_endpoint_cap_get_capAEPBadge(newCap);;
\<acute>unsigned_long_eret_2 :== CALL cap_async_endpoint_cap_get_capAEPBadge(srcCap);;
\<acute>newCapIsRevocable :== (if \<acute>ret__unsigned_long \<noteq> \<acute>unsigned_long_eret_2 then 1 else 0)
ELSE
IF rv = scast cap_irq_handler_cap THEN
\<acute>ret__unsigned_long :== CALL cap_get_capType(srcCap);;
\<acute>newCapIsRevocable :== (if \<acute>ret__unsigned_long = scast cap_irq_control_cap then 1 else 0)
ELSE
IF rv = scast cap_untyped_cap THEN
\<acute>newCapIsRevocable :== scast true
ELSE
IF True THEN
\<acute>newCapIsRevocable :== scast false
FI
FI
FI
FI
FI) Q"
unfolding cteInsert_newCapIsRevocable_if_def
apply (unfold cgt)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp: true_def false_def
is_simple_cap_tag_def
cong: if_cong)
apply (simp add: cap_tag_defs)
apply (intro allI conjI impI)
apply (clarsimp simp: rul)+
done
lemma forget_Q':
"(x \<in> Q) = (y \<in> Q) \<Longrightarrow> (x \<in> Q) = (y \<in> Q)" .
lemmas cteInsert_if_helper' = cteInsert_if_helper [OF _ forget_Q']
(* Useful:
apply (tactic {* let val _ = reset CtacImpl.trace_ceqv; val _ = reset CtacImpl.trace_ctac in all_tac end; *})
*)
declare word_neq_0_conv [simp del]
schematic_lemma ccap_relation_tag_Master:
"\<And>ccap. \<lbrakk> ccap_relation cap ccap \<rbrakk>
\<Longrightarrow> cap_get_tag ccap =
case_capability ?a ?b ?c ?d ?e ?f ?g
(case_arch_capability ?aa ?ab
(\<lambda>ptr rghts sz data. if sz = ARMSmallPage
then scast cap_small_frame_cap else scast cap_frame_cap)
?ad ?ae) ?h ?i ?j ?k
(capMasterCap cap)"
by (fastforce simp: ccap_relation_def option_map_Some_eq2
Let_def cap_lift_def cap_to_H_def
split: split_if_asm)
lemma ccap_relation_is_derived_tag_equal:
"\<lbrakk> is_derived' cs p cap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \<rbrakk>
\<Longrightarrow> cap_get_tag ccap' = cap_get_tag ccap"
unfolding badge_derived'_def is_derived'_def
by (clarsimp simp: ccap_relation_tag_Master)
lemma ccap_relation_Master_tags_eq:
"\<lbrakk> capMasterCap cap = capMasterCap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \<rbrakk>
\<Longrightarrow> cap_get_tag ccap' = cap_get_tag ccap"
by (clarsimp simp: ccap_relation_tag_Master)
lemma is_simple_cap_get_tag_relation:
"ccap_relation cap ccap
\<Longrightarrow> is_simple_cap_tag (cap_get_tag ccap) = is_simple_cap' cap"
apply (simp add: is_simple_cap_tag_def is_simple_cap'_def
cap_get_tag_isCap)
apply (auto simp: isCap_simps)
done
lemma setUntypedCapAsFull_cte_at_wp [wp]:
"\<lbrace> cte_at' x \<rbrace> setUntypedCapAsFull rvb cap src \<lbrace> \<lambda>_. cte_at' x \<rbrace>"
apply (clarsimp simp: setUntypedCapAsFull_def)
apply wp
done
lemma setUntypedCapAsFull_cte_at_wp' [wp]:
"\<lbrace> cte_wp_at' (\<lambda>_. True) x \<rbrace> setUntypedCapAsFull rvb cap src \<lbrace> \<lambda>_. cte_wp_at' (\<lambda>_. True) x \<rbrace>"
apply (clarsimp simp: setUntypedCapAsFull_def)
apply wp
done
lemma valid_cap_untyped_inv:
"valid_cap' (UntypedCap r n f) s \<Longrightarrow> n \<ge> 4 \<and> is_aligned (of_nat f :: word32) 4 \<and> n \<le> 30 \<and> n < word_bits"
apply (clarsimp simp:valid_cap'_def capAligned_def)
done
lemma update_freeIndex:
"ccorres dc xfdc
(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = UntypedCap p sz i) srcSlot
and (\<lambda>_. is_aligned (of_nat i' :: word32) 4 \<and> i' \<le> 2 ^ sz))
(UNIV \<inter> {s. cap_ptr_' s = Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])} \<inter> {s. v_' s = (of_nat (i') :: word32)>> 4})
[] (updateCap srcSlot (UntypedCap p sz i'))
(Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)"
apply (rule ccorres_gen_asm)
apply (rule ccorres_guard_imp)
prefer 3
apply assumption
apply (rule_tac P = "sz \<le> 30" and G = "cte_wp_at' S srcSlot" for S in ccorres_gen_asm)
prefer 2
apply clarsimp
apply (rule conjI, assumption)
apply (clarsimp simp:cte_wp_at_ctes_of)
apply (case_tac cte,clarsimp)
apply (drule(1) ctes_of_valid_cap')
apply (simp add:valid_cap'_def)
apply clarify
proof -
assume ialign:"is_aligned (of_nat i' :: word32) 4"
assume szbound:"sz\<le> 30"
assume ibound:"i'\<le> 2^sz"
have [simp]:"\<And>x. (x::word32) && 0xFFFFFFE0 = x && ~~ mask 5"
by (simp add:mask_def)
have [simp]:"\<And>x. ((x::word32) && ~~ mask 5) && mask 5 = 0"
by (simp add:is_aligned_mask[THEN iffD1,OF is_aligned_neg_mask])
have [simp]:"(0x7FFFFFF::word32) = mask 27"
by (simp add:mask_def)
have [simp]:"\<And>(n::word32) m. (n && mask 5 || m && ~~ mask 5 >> 5) && mask 27 = (m >> 5) && mask 27"
apply (rule word_eqI)
apply (simp add:nth_shiftr)
apply (simp add:neg_mask_bang word_size)
done
have [simp]:"(((of_nat i')::word32) >> 4 << 5 >> 5) = (of_nat i' >> 4)"
using szbound
apply (subst shiftl_shiftr_id)
apply (simp add:word_bits_def)
apply (rule shiftr_less_t2n)
apply (rule word_of_nat_less)
apply (rule le_less_trans[OF ibound])
apply (subst unat_power_lower32[symmetric])
apply (simp add:word_bits_def)
apply (subst word_less_nat_alt[symmetric])
apply (rule le_less_trans)
apply (erule two_power_increasing)
apply (simp add:word_bits_def)
apply (simp add:word_bits_def)
apply simp
done
have ib':"unat ((of_nat i' >> 4 ::word32) && mask 27 << 4) = i'"
using ialign ibound szbound
apply (simp add:is_aligned_mask)
apply (rule of_nat_inj32[THEN iffD1])
apply (rule less_le_trans[OF unat_lt2p])
apply (simp add:word_bits_def)
apply (erule le_less_trans)
apply (rule power_strict_increasing)
apply (simp add:word_bits_def)
apply simp+
apply (subgoal_tac "((of_nat i')::word32) && ~~ mask 31 = 0")
apply (word_bitwise)
apply (simp add: nth_mask word_size)
apply (rule mask_out_eq_0)
apply (erule le_less_trans)
apply (rule power_strict_increasing)
apply simp
apply simp
apply (simp add:word_bits_def)
done
note option.case_cong_weak [cong]
show "ccorresG rf_sr \<Gamma> dc xfdc (cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap p sz i) srcSlot)
(UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v = (of_nat i' :: word32) >> 4\<rbrace>) []
(updateCap srcSlot (capability.UntypedCap p sz i')) (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)"
apply (cinit lift: cap_ptr_' v_')
apply (rule ccorres_pre_getCTE)
apply (rule_tac P = "\<lambda>s. ctes_of s srcSlot = Some rv \<and> (\<exists>i. cteCap rv = UntypedCap p sz i)" in
ccorres_from_vcg[where P' = UNIV])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply (clarsimp simp:guard_simps)
apply (intro conjI)
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp:typ_heap_simps)
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp:split_def)
apply (simp add:hrs_htd_def typ_heap_simps)
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption)
apply (erule bexI [rotated])
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def)
apply (simp add:cpspace_relation_def)
apply (clarsimp simp:typ_heap_simps')
apply (rule conjI)
apply (erule(2) cpspace_cte_relation_upd_capI)
apply (simp add:cte_lift_def)
apply (simp split:option.splits )
apply (simp add:cap_to_H_def Let_def split:cap_CL.splits split_if_asm)
apply (case_tac y)
apply (simp add:cap_lift_def Let_def split:split_if_asm)
apply (case_tac cte',simp)
apply (clarsimp simp:ccap_relation_def cap_lift_def
cap_get_tag_def cap_to_H_def)
apply (simp add:mask_def[where n = 5,simplified,symmetric]
word_bool_alg.conj_disj_distrib2 mask_twice)
apply (simp add:ib')
apply (erule_tac t = s' in ssubst)
apply clarsimp
apply (rule conjI)
apply (erule (1) setCTE_tcb_case)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps')
apply (clarsimp simp:cte_wp_at_ctes_of)
done
qed
(* FIXME: move *)
lemma ccorres_cases:
assumes P: " P \<Longrightarrow> ccorres r xf G G' hs a b"
assumes notP: "\<not>P \<Longrightarrow> ccorres r xf H H' hs a b"
shows "ccorres r xf (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not>P \<longrightarrow> H s))
({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not>P \<longrightarrow> s \<in> H'})
hs a b"
apply (cases P, auto simp: P notP)
done
(* FIXME: move *)
lemma word_and_le': "\<lbrakk> b \<le> c \<rbrakk> \<Longrightarrow> (a :: word32) && b \<le> c"
apply (metis word_and_le1 order_trans)
done
(* FIXME: move *)
lemma word_and_less': "\<lbrakk> b < c \<rbrakk> \<Longrightarrow> (a :: word32) && b < c"
apply (metis word_and_le1 xtr7)
done
lemma capBlockSize_CL_maxSize:
" \<lbrakk> cap_get_tag c = scast cap_untyped_cap \<rbrakk> \<Longrightarrow> capBlockSize_CL (cap_untyped_cap_lift c) < 0x20"
apply (clarsimp simp: cap_untyped_cap_lift_def)
apply (clarsimp simp: cap_lift_def)
apply (clarsimp simp: cap_untyped_cap_def cap_null_cap_def)
apply (rule word_and_less')
apply simp
done
lemma t2p_shiftr:
"\<lbrakk>b\<le> a;a < word_bits \<rbrakk> \<Longrightarrow> (2\<Colon>word32) ^ a >> b = 2 ^ (a - b)"
apply (subst shiftr_w2p)
apply (simp add:word_bits_def)
apply (subst shiftr_w2p[where x = "a - b"])
apply (simp add:word_bits_def)
apply (simp only:word_bits_def[symmetric])
apply (simp add:shiftr_shiftr)
done
lemma setUntypedCapAsFull_ccorres [corres]:
notes split_if [split del]
notes Collect_const [simp del]