-
Notifications
You must be signed in to change notification settings - Fork 0
/
Syscall_R.thy
2399 lines (2189 loc) · 104 KB
/
Syscall_R.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)
*)
(*
Refinement for handleEvent and syscalls
*)
theory Syscall_R
imports Tcb_R Arch_R Interrupt_R
begin
declare if_weak_cong [cong]
(*
syscall has 5 sections: m_fault h_fault m_error h_error m_finalise
run m_fault (faultable code) \<rightarrow> r_fault
failure, i.e. Inr somefault \<rightarrow> \<lambda>somefault. h_fault; done
success, i.e. Inl a
\<rightarrow> run \<lambda>a. m_error a (errable code) \<rightarrow> r_error
failure, i.e. Inr someerror \<rightarrow> \<lambda>someerror. h_error e; done
success, i.e. Inl b \<rightarrow> \<lambda>b. m_finalise b
One can clearly see this is simulating some kind of monadic Maybe sequence
trying to identify all possible errors before actually performing the syscall.
*)
lemma syscall_corres:
assumes corres:
"corres (fr \<oplus> r_flt_rel) P P' m_flt m_flt'"
"\<And>flt flt'. flt' = fault_map flt \<Longrightarrow>
corres r (P_flt flt) (P'_flt flt') (h_flt flt) (h_flt' flt')"
"\<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow>
corres (ser \<oplus> r_err_rel rv rv')
(P_no_flt rv) (P'_no_flt rv')
(m_err rv) (m_err' rv')"
"\<And>rv rv' err err'. \<lbrakk>r_flt_rel rv rv'; err' = syscall_error_map err \<rbrakk>
\<Longrightarrow> corres r (P_err rv err)
(P'_err rv' err') (h_err err) (h_err' err')"
"\<And>rvf rvf' rve rve'. \<lbrakk>r_flt_rel rvf rvf'; r_err_rel rvf rvf' rve rve'\<rbrakk>
\<Longrightarrow> corres (intr \<oplus> r)
(P_no_err rvf rve) (P'_no_err rvf' rve')
(m_fin rve) (m_fin' rve')"
assumes wp:
"\<And>rv. \<lbrace>Q_no_flt rv\<rbrace> m_err rv \<lbrace>P_no_err rv\<rbrace>, \<lbrace>P_err rv\<rbrace>"
"\<And>rv'. \<lbrace>Q'_no_flt rv'\<rbrace> m_err' rv' \<lbrace>P'_no_err rv'\<rbrace>,\<lbrace>P'_err rv'\<rbrace>"
"\<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and Q_no_flt rv\<rbrace>, \<lbrace>P_flt\<rbrace>"
"\<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv. P'_no_flt rv and Q'_no_flt rv\<rbrace>, \<lbrace>P'_flt\<rbrace>"
shows "corres (intr \<oplus> r) (P and Q) (P' and Q')
(Syscall_A.syscall m_flt h_flt m_err h_err m_fin)
(Syscall_H.syscall m_flt' h_flt' m_err' h_err' m_fin')"
apply (simp add: Syscall_A.syscall_def Syscall_H.syscall_def liftE_bindE)
apply (rule corres_split_bind_sum_case)
apply (rule corres_split_bind_sum_case | rule corres | rule wp | simp add: liftE_bindE)+
done
lemma syscall_valid':
assumes x:
"\<And>ft. \<lbrace>P_flt ft\<rbrace> h_flt ft \<lbrace>Q\<rbrace>"
"\<And>err. \<lbrace>P_err err\<rbrace> h_err err \<lbrace>Q\<rbrace>"
"\<And>rv. \<lbrace>P_no_err rv\<rbrace> m_fin rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
"\<And>rv. \<lbrace>P_no_flt rv\<rbrace> m_err rv \<lbrace>P_no_err\<rbrace>, \<lbrace>P_err\<rbrace>"
"\<lbrace>P\<rbrace> m_flt \<lbrace>P_no_flt\<rbrace>, \<lbrace>P_flt\<rbrace>"
shows "\<lbrace>P\<rbrace> Syscall_H.syscall m_flt h_flt m_err h_err m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (simp add: Syscall_H.syscall_def liftE_bindE
cong: sum.case_cong)
apply (rule hoare_split_bind_sum_caseE)
apply (wp x)[1]
apply (rule hoare_split_bind_sum_caseE)
apply (wp x|simp)+
done
text {* Completing the relationship between abstract/haskell invocations *}
primrec
inv_relation :: "Invocations_A.invocation \<Rightarrow> Invocations_H.invocation \<Rightarrow> bool"
where
"inv_relation (Invocations_A.InvokeUntyped i) x =
(\<exists>i'. untypinv_relation i i' \<and> x = InvokeUntyped i')"
| "inv_relation (Invocations_A.InvokeEndpoint w w2 b) x =
(x = InvokeEndpoint w w2 b)"
| "inv_relation (Invocations_A.InvokeAsyncEndpoint w w2 w3) x =
(x = InvokeAsyncEndpoint w w2 w3)"
| "inv_relation (Invocations_A.InvokeReply w ptr) x =
(x = InvokeReply w (cte_map ptr))"
| "inv_relation (Invocations_A.InvokeTCB i) x =
(\<exists>i'. tcbinv_relation i i' \<and> x = InvokeTCB i')"
| "inv_relation (Invocations_A.InvokeDomain tptr domain) x =
(x = InvokeDomain tptr domain)"
| "inv_relation (Invocations_A.InvokeIRQControl i) x =
(\<exists>i'. irq_control_inv_relation i i' \<and> x = InvokeIRQControl i')"
| "inv_relation (Invocations_A.InvokeIRQHandler i) x =
(\<exists>i'. irq_handler_inv_relation i i' \<and> x = InvokeIRQHandler i')"
| "inv_relation (Invocations_A.InvokeCNode i) x =
(\<exists>i'. cnodeinv_relation i i' \<and> x = InvokeCNode i')"
| "inv_relation (Invocations_A.InvokeArchObject i) x =
(\<exists>i'. archinv_relation i i' \<and> x = InvokeArchObject i')"
(* In order to assert conditions that must hold for the appropriate
handleInvocation and handle_invocation calls to succeed, we must have
some notion of what a valid invocation is.
This function defines that.
For example, a InvokeEndpoint requires an endpoint at its first
constructor argument. *)
primrec
valid_invocation' :: "Invocations_H.invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"valid_invocation' (Invocations_H.InvokeUntyped i) = valid_untyped_inv' i"
| "valid_invocation' (Invocations_H.InvokeEndpoint w w2 b) = (ep_at' w and ex_nonz_cap_to' w)"
| "valid_invocation' (Invocations_H.InvokeAsyncEndpoint w w2 w3) = (aep_at' w and ex_nonz_cap_to' w)"
| "valid_invocation' (Invocations_H.InvokeTCB i) = tcb_inv_wf' i"
| "valid_invocation' (Invocations_H.InvokeDomain thread domain) =
(tcb_at' thread and K (domain \<le> maxDomain))"
| "valid_invocation' (Invocations_H.InvokeReply thread slot) =
(tcb_at' thread and cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap thread False) slot)"
| "valid_invocation' (Invocations_H.InvokeIRQControl i) = irq_control_inv_valid' i"
| "valid_invocation' (Invocations_H.InvokeIRQHandler i) = irq_handler_inv_valid' i"
| "valid_invocation' (Invocations_H.InvokeCNode i) = valid_cnode_inv' i"
| "valid_invocation' (Invocations_H.InvokeArchObject i) = valid_arch_inv' i"
(* FIXME: move *)
lemma dec_domain_inv_corres:
shows "\<lbrakk> list_all2 cap_relation (map fst cs) (map fst cs');
list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) cs cs' \<rbrakk> \<Longrightarrow>
corres (ser \<oplus> ((\<lambda>x. inv_relation x \<circ> uncurry Invocations_H.invocation.InvokeDomain) \<circ> (\<lambda>(x,y). Invocations_A.invocation.InvokeDomain x y))) \<top> \<top>
(decode_domain_invocation label args cs)
(decodeDomainInvocation label args cs')"
apply (simp add: decode_domain_invocation_def decodeDomainInvocation_def)
apply (rule whenE_throwError_corres_initial)
apply (simp+)[2]
apply (case_tac "args", simp_all)
apply (rule corres_guard_imp)
apply (rule_tac r'="\<lambda>domain domain'. domain = domain'" and R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>" in corres_splitEE)
apply (rule whenE_throwError_corres_initial)
apply simp
apply (case_tac "cs")
apply ((case_tac "cs'", ((simp add: null_def)+)[2])+)[2]
apply (subgoal_tac "cap_relation (fst (hd cs)) (fst (hd cs'))")
apply (case_tac "fst (hd cs)")
apply (case_tac "fst (hd cs')", simp+, rule corres_returnOkTT)
apply (simp add: inv_relation_def o_def uncurry_def)
apply (case_tac "fst (hd cs')", fastforce+)
apply (case_tac "cs")
apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2])
apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2])
apply (rule whenE_throwError_corres)
apply (simp+)[2]
apply (rule corres_returnOkTT)
apply (wp | simp)+
done
lemma decode_invocation_corres:
"\<lbrakk>cptr = to_bl cptr'; mi' = message_info_map mi;
slot' = cte_map slot; cap_relation cap cap';
args = args'; list_all2 cap_relation (map fst excaps) (map fst excaps');
list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) excaps excaps' \<rbrakk>
\<Longrightarrow>
corres (ser \<oplus> inv_relation)
(invs and valid_sched and valid_list
and valid_cap cap and cte_at slot and cte_wp_at (diminished cap) slot
and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_at (snd x) s)
and (\<lambda>s. length args < 2 ^ word_bits))
(invs' and valid_cap' cap' and cte_at' slot'
and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile>' fst x \<and> cte_at' (snd x) s)
and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(decode_invocation (mi_label mi) args cptr slot cap excaps)
(RetypeDecls_H.decodeInvocation (mi_label mi) args' cptr' slot' cap' excaps')"
apply (rule corres_gen_asm)
apply (unfold decode_invocation_def decodeInvocation_def)
apply (case_tac cap, simp_all only: cap.cases)
--"dammit, simp_all messes things up, must handle cases manually"
-- "Null"
apply (simp add: isCap_defs)
-- "Untyped"
apply (simp add: isCap_defs Let_def o_def split del: split_if)
apply clarsimp
apply (rule corres_guard_imp, rule dec_untyped_inv_corres)
apply ((clarsimp simp:cte_wp_at_caps_of_state diminished_def)+)[3]
-- "(Async)Endpoint"
apply (simp add: isCap_defs returnOk_def)
apply (simp add: isCap_defs)
apply (clarsimp simp: returnOk_def neq_Nil_conv)
-- "ReplyCap"
apply (simp add: isCap_defs Let_def returnOk_def)
-- "CNodeCap"
apply (simp add: isCap_defs Let_def CanModify_def
split del: split_if cong: if_cong)
apply (clarsimp simp add: o_def)
apply (rule corres_guard_imp)
apply (rule_tac F="length list \<le> 32" in corres_gen_asm)
apply (rule dec_cnode_inv_corres, simp+)
apply (simp add: valid_cap_def)
apply simp
-- "ThreadCap"
apply (simp add: isCap_defs Let_def CanModify_def
split del: split_if cong: if_cong)
apply (clarsimp simp add: o_def)
apply (rule corres_guard_imp)
apply (rule decode_tcb_inv_corres, rule refl,
simp_all add: valid_cap_def valid_cap'_def)[3]
apply (simp add: split_def)
apply (rule list_all2_conj)
apply (simp add: list_all2_map2 list_all2_map1)
apply assumption
-- "DomainCap"
apply (simp add: isCap_defs)
apply (rule corres_guard_imp)
apply (rule dec_domain_inv_corres)
apply (simp+)[4]
-- "IRQControl"
apply (simp add: isCap_defs o_def)
apply (rule corres_guard_imp, rule decode_irq_control_corres, simp+)[1]
-- "IRQHandler"
apply (simp add: isCap_defs o_def)
apply (rule corres_guard_imp, rule decode_irq_handler_corres, simp+)[1]
-- "Zombie"
apply (simp add: isCap_defs)
-- "Arch"
apply (clarsimp simp only: cap_relation.simps)
apply (clarsimp simp add: isCap_defs Let_def o_def)
apply (rule corres_guard_imp [OF dec_arch_inv_corres])
apply (simp_all add: list_all2_map2 list_all2_map1)+
apply (clarsimp simp: is_arch_diminished_def cte_wp_at_caps_of_state
is_cap_simps)
done
(* Levity: added (20090126 19:32:38) *)
declare mapME_Nil [simp]
crunch inv' [wp]: lookupCapAndSlot P
(* See also load_word_offs_corres *)
lemma load_word_offs_word_corres:
assumes y: "y < max_ipc_words"
and yv: "y' = y * 4"
shows "corres op = \<top> (valid_ipc_buffer_ptr' a) (load_word_offs_word a y) (loadWordUser (a + y'))"
unfolding loadWordUser_def yv using y
apply -
apply (rule corres_stateAssert_assume [rotated])
apply (simp add: pointerInUserData_def)
apply (erule valid_ipc_buffer_ptr'D2)
apply (subst word_mult_less_iff)
apply simp
apply (unfold word_bits_len_of)
apply (simp, subst mult_commute)
apply (rule nat_less_power_trans [where k = 2, simplified])
apply (rule unat_less_power)
apply (simp add: word_bits_conv)
apply (erule order_less_trans, simp add: max_ipc_words word_bits_conv)
apply (simp add: word_bits_conv)
apply (simp add: max_ipc_words word_bits_conv)
apply assumption
apply (rule is_aligned_mult_triv2 [where n = 2, simplified])
apply (simp add: word_bits_conv)
apply (rule corres_guard_imp)
apply (simp add: load_word_offs_word_def word_size_def)
apply (rule_tac F = "is_aligned a msg_align_bits" in corres_gen_asm2)
apply (rule corres_machine_op)
apply (rule corres_Id [OF refl refl])
apply (rule no_fail_pre)
apply wp
apply (erule aligned_add_aligned)
apply (rule is_aligned_mult_triv2 [where n = 2, simplified])
apply (simp add: word_bits_conv msg_align_bits)+
apply (simp add: valid_ipc_buffer_ptr'_def msg_align_bits)
done
lemma hinv_corres_assist:
"\<lbrakk> info' = message_info_map info \<rbrakk>
\<Longrightarrow> corres (fr \<oplus> (\<lambda>(p, cap, extracaps, buffer) (p', capa, extracapsa, buffera).
p' = cte_map p \<and> cap_relation cap capa \<and> buffer = buffera \<and>
list_all2
(\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))
extracaps extracapsa))
(invs and tcb_at thread and (\<lambda>_. valid_message_info info))
(invs' and tcb_at' thread)
(doE (cap, slot) \<leftarrow>
cap_fault_on_failure cptr' False
(lookup_cap_and_slot thread (to_bl cptr'));
do
buffer \<leftarrow> lookup_ipc_buffer False thread;
doE extracaps \<leftarrow> lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE)
(doE (cap, slot) \<leftarrow> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr');
do buffer \<leftarrow> VSpace_H.lookupIPCBuffer False thread;
doE extracaps \<leftarrow> lookupExtraCaps thread buffer info';
returnOk (slot, cap, extracaps, buffer)
odE
od
odE)"
apply (clarsimp simp add: split_def)
apply (rule corres_guard_imp)
apply (rule corres_splitEE [OF _ corres_cap_fault])
prefer 2
-- "switched over to argument of corres_cap_fault"
apply (rule lcs_corres, simp)
apply (rule corres_split [OF _ lipcb_corres])
apply (rule corres_splitEE [OF _ lec_corres])
apply (rule corres_returnOkTT)
apply simp+
apply (wp | simp)+
apply auto
done
lemma msg_from_lookup_failure_map[simp]:
"msgFromLookupFailure (lookup_failure_map f) = msg_from_lookup_failure f"
apply (simp add: msgFromLookupFailure_def)
apply (case_tac f, simp_all add: lookup_failure_map_def)
done
lemma msg_from_syserr_map[simp]:
"msgFromSyscallError (syscall_error_map err) = msg_from_syscall_error err"
apply (simp add: msgFromSyscallError_def)
apply (case_tac err,clarsimp+)
done
(* FIXME: move *)
lemma non_exst_same_timeSlice_upd[simp]:
"non_exst_same tcb (tcbDomain_update f tcb)"
by (cases tcb, simp add: non_exst_same_def)
lemma threadSet_tcbDomain_update_ct_idle_or_in_cur_domain':
"\<lbrace>ct_idle_or_in_cur_domain' and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread) \<rbrace>
threadSet (tcbDomain_update (\<lambda>_. domain)) t
\<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>"
apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
apply (wp hoare_vcg_disj_lift hoare_vcg_imp_lift)
apply (wp | wps)+
apply (auto simp: obj_at'_def)
done
lemma threadSet_tcbDomain_update_ct_not_inQ:
"\<lbrace>ct_not_inQ \<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
apply (simp add: threadSet_def ct_not_inQ_def)
apply (wp)
apply (rule hoare_convert_imp [OF setObject_nosch])
apply (rule updateObject_tcb_inv)
apply (wps setObject_ct_inv)
apply (wp setObject_tcb_strongest getObject_tcb_wp)
apply (case_tac "t = ksCurThread s")
apply (clarsimp simp: obj_at'_def)+
done
(* FIXME: move *)
lemma setObject_F_ct_activatable':
"\<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb \<rbrakk> \<Longrightarrow> \<lbrace>ct_in_state' activatable' and obj_at' (op = tcb) t\<rbrace>
setObject t (F f tcb)
\<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>"
apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def)
apply (rule hoare_pre)
apply (wps setObject_ct_inv)
apply (wp setObject_tcb_strongest)
apply (clarsimp simp: obj_at'_def)
done
lemmas setObject_tcbDomain_update_ct_activatable'[wp] = setObject_F_ct_activatable'[where F="tcbDomain_update", simplified]
(* FIXME: move *)
lemma setObject_F_st_tcb_at':
"\<lbrakk>\<And>tcb f. tcbState (F f tcb) = tcbState tcb \<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at' P t' and obj_at' (op = tcb) t\<rbrace>
setObject t (F f tcb)
\<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>"
apply (simp add: st_tcb_at'_def)
apply (rule hoare_pre)
apply (wp setObject_tcb_strongest)
apply (clarsimp simp: obj_at'_def)
done
lemmas setObject_tcbDomain_update_st_tcb_at'[wp] = setObject_F_st_tcb_at'[where F="tcbDomain_update", simplified]
lemma threadSet_tcbDomain_update_sch_act_wf[wp]:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s\<rbrace>
threadSet (tcbDomain_update (\<lambda>_. domain)) t
\<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: sch_act_wf_cases
split: scheduler_action.split)
apply (wp hoare_vcg_conj_lift)
apply (simp add: threadSet_def)
apply wp
apply (wps setObject_sa_unchanged)
apply (wp static_imp_wp getObject_tcb_wp)+
apply (clarsimp simp: obj_at'_def)
apply (rule hoare_vcg_all_lift)
apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s \<and> word \<noteq> t"
in hoare_strengthen_post)
apply (wp hoare_vcg_all_lift hoare_vcg_conj_lift hoare_imp_lift_something)+
apply (simp add: threadSet_def)
apply (wp_trace getObject_tcb_wp )
apply (clarsimp simp: obj_at'_def)
apply (wp threadSet_tcbDomain_triv')
apply (auto)
done
lemma threadSet_tcbDomain_update_invs':
"\<lbrace>invs' and tcb_at' t and sch_act_simple
and obj_at' (Not \<circ> tcbQueued) t
and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)
and K (domain \<le> maxDomain)\<rbrace>
threadSet (tcbDomain_update (\<lambda>_. domain)) t
\<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: invs'_def valid_state'_def split del: split_if)
apply (rule hoare_pre)
apply (wp_trace
threadSet_valid_pspace'
threadSet_valid_queues
threadSet_valid_queues'
threadSet_state_refs_of'T_P[where f'=id and P'=False and Q=\<bottom>]
threadSet_iflive'T
threadSet_ifunsafe'T
threadSet_idle'T
threadSet_global_refsT
threadSet_cur
irqs_masked_lift
valid_irq_node_lift
valid_irq_handlers_lift''
threadSet_ctes_ofT
threadSet_tcbDomain_update_ct_not_inQ
threadSet_valid_dom_schedule'
threadSet_tcbDomain_update_sch_act_wf
threadSet_tcbDomain_update_ct_idle_or_in_cur_domain'
| clarsimp simp: tcb_cte_cases_def)+
apply (auto simp: inQ_def obj_at'_def)
done
lemma set_domain_setDomain_corres:
"corres dc
(valid_etcbs and valid_sched and tcb_at tptr)
(invs' and sch_act_simple
and tcb_at' tptr and (\<lambda>s. new_dom \<le> maxDomain))
(set_domain tptr new_dom)
(setDomain tptr new_dom)"
apply (rule corres_gen_asm2)
apply (simp add: set_domain_def setDomain_def thread_set_domain_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ gct_corres])
apply (rule corres_split[OF _ tcbSchedDequeue_corres])
apply (rule corres_split[OF _ ethread_set_corres])
apply (rule corres_split[OF _ gts_isRunnable_corres])
apply simp
apply (rule corres_split[OF corres_when[OF refl]])
apply (rule rescheduleRequired_corres)
apply clarsimp
apply (rule corres_when[OF refl])
apply (rule tcbSchedEnqueue_corres)
apply (wp hoare_drop_imps hoare_vcg_conj_lift | clarsimp| assumption)+
apply (clarsimp simp: etcb_relation_def)
apply ((wp_trace hoare_vcg_conj_lift hoare_vcg_disj_lift | clarsimp)+)[1]
apply clarsimp
apply (rule_tac Q="\<lambda>_. valid_objs' and valid_queues' and valid_queues and
(\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and tcb_at' tptr"
in hoare_strengthen_post[rotated])
apply (auto simp: invs'_def valid_state'_def sch_act_wf_weak st_tcb_at'_def o_def)[1]
apply (wp threadSet_valid_objs' threadSet_valid_queues'_no_state
threadSet_valid_queues_no_state
threadSet_st_tcb_no_state | simp)+
apply (rule_tac Q = "\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s
\<and> tcb_at' tptr s" in hoare_strengthen_post[rotated])
apply (clarsimp simp:invs'_def valid_state'_def valid_pspace'_def sch_act_simple_def)
apply (clarsimp simp:valid_tcb'_def)
apply (drule(1) bspec)
apply (clarsimp simp:tcb_cte_cases_def)
apply fastforce
apply (wp hoare_vcg_all_lift Tcb_R.tcbSchedDequeue_not_in_queue)
apply clarsimp
apply (frule tcb_at_is_etcb_at)
apply simp+
apply (auto elim: tcb_at_is_etcb_at valid_objs'_maxDomain valid_objs'_maxPriority st_tcb'_weakenE
simp: valid_sched_def valid_sched_action_def)
done
lemma pinv_corres:
"\<lbrakk> inv_relation i i'; call \<longrightarrow> block \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> op=)
(einvs and valid_invocation i
and simple_sched_action
and ct_active
and (\<lambda>s. (\<exists>w w2 b. i = Invocations_A.InvokeEndpoint w w2 b) \<longrightarrow> st_tcb_at simple (cur_thread s) s))
(invs' and sch_act_simple and valid_invocation' i' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(perform_invocation block call i) (performInvocation block call i')"
apply (simp add: performInvocation_def)
apply (case_tac i)
apply (clarsimp simp: o_def liftE_bindE)
apply (rule corres_guard_imp)
apply (rule corres_split[OF corres_returnOkTT])
apply simp
apply (erule corres_guard_imp [OF inv_untyped_corres])
apply assumption+
apply wp
apply simp+
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ gct_corres])
apply simp
apply (rule corres_split [OF _ send_ipc_corres])
apply (rule corres_trivial)
apply simp
apply simp
apply wp
apply (clarsimp simp: ct_in_state_def)
apply (fastforce elim: st_tcb_ex_cap)
apply (clarsimp simp: pred_conj_def invs'_def cur_tcb'_def simple_sane_strg
sch_act_simple_def)
apply (rule corres_guard_imp)
apply (simp add: liftE_bindE)
apply (rule corres_split [OF _ send_async_ipc_corres])
apply (rule corres_trivial)
apply (simp add: returnOk_def)
apply wp
apply (simp+)[2]
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split_eqr [OF _ gct_corres])
apply (rule corres_split_nor [OF _ do_reply_transfer_corres])
apply (rule corres_trivial, simp)
apply wp
apply (clarsimp simp: tcb_at_invs)
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def)
apply (clarsimp simp: tcb_at_invs')
apply (fastforce elim!: cte_wp_at_weakenE')
apply (clarsimp simp: liftME_def)
apply (rule corres_guard_imp)
apply (erule tcbinv_corres)
apply (simp)+
-- "domain cap"
apply (clarsimp simp: invoke_domain_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ set_domain_setDomain_corres])
apply (rule corres_trivial, simp)
apply (wp)
apply (clarsimp+)[2]
-- "CNodes"
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_splitEE [OF _ inv_cnode_corres])
apply (rule corres_trivial, simp add: returnOk_def)
apply assumption
apply wp
apply (clarsimp+)[2]
apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric])
apply (rule corres_guard_imp, rule invoke_irq_control_corres, simp+)
apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric])
apply (rule corres_guard_imp, rule invoke_irq_handler_corres, simp+)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule inv_arch_corres, assumption)
apply (clarsimp+)[2]
done
lemma sendAsyncIPC_tcb_at'[wp]:
"\<lbrace>tcb_at' t\<rbrace>
sendAsyncIPC aepptr bdg val
\<lbrace>\<lambda>rv. tcb_at' t\<rbrace>"
apply (simp add: sendAsyncIPC_def doAsyncTransfer_def
cong: list.case_cong async_endpoint.case_cong)
apply (wp aep'_cases_weak_wp list_cases_weak_wp)
apply simp
done
lemmas checkCap_inv_typ_at'
= checkCap_inv[where P="\<lambda>s. P (typ_at' T p s)", standard]
crunch typ_at'[wp]: restart "\<lambda>s. P (typ_at' T p s)"
crunch typ_at'[wp]: performTransfer "\<lambda>s. P (typ_at' T p s)"
lemma invokeTCB_typ_at'[wp]:
"\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace>
invokeTCB tinv
\<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
apply (cases tinv,
simp_all add: invokeTCB_def
getThreadBufferSlot_def locateSlot_conv
split del: split_if)
apply (simp only: cases_simp if_cancel simp_thms conj_ac pred_conj_def
Let_def split_def getThreadVSpaceRoot
| (simp split del: split_if cong: if_cong)
| (wp mapM_x_wp[where S=UNIV, simplified]
checkCap_inv_typ_at'
option_cases_weak_wp)[1]
| wpcw)+
done
lemmas invokeTCB_typ_ats[wp] = typ_at_lifts [OF invokeTCB_typ_at']
crunch typ_at'[wp]: doReplyTransfer "\<lambda>s. P (typ_at' T p s)"
(wp: hoare_drop_imps)
lemmas doReplyTransfer_typ_ats[wp] = typ_at_lifts [OF doReplyTransfer_typ_at']
crunch typ_at'[wp]: invokeIRQControl "\<lambda>s. P (typ_at' T p s)"
lemmas invokeIRQControl_typ_ats[wp] = typ_at_lifts [OF invokeIRQControl_typ_at']
crunch typ_at'[wp]: invokeIRQHandler "\<lambda>s. P (typ_at' T p s)"
lemmas invokeIRQHandler_typ_ats[wp] = typ_at_lifts [OF invokeIRQHandler_typ_at']
crunch tcb_at'[wp]: setDomain "tcb_at' tptr"
(simp: crunch_simps)
lemma pinv_tcb'[wp]:
"\<lbrace>invs' and st_tcb_at' active' tptr
and valid_invocation' i and ct_active'\<rbrace>
RetypeDecls_H.performInvocation block call i
\<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>"
apply (simp add: performInvocation_def)
apply (case_tac i, simp_all)
apply (wp invokeArch_tcb_at' | clarsimp simp: st_tcb_at')+
done
lemma setQueue_cte_wp_at[wp]:
"\<lbrace>cte_wp_at' P p\<rbrace> setQueue d prio queue \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>"
apply (simp add: setQueue_def)
apply wp
apply (clarsimp elim!: cte_wp_at'_pspaceI)
done
lemma sts_cte_at[wp]:
"\<lbrace>cte_at' p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_at' p\<rbrace>"
apply (simp add: setThreadState_def)
apply (wp|simp)+
done
lemma sts_valid_inv'[wp]:
"\<lbrace>valid_invocation' i\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_invocation' i\<rbrace>"
apply (case_tac i, simp_all add: sts_valid_untyped_inv' sts_valid_arch_inv')
apply (wp | simp)+
apply (case_tac tcbinvocation,
simp_all add: setThreadState_tcb',
auto intro!: hoare_vcg_conj_lift hoare_vcg_disj_lift
simp only: imp_conv_disj simp_thms pred_conj_def,
auto intro!: hoare_vcg_prop
sts_cap_to' sts_cte_cap_to'
setThreadState_typ_ats
split: option.splits)[1]
apply (case_tac cnode_invocation, simp_all add: cte_wp_at_ctes_of)
apply (wp | simp)+
apply (case_tac irqcontrol_invocation, simp_all)
apply (wp | simp add: irq_issued'_def)+
apply (case_tac irqhandler_invocation, simp_all)
apply (wp hoare_vcg_ex_lift ex_cte_cap_to'_pres | simp)+
done
(* FIXME: move to TCB *)
crunch inv[wp]: decodeDomainInvocation P
(wp: crunch_wps simp: crunch_simps)
lemma decode_inv_inv'[wp]:
"\<lbrace>P\<rbrace> decodeInvocation label args cap_index slot cap excaps \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decodeInvocation_def Let_def
split del: split_if
cong: if_cong)
apply (rule hoare_pre)
apply (wp decodeTCBInv_inv |
simp only: o_def |
clarsimp split: capability.split_asm simp: isCap_defs)+
done
lemma diminished_IRQHandler' [simp]:
"diminished' (IRQHandlerCap h) cap = (cap = IRQHandlerCap h)"
apply (rule iffI)
apply (drule diminished_capMaster)
apply clarsimp
apply (simp add: diminished'_def maskCapRights_def isCap_simps Let_def)
done
lemma diminished_ReplyCap' [simp]:
"diminished' (ReplyCap x y) cap = (cap = ReplyCap x y)"
apply (rule iffI)
apply (clarsimp simp: diminished'_def maskCapRights_def Let_def split del: split_if)
apply (cases cap, simp_all add: isCap_simps)[1]
apply (simp add: ArchRetype_H.maskCapRights_def split: arch_capability.splits)
apply (simp add: diminished'_def maskCapRights_def isCap_simps Let_def)
done
lemma diminished_IRQControlCap' [simp]:
"diminished' IRQControlCap cap = (cap = IRQControlCap)"
apply (rule iffI)
apply (drule diminished_capMaster)
apply clarsimp
apply (simp add: diminished'_def maskCapRights_def isCap_simps Let_def)
done
(* FIXME: move to TCB *)
lemma dec_dom_inv_wf[wp]:
"\<lbrace>invs' and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile>' fst x)\<rbrace>
decodeDomainInvocation label args excaps
\<lbrace>\<lambda>x s. tcb_at' (fst x) s \<and> snd x \<le> maxDomain\<rbrace>, -"
apply (simp add:decodeDomainInvocation_def)
apply (wp whenE_throwError_wp | wpc |simp)+
apply clarsimp
apply (drule_tac x = "hd excaps" in bspec)
apply (rule hd_in_set)
apply (simp add:null_def)
apply (simp add:valid_cap'_def)
apply (simp add:not_le)
apply (simp add:ucast_nat_def[symmetric])
apply (rule word_of_nat_le)
apply (simp add:numDomains_def maxDomain_def)
done
lemma decode_inv_wf'[wp]:
"\<lbrace>valid_cap' cap and invs' and sch_act_simple
and cte_wp_at' (diminished' cap \<circ> cteCap) slot and real_cte_at' slot
and (\<lambda>s. \<forall>r\<in>zobj_refs' cap. ex_nonz_cap_to' r s)
and (\<lambda>s. \<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_to' r s)
and (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_to' r s)
and (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s)
and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at' (diminished' (fst x) o cteCap) (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile>' fst x)
and (\<lambda>s. \<forall>x \<in> set excaps. real_cte_at' (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at' (badge_derived' (fst x) o cteCap) (snd x) s)
and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
decodeInvocation label args cap_index slot cap excaps
\<lbrace>valid_invocation'\<rbrace>,-"
apply (case_tac cap, simp_all add: decodeInvocation_def Let_def isCap_defs uncurry_def split_def
split del: split_if
cong: if_cong)
apply ((rule hoare_pre,
((wp_trace decodeTCBInv_wf | simp add: o_def)+)[1],
clarsimp simp: valid_cap'_def cte_wp_at_ctes_of
| (rule exI, rule exI, erule (1) conjI))+)
done
lemma ct_active_imp_simple'[elim!]:
"ct_active' s \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s"
by (clarsimp simp: ct_in_state'_def
elim!: st_tcb'_weakenE)
lemma ct_running_imp_simple'[elim!]:
"ct_running' s \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s"
by (clarsimp simp: ct_in_state'_def
elim!: st_tcb'_weakenE)
lemma active_ex_cap'[elim]:
"\<lbrakk> ct_active' s; if_live_then_nonz_cap' s \<rbrakk>
\<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s"
by (fastforce simp: ct_in_state'_def elim!: st_tcb_ex_cap'')
crunch st_tcb'[wp]: handleFaultReply "st_tcb_at' P t"
crunch it[wp]: handleFaultReply "\<lambda>s. P (ksIdleThread s)"
lemma handleFaultReply_invs[wp]:
"\<lbrace>invs' and tcb_at' t\<rbrace> handleFaultReply x t label msg \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: handleFaultReply_def)
apply (case_tac x, simp_all)
apply (wp | simp)+
done
crunch sch_act_simple[wp]: handleFaultReply sch_act_simple
(wp: crunch_wps)
lemma transferCaps_non_null_cte_wp_at':
assumes PUC: "\<And>cap. P cap \<Longrightarrow> \<not> isUntypedCap cap"
shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
transferCaps info caps ep rcvr rcvBuf dim
\<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>"
proof -
have CTEF: "\<And>P p s. \<lbrakk> cte_wp_at' P p s; \<And>cte. P cte \<Longrightarrow> False \<rbrakk> \<Longrightarrow> False"
by (erule cte_wp_atE', auto)
show ?thesis
unfolding transferCaps_def
apply (wp | wpc)+
apply (rule transferCapsToSlots_pres2)
apply (rule hoare_weaken_pre [OF cteInsert_weak_cte_wp_at3])
apply (rule PUC,simp)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (wp hoare_vcg_all_lift static_imp_wp | simp add:ball_conj_distrib)+
done
qed
crunch cte_wp_at' [wp]: setMessageInfo "cte_wp_at' P p"
lemma copyMRs_cte_wp_at'[wp]:
"\<lbrace>cte_wp_at' P ptr\<rbrace> copyMRs sender sendBuf receiver recvBuf n \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace>"
unfolding copyMRs_def
apply (wp mapM_wp | wpc | simp add: split_def | rule equalityD1)+
done
lemma doNormalTransfer_non_null_cte_wp_at':
assumes PUC: "\<And>cap. P cap \<Longrightarrow> \<not> isUntypedCap cap"
shows
"\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
doNormalTransfer st send_buffer ep b gr rt recv_buffer dim
\<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>"
unfolding doNormalTransfer_def
apply (wp transferCaps_non_null_cte_wp_at' | simp add:PUC)+
done
lemma setMRs_cte_wp_at'[wp]:
"\<lbrace>cte_wp_at' P ptr\<rbrace> setMRs thread buffer messageData \<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace>"
by (simp add: setMRs_def zipWithM_x_mapM split_def, wp crunch_wps)
lemma doFaultTransfer_cte_wp_at'[wp]:
"\<lbrace>cte_wp_at' P ptr\<rbrace>
doFaultTransfer badge sender receiver receiverIPCBuffer
\<lbrace>\<lambda>_. cte_wp_at' P ptr\<rbrace>"
unfolding doFaultTransfer_def
apply (wp | wpc | simp add: split_def)+
done
lemma doIPCTransfer_non_null_cte_wp_at':
assumes PUC: "\<And>cap. P cap \<Longrightarrow> \<not> isUntypedCap cap"
shows
"\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
doIPCTransfer sender endpoint badge grant receiver dim
\<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>"
unfolding doIPCTransfer_def
apply (wp doNormalTransfer_non_null_cte_wp_at' hoare_drop_imp hoare_allI | wpc | clarsimp simp:PUC)+
done
lemma doIPCTransfer_non_null_cte_wp_at2':
fixes P
assumes PNN: "\<And>cte. P (cteCap cte) \<Longrightarrow> cteCap cte \<noteq> capability.NullCap"
and PUC: "\<And>cap. P cap \<Longrightarrow> \<not> isUntypedCap cap"
shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace>
doIPCTransfer sender endpoint badge grant receiver dim
\<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace>"
proof -
have PimpQ: "\<And>P Q ptr s. \<lbrakk> cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s;
\<And>cte. P (cteCap cte) \<Longrightarrow> Q (cteCap cte) \<rbrakk>
\<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> Q (cteCap cte)) ptr s"
by (erule cte_wp_at_weakenE', clarsimp)
show ?thesis
apply (rule hoare_chain [OF doIPCTransfer_non_null_cte_wp_at'])
apply (erule PUC)
apply (erule PimpQ)
apply (drule PNN, clarsimp)
apply (erule cte_wp_at_weakenE')
apply (clarsimp)
done
qed
lemma st_tcb_at'_eqD:
"\<lbrakk> st_tcb_at' (\<lambda>s. s = st) t s; st_tcb_at' (\<lambda>s. s = st') t s \<rbrakk> \<Longrightarrow> st = st'"
by (clarsimp simp add: st_tcb_at'_def obj_at'_def)
lemma isReply_awaiting_reply':
"isReply st = awaiting_reply' st"
by (case_tac st, (clarsimp simp add: isReply_def)+)
lemma doReply_invs[wp]:
"\<lbrace>tcb_at' t and tcb_at' t' and
cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t False) slot and
invs' and sch_act_simple\<rbrace>
doReplyTransfer t' t slot
\<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: doReplyTransfer_def liftM_def)
apply (rule hoare_seq_ext [OF _ gts_sp'])
apply (rule hoare_seq_ext [OF _ assert_sp])
apply (rule hoare_seq_ext [OF _ getCTE_sp])
apply (wp, wpc)
apply (wp)
apply (wp_once sts_invs_minor'')
apply (simp)
apply (wp_once sts_st_tcb')
apply (wp)[1]
apply (rule_tac Q="\<lambda>rv s. invs' s
\<and> t \<noteq> ksIdleThread s
\<and> st_tcb_at' awaiting_reply' t s"
in hoare_post_imp)
apply (clarsimp)
apply (frule_tac t=t in invs'_not_runnable_not_queued)
apply (erule st_tcb'_weakenE, case_tac st, clarsimp+)
apply (rule conjI, erule st_tcb'_weakenE, case_tac st, clarsimp+)
apply (rule conjI, rule impI, erule st_tcb'_weakenE, case_tac st)
apply (clarsimp | drule(1) obj_at_conj')+
apply (clarsimp simp: invs'_def valid_state'_def ct_in_state'_def)
apply (drule(1) st_tcb_at_conj')
apply (subgoal_tac "st_tcb_at' (\<lambda>_. False) (ksCurThread s) s")
apply (clarsimp)
apply (erule_tac P="\<lambda>st. awaiting_reply' st \<and> activatable' st"
in st_tcb'_weakenE)
apply (case_tac st, clarsimp+)
apply (wp cteDeleteOne_reply_st_tcb_at)
apply (clarsimp)
apply (rule_tac Q="\<lambda>_. (\<lambda>s. t \<noteq> ksIdleThread s)
and cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t False) slot"
in hoare_strengthen_post [rotated])
apply clarsimp
apply (erule cte_wp_at_weakenE', simp)
apply (wp)
apply (rule hoare_strengthen_post [OF doIPCTransfer_non_null_cte_wp_at'])
apply (erule conjE)
apply assumption
apply (erule cte_wp_at_weakenE')
apply (fastforce)
apply (wp sts_invs_minor'' sts_st_tcb' static_imp_wp)
apply (rule_tac Q="\<lambda>rv s. invs' s \<and> sch_act_simple s
\<and> st_tcb_at' awaiting_reply' t s
\<and> t \<noteq> ksIdleThread s"
in hoare_post_imp)
apply (clarsimp)
apply (frule_tac t=t in invs'_not_runnable_not_queued)
apply (erule st_tcb'_weakenE, case_tac st, clarsimp+)
apply (rule conjI, erule st_tcb'_weakenE, case_tac st, clarsimp+)
apply (rule conjI, rule impI, erule st_tcb'_weakenE, case_tac st)
apply (clarsimp | drule(1) obj_at_conj')+
apply (clarsimp simp: invs'_def valid_state'_def ct_in_state'_def)
apply (drule(1) st_tcb_at_conj')
apply (subgoal_tac "st_tcb_at' (\<lambda>_. False) (ksCurThread s) s")
apply (clarsimp)
apply (erule_tac P="\<lambda>st. awaiting_reply' st \<and> activatable' st"
in st_tcb'_weakenE)
apply (case_tac st, clarsimp+)
apply (wp threadSet_invs_trivial threadSet_st_tcb_at2 static_imp_wp
| clarsimp simp add: inQ_def)+
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t
and sch_act_simple and st_tcb_at' awaiting_reply' t"
in hoare_strengthen_post [rotated])
apply (clarsimp)
apply (rule conjI)
apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def)
apply (rule conjI)
apply clarsimp
apply clarsimp
apply (drule(1) st_tcb_at'_eqD, simp)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def)
apply (erule st_tcb'_weakenE, clarsimp)
apply (rule conjI)
apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def)
apply (drule(1) st_tcb_at'_eqD, simp)
apply (rule conjI)
apply clarsimp
apply (frule invs'_not_runnable_not_queued)
apply (erule st_tcb'_weakenE, clarsimp)
apply (frule (1) not_tcbQueued_not_ksQ)
apply simp
apply clarsimp
apply (wp cteDeleteOne_reply_st_tcb_at hoare_drop_imp hoare_allI)
apply (clarsimp simp add: isReply_awaiting_reply' cte_wp_at_ctes_of)
apply (auto dest!: st_tcb_idle'[rotated] simp:isCap_simps)
done
lemma ct_active_runnable' [simp]:
"ct_active' s \<Longrightarrow> ct_in_state' runnable' s"
by (fastforce simp: ct_in_state'_def elim!: st_tcb'_weakenE)
lemma valid_irq_node_tcbSchedEnqueue[wp]:
"\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s \<rbrace> tcbSchedEnqueue ptr
\<lbrace>\<lambda>rv s'. valid_irq_node' (irq_node' s') s'\<rbrace>"
apply (rule hoare_pre)
apply (simp add:valid_irq_node'_def )
apply (wp hoare_unless_wp hoare_vcg_all_lift | wps)+
apply (simp add:tcbSchedEnqueue_def)
apply (wp hoare_unless_wp| simp)+
apply (simp add:valid_irq_node'_def)
done
lemma updateDomain_valid_pspace[wp]:
"\<lbrace>\<lambda>s. valid_pspace' s \<and> ds \<le> maxDomain \<rbrace> threadSet (tcbDomain_update (\<lambda>_. ds)) thread
\<lbrace>\<lambda>r. valid_pspace'\<rbrace>"
apply (rule hoare_name_pre_state)
apply (wp threadSet_valid_pspace'T)
apply (auto simp:tcb_cte_cases_def)
done
lemma rescheduleRequired_valid_queues_but_ct_domain:
"\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> valid_objs' s
\<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) \<rbrace>
rescheduleRequired
\<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>"
apply (simp add: rescheduleRequired_def)
apply (wp | wpc | simp)+
done
lemma rescheduleRequired_valid_queues'_but_ct_domain:
"\<lbrace>\<lambda>s. valid_queues' s
\<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)
\<rbrace>
rescheduleRequired
\<lbrace>\<lambda>_. valid_queues'\<rbrace>"
apply (simp add: rescheduleRequired_def)
apply (wp | wpc | simp | fastforce simp: valid_queues'_def)+
done
lemma tcbSchedEnqueue_valid_action:
"\<lbrace>\<lambda>s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s\<rbrace>
tcbSchedEnqueue ptr
\<lbrace>\<lambda>rv s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s\<rbrace>"
apply (wp_trace hoare_vcg_all_lift hoare_vcg_imp_lift)
apply clarsimp
done
abbreviation (input) "all_invs_but_sch_extra \<equiv>