-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathInvoke_C.thy
3037 lines (2915 loc) · 157 KB
/
Invoke_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 Invoke_C
imports Recycle_C "../../lib/clib/MonadicRewrite_C"
begin
context kernel_m
begin
(************************************************************************)
(* *)
(* decodeDomainInvocation **********************************************)
(* *)
(************************************************************************)
lemma slotcap_in_mem_ThreadCap:
"\<lbrakk> slotcap_in_mem cap slot (ctes_of s); (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v
\<and> (cap_get_tag (cte_C.cap_C v) = scast cap_thread_cap)
= (isThreadCap cap)
\<and> (isThreadCap cap
\<longrightarrow> ccap_relation cap (cte_C.cap_C v))"
apply (clarsimp simp: slotcap_in_mem_def)
apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
apply (clarsimp dest!: ccte_relation_ccap_relation)
apply (simp add: cap_get_tag_isCap)
done
lemma cap_case_ThreadCap2:
"(case cap of (ThreadCap ptr) \<Rightarrow> f ptr | _ \<Rightarrow> g)
= (if isThreadCap cap
then f (capTCBPtr cap)
else g)"
by (simp add: isCap_simps
split: capability.split)
lemma setDomain_ccorres:
"ccorres dc xfdc
(invs' and tcb_at' t and sch_act_simple
and (\<lambda>s. d \<le> maxDomain))
(UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. dom_' s = ucast d})
[] (setDomain t d) (Call setDomain_'proc)"
apply (rule ccorres_gen_asm)
apply (cinit lift: tptr_' dom_')
apply (rule ccorres_pre_getCurThread)
apply (ctac(no_vcg) add: tcbSchedDequeue_ccorres)
apply (rule ccorres_move_c_guard_tcb)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule threadSet_ccorres_lemma2[where P=\<top>])
apply vcg
apply clarsimp
apply (erule(1) rf_sr_tcb_update_no_queue2,
(simp add: typ_heap_simps)+, simp_all)[1]
apply (subst heap_update_field_hrs | fastforce intro: typ_heap_simps)+
apply (rule ball_tcb_cte_casesI, simp+)
apply (simp add: ctcb_relation_def)
apply (ctac(no_vcg) add: isRunnable_ccorres)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (simp add: when_def to_bool_def del: Collect_const)
apply (rule ccorres_cond2[where R=\<top>], simp add: Collect_const_mem)
apply (ctac add: tcbSchedEnqueue_ccorres)
apply (rule ccorres_return_Skip)
apply (simp add: when_def to_bool_def)
apply (rule_tac R="\<lambda>s. rv = ksCurThread s"
in ccorres_cond2)
apply (clarsimp simp: rf_sr_ksCurThread)
apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def])
apply (rule ccorres_return_Skip')
apply simp
apply (wp hoare_drop_imps weak_sch_act_wf_lift_linear)
apply (simp add: guard_is_UNIV_def)
apply simp
apply wp
apply (rule_tac Q="\<lambda>_. all_invs_but_sch_extra and tcb_at' t and sch_act_simple
and (\<lambda>s. rv = ksCurThread s)" in hoare_strengthen_post)
apply (wp_trace threadSet_all_invs_but_sch_extra)
apply (clarsimp simp:valid_pspace_valid_objs' st_tcb_at_def[symmetric]
sch_act_simple_def st_tcb_at'_def o_def weak_sch_act_wf_def split:if_splits)
apply (simp add: guard_is_UNIV_def)
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t and sch_act_simple
and (\<lambda>s. rv = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))" in hoare_strengthen_post)
apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_not_queued
tcbSchedDequeue_not_in_queue hoare_vcg_imp_lift hoare_vcg_all_lift)
apply (clarsimp simp:invs'_def valid_pspace'_def valid_state'_def)
apply (fastforce simp: valid_tcb'_def tcb_cte_cases_def
invs'_def valid_state'_def valid_pspace'_def)
done
lemma active_runnable':
"active' state \<Longrightarrow> runnable' state"
by (fastforce simp: runnable'_def)
lemma decodeDomainInvocation_ccorres:
notes Collect_const[simp del]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and (\<lambda>s. ksCurThread s = thread)
and sch_act_simple and ct_active'
and (excaps_in_mem extraCaps \<circ> ctes_of)
and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v).
ex_nonz_cap_to' y s)
and (\<lambda>s. \<forall>v \<in> set extraCaps.
s \<turnstile>' fst v)
and sysargs_rel args buffer)
(UNIV
\<inter> {s. unat (length_' s) = length args}
\<inter> {s. extraCaps_' s = extraCaps'}
\<inter> {s. call_' s = from_bool isCall}
\<inter> {s. label_' s = lab}
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
(decodeDomainInvocation lab args extraCaps
>>= invocationCatch thread isBlocking isCall (uncurry InvokeDomain))
(Call decodeDomainInvocation_'proc)"
apply (cinit' lift: length_' extraCaps_' call_' label_' buffer_'
simp: decodeDomainInvocation_def list_case_If2 whenE_def)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: throwError_bind invocationCatch_def invocation_eq_use_types
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: invocation_eq_use_types)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: throwError_bind invocationCatch_def
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: unat_gt_0[symmetric] del:)
apply (rule ccorres_add_return)
apply (rule ccorres_rhs_assoc)+
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer])
apply (simp add: numDomains_def hd_conv_nth word_le_nat_alt)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: throwError_bind invocationCatch_def numDomains_def
hd_conv_nth word_le_nat_alt
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: null_def excaps_map_def)
apply (rule ccorres_Guard_Seq)+
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: throwError_bind invocationCatch_def
interpret_excaps_test_null
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: interpret_excaps_test_null hd_conv_nth cap_case_ThreadCap2)
apply (rule ccorres_add_return)
apply (rule_tac r'="(\<lambda>rv _ rv'. ((cap_get_tag rv' = scast cap_thread_cap)
= (isThreadCap rv))
\<and> (cap_get_tag rv' = scast cap_thread_cap \<longrightarrow> ccap_relation rv rv'))
(fst (extraCaps ! 0))"
and xf'=tcap_' in ccorres_split_nothrow)
apply (rule ccorres_from_vcg[where P="excaps_in_mem extraCaps \<circ> ctes_of" and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: excaps_in_mem_def return_def neq_Nil_conv)
apply (drule(1) slotcap_in_mem_ThreadCap)
apply (frule interpret_excaps_eq[rule_format, where n=0], simp)
apply (clarsimp simp: typ_heap_simps' mask_def word_sless_def word_sle_def)
apply ceqv
apply csymbr
apply clarsimp
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: Collect_const)
apply (simp add: throwError_bind invocationCatch_def
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: Collect_const returnOk_def uncurry_def)
apply (simp (no_asm) add: ccorres_invocationCatch_Inr split_def
performInvocation_def liftE_bindE bind_assoc)
apply (ctac add: setThreadState_ccorres)
apply csymbr
apply (ctac add: setDomain_ccorres)
apply (rule ccorres_alternative2)
apply (ctac add: ccorres_return_CE)
apply wp
apply (vcg exspec=setDomain_modifies)
apply (wp sts_invs_minor')
apply (vcg exspec=setThreadState_modifies)
apply wp
apply simp
apply clarsimp
apply vcg
apply wp
apply simp
apply clarsimp
apply (vcg exspec=getSyscallArg_modifies)
apply (clarsimp simp: valid_tcb_state'_def invs_valid_queues' invs_valid_objs'
invs_queues invs_sch_act_wf' ct_in_state'_def st_tcb_at_tcb_at'
rf_sr_ksCurThread word_sle_def word_sless_def sysargs_rel_to_n
mask_eq_iff_w2p mask_eq_iff_w2p word_size "StrictC'_thread_state_defs"
maxDomain_def numDomains_def)
apply (rule conjI)
apply (clarsimp simp: linorder_not_le isCap_simps)
apply (rule conjI, clarsimp simp: unat32_eq_of_nat)
apply clarsimp
apply (drule_tac x="extraCaps ! 0" and P="\<lambda>v. valid_cap' (fst v) s" in bspec)
apply (clarsimp simp: nth_mem interpret_excaps_test_null excaps_map_def)
apply (clarsimp simp: valid_cap_simps' st_tcb'_weakenE active_runnable')
apply (rule conjI)
apply (fastforce simp: tcb_st_refs_of'_def elim:st_tcb'_weakenE)
apply (simp add: word_le_nat_alt unat_ucast)
apply (clarsimp simp: ucast_ucast_len word_less_nat_alt
ccap_relation_def cap_to_H_simps cap_thread_cap_lift)
done
(************************************************************************)
(* *)
(* invokeCNodeDelete_ccorres ********************************************)
(* *)
(************************************************************************)
lemma invokeCNodeDelete_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(\<lambda>s. invs' s \<and> sch_act_simple s)
(UNIV \<inter> {s. destSlot_' s = Ptr destSlot}) []
(invokeCNode (Delete destSlot))
(Call invokeCNodeDelete_'proc)"
apply (cinit lift: destSlot_' simp del: return_bind cong:call_ignore_cong)
apply (rule ccorres_trim_returnE, simp, simp)
apply (rule ccorres_callE)
apply (rule cteDelete_ccorres[simplified])
apply (simp add: from_bool_def true_def)+
done
(************************************************************************)
(* *)
(* invokeCNodeRevoke_ccorres ********************************************)
(* *)
(************************************************************************)
lemma invokeCNodeRevoke_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and sch_act_simple)
(UNIV \<inter> {s. destSlot_' s = cte_Ptr destSlot}) []
(invokeCNode (Revoke destSlot))
(Call invokeCNodeRevoke_'proc)"
apply (cinit lift: destSlot_' simp del: return_bind cong:call_ignore_cong)
apply (rule ccorres_trim_returnE, simp, simp)
apply (rule ccorres_callE)
apply (rule cteRevoke_ccorres[simplified])
apply (simp add: from_bool_def true_def)+
done
(************************************************************************)
(* *)
(* invokeCNodeRecycle_ccorres ********************************************)
(* *)
(************************************************************************)
lemma invokeCNodeRecycle_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and sch_act_simple) (UNIV \<inter> {s. destSlot_' s = cte_Ptr destSlot}) []
(invokeCNode (Recycle destSlot))
(Call invokeCNodeRecycle_'proc)"
apply (cinit lift: destSlot_' simp del: return_bind cong:call_ignore_cong)
apply (rule ccorres_trim_returnE, simp, simp)
apply (rule ccorres_callE)
apply (rule cteRecycle_ccorres[simplified])
apply (simp add: from_bool_def true_def)+
done
(************************************************************************)
(* *)
(* invokeCNodeInsert_ccorres ********************************************)
(* *)
(************************************************************************)
lemma invokeCNodeInsert_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src
and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap)
(UNIV \<inter> {s. destSlot_' s = Ptr dest} \<inter>
{s. srcSlot_' s = Ptr src} \<inter>
{s. ccap_relation cap (cap_' s)}) []
(invokeCNode (Insert cap src dest))
(Call invokeCNodeInsert_'proc)"
apply (cinit lift: destSlot_' srcSlot_' cap_' simp del: return_bind cong:call_ignore_cong)
apply (simp add: liftE_def)
apply (ctac (no_vcg) add: cteInsert_ccorres)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre,vcg) apply clarsimp apply (simp add: return_def)
apply wp
apply (clarsimp simp: cte_wp_at_ctes_of)
done
(************************************************************************)
(* *)
(* invokeCNodeMove_ccorres *********************************************)
(* *)
(************************************************************************)
lemma invokeCNodeMove_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(valid_mdb' and pspace_aligned' )
(UNIV \<inter> {s. destSlot_' s = Ptr dest} \<inter>
{s. srcSlot_' s = Ptr src} \<inter>
{s. ccap_relation cap (cap_' s)}) []
(invokeCNode (Move cap src dest))
(Call invokeCNodeMove_'proc)"
apply (cinit lift: destSlot_' srcSlot_' cap_' simp del: return_bind cong:call_ignore_cong)
apply (simp add: liftE_def)
apply (ctac (no_vcg) add: cteMove_ccorres)
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre,vcg) apply clarsimp apply (simp add: return_def)
apply wp
apply clarsimp
done
(************************************************************************)
(* *)
(* invokeCNodeRotate_ccorres *******************************************)
(* *)
(************************************************************************)
lemma invokeCNodeRotate_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(\<lambda>s. cte_at' slot1 s \<and> cte_at' slot2 s \<and> slot1 \<noteq> slot2
\<and> valid_pspace' s \<and> valid_cap' cap2 s
\<and> cte_wp_at' (\<lambda>c. weak_derived' cap2 (cteCap c)) slot2 s
\<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> (cteCap c) = cap2) slot2 s
\<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> NullCap) slot2 s
\<and> (slot1 \<noteq> slot3 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot3 s))
(UNIV \<inter> {s. slot1_' s = Ptr slot1} \<inter>
{s. slot2_' s = Ptr slot2} \<inter>
{s. slot3_' s = Ptr slot3} \<inter>
{s. ccap_relation cap1 (cap1_' s)} \<inter>
{s. ccap_relation cap2 (cap2_' s)}) []
(invokeCNode (Rotate cap1 cap2 slot1 slot2 slot3))
(Call invokeCNodeRotate_'proc)"
apply (cinit lift: slot1_' slot2_' slot3_' cap1_' cap2_' simp del: return_bind cong:call_ignore_cong)
apply (simp split del: split_if del: Collect_const)
apply (simp only: liftE_def)
apply (rule_tac r'="dc" and xf'="xfdc" in ccorres_split_nothrow_novcg)
apply (rule ccorres_cond [where R = \<top>])
apply (clarsimp simp: Collect_const_mem)
apply (ctac (no_vcg) add: cteSwap_ccorres)
apply (ctac (no_vcg) add: cteMove_ccorres)
apply (simp only: K_bind_def)
apply (ctac (no_vcg) add: cteMove_ccorres)
apply (rule hoare_strengthen_post)
apply (rule cteMove_valid_pspace')
apply (simp add: valid_pspace'_def)
apply ceqv
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre,vcg)
apply clarsimp
apply (simp add: return_def)
apply wp
apply (simp add: guard_is_UNIV_def dc_def xfdc_def)
apply (clarsimp simp: valid_pspace'_def)
apply (rule conjI, clarsimp)
apply (clarsimp simp:cte_wp_at_ctes_of)
apply (clarsimp simp: weak_derived'_def isCap_simps)
done
(************************************************************************)
(* *)
(* invokeCNodeSaveCaller ***********************************************)
(* *)
(************************************************************************)
lemma invokeCNodeSaveCaller_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(valid_mdb' and pspace_aligned' and cur_tcb')
(UNIV \<inter> {s. destSlot_' s = Ptr destSlot}) []
(invokeCNode (SaveCaller destSlot))
(Call invokeCNodeSaveCaller_'proc)"
apply (cinit lift: destSlot_' simp del: return_bind cong:call_ignore_cong)
apply (simp split del: split_if del: Collect_const cong:call_ignore_cong)
apply (simp only: liftE_def)
apply (rule ccorres_Guard_Seq)+
apply (simp only: bind_assoc)
apply (rule ccorres_pre_getCurThread)
apply (simp only: getThreadCallerSlot_def locateSlot_conv)
apply (rule_tac P="\<lambda>s. rv=ksCurThread s \<and> is_aligned rv 9" and r'="\<lambda> a c. c = Ptr a"
and xf'="srcSlot_'" and P'=UNIV in ccorres_split_nothrow)
apply (rule ccorres_return)
apply vcg
apply clarsimp
apply (simp add: cte_level_bits_def size_of_def of_nat_def)
apply (simp add: rf_sr_def cstate_relation_def Kernel_C.tcbCaller_def tcbCallerSlot_def)
apply (clarsimp simp: Let_def)
apply (subst ptr_val_tcb_ptr_mask2 [simplified mask_def, simplified])
apply assumption
apply simp
apply ceqv
apply (simp del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_getSlotCap_cte_at)
apply (rule ccorres_move_c_guard_cte)
apply (ctac (no_vcg))
apply csymbr
apply (wpc, simp_all add: cap_get_tag_isCap isCap_simps
Collect_False Collect_True
del: Collect_const)[1]
apply (rule ccorres_fail)+
-- "NullCap case"
apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (simp add: return_def)
apply (rule ccorres_fail)+
-- "ReplyCap case"
apply (rule ccorres_rhs_assoc)
apply csymbr
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (simp add: cap_get_tag_ReplyCap)
apply (case_tac " (capReplyMaster_CL (cap_reply_cap_lift cap))=0", simp_all add: to_bool_def)[1]
apply (ctac (no_vcg) add: cteMove_ccorres)
apply (rule ccorres_return_CE [unfolded returnOk_def,simplified], simp+)[1]
apply wp
apply (rule ccorres_fail')
apply (rule ccorres_fail)+
apply (wp getSlotCap_wp)
apply (clarsimp simp: cap_get_tag_isCap isCap_simps)
apply wp
apply vcg
apply (clarsimp simp: word_sle_def cte_wp_at_ctes_of
tcb_aligned' cur_tcb'_def)
done
(************************************************************************)
(* *)
(* decodeCNodeInvocation ***********************************************)
(* *)
(************************************************************************)
lemma ccorres_basic_srnoop2:
"\<lbrakk> \<And>s. globals (g s) = globals s;
ccorres_underlying rf_sr Gamm r xf arrel axf G (g ` G') hs a c \<rbrakk>
\<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf G G'
hs a (Basic g ;; c)"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_symb_exec_r)
apply assumption
apply vcg
apply (rule conseqPre, vcg)
apply clarsimp
apply simp
done
lemma updateCapData_spec2:
"\<forall>cap preserve newData. \<Gamma> \<turnstile> \<lbrace> ccap_relation cap \<acute>cap \<and> preserve = to_bool (\<acute>preserve) \<and> newData = \<acute>newData\<rbrace>
Call updateCapData_'proc
\<lbrace> ccap_relation (updateCapData preserve newData cap) \<acute>ret__struct_cap_C \<rbrace>"
by (simp add: updateCapData_spec)
lemma mdbRevocable_CL_cte_to_H:
"(mdbRevocable_CL (cteMDBNode_CL clcte) = 0)
= (\<not> mdbRevocable (cteMDBNode (cte_to_H clcte)))"
by (simp add: cte_to_H_def mdb_node_to_H_def to_bool_def)
lemma ccorres_add_specific_return:
"ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs
(do v \<leftarrow> return val; f v od) c
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (f val) c"
by simp
(* FIXME: also in Tcb_C *)
lemma ccorres_subgoal_tailE:
"\<lbrakk> ccorres rvr xf Q Q' hs (b ()) d;
ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d) \<rbrakk>
\<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)"
by simp
lemma label_in_CNodeInv_ranges:
"(label < scast Kernel_C.CNodeRevoke \<or> scast Kernel_C.CNodeSaveCaller < label)
= (invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
"(scast Kernel_C.CNodeCopy \<le> label \<and> label \<le> scast Kernel_C.CNodeMutate)
= (invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])"
apply (simp_all add: upto_enum_def fromEnum_def enum_invocation_label
del: upt.simps)
apply (simp_all add: atLeastLessThanSuc)
apply (simp_all add: toEnum_def enum_invocation_label)
apply (simp_all add: invocation_eq_use_types[symmetric] invocation_label_defs)
apply (simp_all add: unat_arith_simps)
apply arith+
done
lemma cnode_invok_case_cleanup2:
"i \<in> set [CNodeCopy .e. CNodeMutate] \<Longrightarrow>
(case i of CNodeRevoke \<Rightarrow> P | CNodeDelete \<Rightarrow> Q | CNodeRecycle \<Rightarrow> R
| CNodeRotate \<Rightarrow> S | CNodeSaveCaller \<Rightarrow> T | _ \<Rightarrow> U) = U"
apply (rule cnode_invok_case_cleanup)
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
apply auto
done
lemma Arch_hasRecycleRights_spec:
"\<forall>cap. \<Gamma> \<turnstile> \<lbrace> ccap_relation (ArchObjectCap cap) \<acute>cap \<rbrace>
Call Arch_hasRecycleRights_'proc
\<lbrace> \<acute>ret__unsigned_long = from_bool (ArchRetypeDecls_H.hasRecycleRights cap) \<rbrace>"
apply vcg
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (frule cap_get_tag_PageCap_frame [THEN iffD1], assumption)
apply clarsimp
apply (drule ccap_relation_PageCap_generics)
apply (auto simp: ArchRetype_H.hasRecycleRights_def
vmrights_to_H_def true_def false_def
vmrights_defs
dest: less_4_cases
split: if_splits)[1]
apply (rule conjI)
apply clarsimp
apply (frule cap_get_tag_PageCap_small_frame [THEN iffD1], assumption)
apply clarsimp
apply (drule ccap_relation_PageCap_generics)
apply (auto simp: ArchRetype_H.hasRecycleRights_def
vmrights_to_H_def true_def false_def
vmrights_defs
dest: less_4_cases
split: if_splits)[1]
apply (case_tac cap,
auto simp: ArchRetype_H.hasRecycleRights_def
dest: ccap_relation_frame_tags)[1]
done
lemma hasRecycleRights_spec:
"\<forall>cap. \<Gamma> \<turnstile> \<lbrace> ccap_relation cap \<acute>cap \<rbrace>
Call hasRecycleRights_'proc
\<lbrace> \<acute>ret__unsigned_long = from_bool (hasRecycleRights cap) \<rbrace>"
apply vcg
apply (clarsimp simp: if_1_0_0)
apply (rule conjI)
-- "DomainCap"
apply clarsimp
apply (drule (1) cap_get_tag_to_H)
apply (clarsimp simp: hasRecycleRights_def)
apply (rule conjI)
-- "NullCap"
apply clarsimp
apply (drule cap_get_tag_to_H, simp)
apply (clarsimp simp: hasRecycleRights_def)
apply (rule impI)
apply (rule conjI)
-- "EP"
apply clarsimp
apply (drule sym, drule (1) cap_get_tag_to_H)
apply (clarsimp simp: hasRecycleRights_def to_bool_def
true_def false_def
split: split_if bool.splits)
apply (rule impI)
apply (rule conjI)
-- "AEP"
apply clarsimp
apply (drule sym, drule (1) cap_get_tag_to_H)
apply (clarsimp simp: hasRecycleRights_def to_bool_def
true_def false_def
split: split_if bool.splits)
apply (rule impI)
apply (rule conjI)
-- "Arch"
apply (clarsimp simp: from_bool_neq_0)
apply (frule (1) cap_get_tag_isCap_ArchObject2_worker [rotated])
apply (rule refl)
apply (clarsimp simp: isCap_simps hasRecycleRights_def)
apply fastforce
-- "rest"
apply (case_tac cap,
auto simp: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs
from_bool_def false_def true_def hasRecycleRights_def
dest: cap_get_tag_isArchCap_unfolded_H_cap
split: capability.splits bool.splits)[1]
done
lemma updateCapData_Untyped:
"isUntypedCap a
\<Longrightarrow> updateCapData b c a = a"
by (clarsimp simp:isCap_simps updateCapData_def)
lemma ctes_of_valid_strengthen:
"(invs' s \<and> ctes_of s p = Some cte) \<longrightarrow> valid_cap' (cteCap cte) s"
apply (case_tac cte)
apply clarsimp
apply (erule ctes_of_valid_cap')
apply fastforce
done
lemma decodeCNodeInvocation_ccorres:
notes tl_drop_1[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and (\<lambda>s. ksCurThread s = thread)
and sch_act_simple and ct_active'
and valid_cap' cp
and (excaps_in_mem extraCaps \<circ> ctes_of)
and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v).
ex_nonz_cap_to' y s)
and (\<lambda>s. \<forall>v \<in> set extraCaps.
s \<turnstile>' fst v)
and sysargs_rel args buffer)
(UNIV
\<inter> {s. unat (length_' s) = length args}
\<inter> {s. ccap_relation cp (cap_' s)}
\<inter> {s. extraCaps_' s = extraCaps'}
\<inter> {s. call_' s = from_bool isCall}
\<inter> {s. label_' s = lab}
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
(decodeCNodeInvocation lab args cp (map fst extraCaps)
>>= invocationCatch thread isBlocking isCall InvokeCNode)
(Call decodeCNodeInvocation_'proc)"
apply (cases "\<not>isCNodeCap cp")
apply (simp add: decodeCNodeInvocation_def
cong: conj_cong)
apply (rule ccorres_fail')
apply (cinit' (no_subst_asm) lift: length_' cap_' extraCaps_'
call_' label_' buffer_')
apply (clarsimp simp: word_less_nat_alt decodeCNodeInvocation_def
list_case_If2 invocation_eq_use_types
label_in_CNodeInv_ranges[unfolded word_less_nat_alt]
cnode_invok_case_cleanup2
simp del: Collect_const
cong: call_ignore_cong globals.fold_congs
StateSpace.state.fold_congs bool.case_cong
cong del: invocation_label.weak_case_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: unlessE_def throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: length_ineq_not_Nil unlessE_whenE
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer])
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=1 and buffer=buffer])
apply (simp add: split_def Let_def invocationCatch_use_injection_handler
injection_bindE [OF refl refl] bindE_assoc
del: Collect_const)
(* sigh \<dots> just going to blog this here. i can't use call_ignore_cong
because we need to rewrite within at least one argument in order to
match the rewrite that's happened in the argument to ?R13918 and we
can't apply ctac below. but once we have simplified away
newData = newData below there's no way to get it back. sigh *)
apply (ctac add: ccorres_injection_handler_csum1
[OF lookupTargetSlot_ccorres,
unfolded lookupTargetSlot_def])
apply (simp add: Collect_False del: Collect_const
cong: call_ignore_cong)
apply csymbr
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: word_less_nat_alt
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_split_throws)
apply (rule ccorres_rhs_assoc | csymbr)+
apply (simp add: invocationCatch_use_injection_handler
[symmetric, unfolded o_def]
if_1_0_0 dc_def[symmetric]
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add:if_P del: Collect_const)
apply (rule ccorres_cond_true_seq)
apply (simp add: throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: linorder_not_less del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_Guard_Seq)+
apply csymbr
apply (simp add: if_1_0_0 interpret_excaps_test_null
excaps_map_def
del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=2 and buffer=buffer])
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=3 and buffer=buffer])
apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0])
apply (rule ccorres_move_c_guard_cte)
apply ctac
apply (rule ccorres_assert2)
apply (simp add: split_def invocationCatch_use_injection_handler
injection_bindE [OF refl refl] bindE_assoc
injection_liftE [OF refl] if_not_P
cong: call_ignore_cong)
apply (ctac add: ccorres_injection_handler_csum1 [OF ensureEmptySlot_ccorres])
prefer 2
apply simp
apply (rule ccorres_split_throws)
apply simp
apply (rule ccorres_return_C_errorE, simp+)[1]
apply vcg
apply simp
apply (ctac add: ccorres_injection_handler_csum1
[OF lookupSourceSlot_ccorres,
unfolded lookupSourceSlot_def])
prefer 2
apply simp
apply (rule ccorres_split_throws)
apply simp
apply (rule ccorres_return_C_errorE, simp+)[1]
apply vcg
apply (simp add: liftE_bindE cong: call_ignore_cong)
apply csymbr
apply (rule ccorres_move_c_guard_cte)
apply (rule ccorres_pre_getCTE)
apply (rule ccorres_add_return)
apply (rule_tac xf'=ret__unsigned_long_'
and r'="\<lambda>_ rv'. (rv' = scast cap_null_cap)
= (cteCap rvb = NullCap)"
in ccorres_split_nothrow)
apply (rule_tac P'="{s. \<exists>v. cslift s (cte_Ptr rva) = Some v
\<and> ccte_relation rvb v}"
in ccorres_from_vcg[where P=\<top>])
apply (rule allI, rule conseqPre, vcg)
apply (rule subsetI, clarsimp simp: Collect_const_mem return_def)
apply (clarsimp dest!: ccte_relation_ccap_relation
simp: cap_get_tag_NullCap
typ_heap_simps)
apply ceqv
apply (simp del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: whenE_def injection_handler_throwError)
apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
apply vcg
apply (rule conseqPre, vcg)
apply (clarsimp simp: throwError_def return_def hd_conv_nth
syscall_error_rel_def exception_defs
syscall_error_to_H_cases numeral_eqs)
apply (clarsimp simp: lookup_fault_missing_capability_lift
mask_eq_iff_w2p word_size word_less_nat_alt
word_bits_def hd_conv_nth)
apply (simp add: whenE_def[where P=False]
injection_handler_returnOk Collect_const[symmetric]
cong: call_ignore_cong del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
-- "CNodeCopy case"
apply (simp add: Collect_const[symmetric] del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: injection_handler_throwError dc_def[symmetric]
if_P)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: list_case_helper injection_handler_returnOk
split_def hd_conv_nth numeral_eqs[symmetric]
if_not_P
del: Collect_const)
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=4 and buffer=buffer])
apply csymbr
apply (rule ccorres_move_c_guard_cte)
apply (simp add: split_def del: Collect_const)
apply (rule_tac val="maskCapRights (rightsFromWord (args ! 4)) (cteCap rvb)"
in ccorres_add_specific_return)
apply (ctac add: maskCapRights_ccorres)
apply (ctac add: ccorres_injection_handler_csum1 [OF deriveCap_ccorres])
prefer 2
apply simp
apply (rule ccorres_split_throws)
apply simp
apply (rule ccorres_return_C_errorE, simp+)[1]
apply vcg
apply simp
apply csymbr
apply csymbr
apply csymbr
apply (simp add: cap_get_tag_NullCap del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: injection_handler_throwError whenE_def
dc_def[symmetric])
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: whenE_def injection_handler_returnOk
ccorres_invocationCatch_Inr performInvocation_def
bindE_assoc false_def)
apply (ctac add: setThreadState_ccorres)
apply (simp add: ccorres_cond_iffs)
apply (ctac(no_vcg) add: invokeCNodeInsert_ccorres)
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (wp sts_valid_pspace_hangers)
apply (simp add: Collect_const_mem)
apply (vcg exspec=setThreadState_modifies)
apply simp
apply (wp injection_wp_E[OF refl])
apply (rule hoare_post_imp_R)
apply (rule_tac Q'="\<lambda>rv. valid_pspace' and valid_queues
and valid_cap' rv and valid_objs'
and tcb_at' thread and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)"
in hoare_vcg_R_conj)
apply (rule deriveCap_Null_helper[OF deriveCap_derived])
apply wp
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (simp add: is_derived'_def badge_derived'_def
valid_tcb_state'_def)
apply (simp add: Collect_const_mem all_ex_eq_helper)
apply (vcg exspec=deriveCap_modifies)
apply wp
apply (simp add: Collect_const_mem)
apply (vcg exspec=maskCapRights_modifies)
apply wp
apply (simp add: Collect_const_mem)
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_Cond_rhs_Seq)
-- "CNodeMint case"
apply (simp add: Collect_const[symmetric]
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule ccorres_Cond_rhs_Seq)
apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
apply vcg
apply (rule conseqPre, vcg)
apply (clarsimp split: split_if simp: injection_handler_throwError)
apply (auto simp: throwError_def return_def
syscall_error_to_H_cases syscall_error_rel_def
exception_defs)[1]
apply (simp add: list_case_helper injection_handler_returnOk
split_def linorder_not_less numeral_eqs[symmetric]
hd_conv_nth le_Suc_eq le_imp_diff_is_add if_not_P
del: Collect_const)
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=4 and buffer=buffer])
apply csymbr
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=5 and buffer=buffer])
apply (rule ccorres_move_c_guard_cte)
apply (simp del: Collect_const)
apply (rule_tac val="maskCapRights (rightsFromWord (args ! 4)) (cteCap rvb)"
in ccorres_add_specific_return)
apply (ctac add: maskCapRights_ccorres)
apply (rule ccorres_symb_exec_r)
apply (ctac add: ccorres_injection_handler_csum1 [OF deriveCap_ccorres])
prefer 2
apply simp
apply (rule ccorres_split_throws)
apply simp
apply (rule ccorres_return_C_errorE, simp+)[1]
apply vcg
apply simp
apply csymbr
apply csymbr
apply csymbr
apply (simp add: cap_get_tag_NullCap del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: whenE_def injection_handler_returnOk
invocationCatch_def injection_handler_throwError
dc_def[symmetric])
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: whenE_def injection_handler_returnOk
ccorres_invocationCatch_Inr false_def
performInvocation_def bindE_assoc)
apply (ctac add: setThreadState_ccorres)
apply (simp add: ccorres_cond_iffs)
apply (ctac(no_vcg) add: invokeCNodeInsert_ccorres)
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (wp sts_valid_pspace_hangers)
apply (simp add: Collect_const_mem)
apply (vcg exspec=setThreadState_modifies)
apply (simp add: conj_ac valid_tcb_state'_def)
apply (wp injection_wp_E[OF refl])
apply (rule hoare_post_imp_R)
apply (rule_tac Q'="\<lambda>rv. valid_pspace' and valid_queues
and valid_cap' rv and valid_objs'
and tcb_at' thread and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)"
in hoare_vcg_R_conj)
apply (rule deriveCap_Null_helper [OF deriveCap_derived])
apply wp
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (simp add: is_derived'_def badge_derived'_def)
apply (simp add: Collect_const_mem all_ex_eq_helper)
apply (vcg exspec=deriveCap_modifies)
apply (simp add: Collect_const_mem)
apply (vcg exspec=updateCapData_spec2)
apply (rule conseqPre, vcg exspec=updateCapData_spec2, clarsimp)
apply fastforce
apply simp
apply wp
apply (simp add: Collect_const_mem hd_drop_conv_nth)
apply (vcg exspec=maskCapRights_modifies)
apply simp
apply wp
apply (simp add: Collect_const_mem)
apply (vcg exspec=getSyscallArg_modifies)
apply simp
apply wp
apply (simp add: Collect_const_mem)
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_Cond_rhs_Seq)
-- "CNodeMove case"
apply (simp add: Collect_const[symmetric] split_def
injection_handler_returnOk whenE_def
ccorres_invocationCatch_Inr
performInvocation_def bindE_assoc
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule ccorres_move_c_guard_cte)
apply (rule ccorres_symb_exec_r)
apply (rule_tac xf'=newCap_' in ccorres_abstract, ceqv)
apply (rule_tac P="ccap_relation (cteCap rvb) rv'a"
in ccorres_gen_asm2)
apply csymbr
apply csymbr
apply (simp add: cap_get_tag_NullCap true_def)
apply (ctac add: setThreadState_ccorres)
apply (simp add: ccorres_cond_iffs)
apply (ctac(no_vcg) add: invokeCNodeMove_ccorres)
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (wp sts_valid_pspace_hangers)
apply (simp add: Collect_const_mem)
apply (vcg exspec=setThreadState_modifies)
apply vcg
apply (rule conseqPre, vcg, clarsimp)
apply (rule ccorres_Cond_rhs_Seq)
-- "CNodeMutate case"
apply (rule ccorres_rhs_assoc)+
apply (simp add: Collect_const[symmetric] del: Collect_const
cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: injection_handler_throwError dc_def[symmetric] if_P)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: if_not_P del: Collect_const)
apply (rule ccorres_add_return)
apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=4 and buffer=buffer])
apply (simp add: list_case_helper split_def hd_conv_nth
Collect_const[symmetric]
injection_handler_returnOk
del: Collect_const)
apply (rule ccorres_move_c_guard_cte)
apply (rule ccorres_symb_exec_r)
apply (rule_tac xf'="newCap_'" in ccorres_abstract, ceqv)
apply (rule_tac P="ccap_relation (updateCapData True (args ! 4) (cteCap rvb)) rv'a"
in ccorres_gen_asm2)
apply csymbr
apply csymbr
apply (simp add: cap_get_tag_isCap del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: whenE_def injection_handler_throwError
dc_def[symmetric] numeral_eqs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply (simp add: whenE_def injection_handler_returnOk
ccorres_invocationCatch_Inr numeral_eqs
performInvocation_def bindE_assoc)
apply (ctac add: setThreadState_ccorres)
apply (simp add: true_def ccorres_cond_iffs)
apply (ctac(no_vcg) add: invokeCNodeMove_ccorres)
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_return_C_errorE, simp+)[1]
apply (wp sts_valid_pspace_hangers)
apply (simp add: Collect_const_mem)
apply (vcg exspec=setThreadState_modifies)
apply (simp add: Collect_const_mem exception_defs)
apply (vcg exspec=updateCapData_spec2)