-
Notifications
You must be signed in to change notification settings - Fork 0
/
Syscall_AI.thy
1266 lines (1107 loc) · 52.4 KB
/
Syscall_AI.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_AI
imports
BCorres2_AI
Tcb_AI
Arch_AI
Interrupt_AI
begin
(*
lemmas schedule_ct_activateable'[wp] = use_bcorres[where Q="\<lambda>_. ct_in_state activatable" and P="invs",simplified o_def,simplified, OF schedule_bcorres schedule_ct_activateable]
*)
(*
lemmas schedule_invs'[wp] = use_bcorres[where Q="\<lambda>_. invs" and P="invs",simplified o_def,simplified, OF schedule_bcorres schedule_invs]
*)
lemma schedule_invs[wp]: "\<lbrace>invs\<rbrace> (Schedule_A.schedule :: (unit,det_ext) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: Schedule_A.schedule_def)
apply (wp dmo_invs thread_get_inv gts_wp
do_machine_op_tcb when_def hoare_vcg_all_lift
| wpc | clarsimp simp: guarded_switch_to_def get_tcb_def choose_thread_def
| wp_once hoare_drop_imps)+
done
lemma schedule_ct_activateable[wp]:
"\<lbrace>invs\<rbrace> (Schedule_A.schedule :: (unit,det_ext) s_monad) \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>"
proof -
have P: "\<And>t s. ct_in_state activatable (cur_thread_update (\<lambda>_. t) s) = st_tcb_at activatable t s"
by (fastforce simp: ct_in_state_def st_tcb_at_def intro: obj_at_pspaceI)
show ?thesis
apply (simp add: Schedule_A.schedule_def)
apply (wp dmo_st_tcb_at gts_wp
stt_activatable stit_activatable hoare_vcg_all_lift
| simp add: P set_scheduler_action_def guarded_switch_to_def choose_thread_def
next_domain_def Let_def tcb_sched_action_def set_tcb_queue_def
get_tcb_queue_def ethread_get_def
| wpc | wp_once hoare_drop_imps)+
apply (force simp: ct_in_state_def st_tcb_at_def obj_at_def invs_def valid_state_def
valid_idle_def split: split_if_asm)
done
qed
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_A.syscall m_flt h_flt m_err h_err m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (simp add: Syscall_A.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
(* 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_A.invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_invocation (Invocations_A.InvokeUntyped i) = valid_untyped_inv i"
| "valid_invocation (Invocations_A.InvokeEndpoint w w2 b) = (ep_at w and ex_nonz_cap_to w)"
| "valid_invocation (Invocations_A.InvokeAsyncEndpoint w w2 w3) = (aep_at w and ex_nonz_cap_to w)"
| "valid_invocation (Invocations_A.InvokeTCB i) = tcb_inv_wf i"
| "valid_invocation (Invocations_A.InvokeDomain thread domain) = (tcb_at thread and (\<lambda>s. thread \<noteq> idle_thread s))"
| "valid_invocation (Invocations_A.InvokeReply thread slot) =
(tcb_at thread and cte_wp_at (op = (cap.ReplyCap thread False)) slot)"
| "valid_invocation (Invocations_A.InvokeIRQControl i) = irq_control_inv_valid i"
| "valid_invocation (Invocations_A.InvokeIRQHandler i) = irq_handler_inv_valid i"
| "valid_invocation (Invocations_A.InvokeCNode i) = valid_cnode_inv i"
| "valid_invocation (Invocations_A.InvokeArchObject i) = valid_arch_inv i"
crunch inv [wp]: lookup_cap_and_slot P
lemma sts_Restart_invs[wp]:
"\<lbrace>st_tcb_at active t and invs and ex_nonz_cap_to t\<rbrace>
set_thread_state t Structures_A.Restart
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (wp sts_invs_minor2)
apply (auto elim!: st_tcb_weakenE
notE [rotated, OF _ idle_no_ex_cap]
simp: invs_def valid_state_def valid_pspace_def)
done
lemma invoke_tcb_tcb[wp]:
"\<lbrace>tcb_at tptr\<rbrace> invoke_tcb i \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>"
by (simp add: tcb_at_typ invoke_tcb_typ_at [where P=id, simplified])
lemma invoke_domain_tcb[wp]:
"\<lbrace>tcb_at tptr\<rbrace> invoke_domain thread domain \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>"
by (simp add: tcb_at_typ invoke_domain_typ_at [where P=id, simplified])
lemma simple_from_active:
"st_tcb_at active t s \<Longrightarrow> st_tcb_at simple t s"
by (fastforce elim!: st_tcb_weakenE)
lemma simple_from_running:
"ct_running s \<Longrightarrow> st_tcb_at simple (cur_thread s) s"
by (fastforce simp: ct_in_state_def
elim!: st_tcb_weakenE)
crunch st_tcb[wp]: handle_fault_reply "st_tcb_at P t"
crunch invs[wp]: handle_fault_reply "invs"
crunch cap_to[wp]: handle_fault_reply "ex_nonz_cap_to c"
crunch it[wp]: handle_fault_reply "\<lambda>s. P (idle_thread s)"
crunch caps[wp]: handle_fault_reply "\<lambda>s. P (caps_of_state s)"
crunch cap_to[wp]: handle_fault_reply "ex_nonz_cap_to c"
crunch it[wp]: handle_fault_reply "\<lambda>s. P (idle_thread s)"
crunch caps[wp]: handle_fault_reply "\<lambda>s. P (caps_of_state s)"
lemma st_tcb_at_eq:
"\<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 do_ipc_transfer_tcb_at [wp]:
"\<lbrace>\<lambda>s. P (tcb_at t s)\<rbrace> do_ipc_transfer s ep bg grt r dim \<lbrace>\<lambda>rv s. P (tcb_at t s)\<rbrace>"
by (simp add: tcb_at_typ) wp
lemma do_ipc_transfer_emptyable[wp]:
"\<lbrace>emptyable sl\<rbrace> do_ipc_transfer sender ep badge grant receiver diminis \<lbrace>\<lambda>_. emptyable sl\<rbrace>"
apply (clarsimp simp add: emptyable_def)
apply (wp hoare_convert_imp | clarsimp)+
done
crunch emptyable[wp]: do_ipc_transfer "emptyable sl"
lemma do_ipc_transfer_non_null_cte_wp_at2:
fixes P
assumes PNN: "\<And>cap. P cap \<Longrightarrow> cap \<noteq> cap.NullCap"
assumes PUC: "\<And>cap. P cap \<Longrightarrow> \<not> is_untyped_cap cap"
shows "\<lbrace>valid_objs and cte_wp_at P ptr\<rbrace> do_ipc_transfer st ep b gr rt dim \<lbrace>\<lambda>_. cte_wp_at P ptr\<rbrace>"
proof -
have PimpQ: "\<And>P Q ptr s. \<lbrakk> cte_wp_at P ptr s; \<And>cap. P cap \<Longrightarrow> Q cap \<rbrakk> \<Longrightarrow> cte_wp_at (P and Q) ptr s"
by (erule cte_wp_at_weakenE, clarsimp)
show ?thesis
apply (rule hoare_chain [OF do_ipc_transfer_non_null_cte_wp_at])
apply (erule PUC)
apply (clarsimp )
apply (erule PimpQ)
apply (drule PNN, clarsimp)
apply (erule cte_wp_at_weakenE)
apply (clarsimp)
done
qed
lemma thread_set_cap_to:
"(\<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF tcb)
\<Longrightarrow> \<lbrace>ex_nonz_cap_to p\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. ex_nonz_cap_to p\<rbrace>"
apply (clarsimp simp add: ex_nonz_cap_to_def)
apply (wp hoare_ex_wp thread_set_cte_wp_at_trivial)
apply (clarsimp)
done
lemma thread_set_has_no_reply_cap:
"(\<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF tcb)
\<Longrightarrow> \<lbrace>\<lambda>s. \<not>has_reply_cap tt s\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. \<not>has_reply_cap tt s\<rbrace>"
apply (clarsimp simp add: has_reply_cap_def)
apply (wp hoare_vcg_all_lift thread_set_cte_wp_at_trivial)
apply (clarsimp)
done
lemma set_object_cte_wp_at2:
"\<lbrace>\<lambda>s. P (cte_wp_at P' p (s\<lparr>kheap := kheap s(ptr \<mapsto> ko)\<rparr>))\<rbrace> set_object ptr ko \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>"
unfolding set_object_def
apply (wp)
done
lemma handle_fault_reply_cte_wp_at:
"\<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>"
proof -
have SC:
"\<And>p' s tcb nc. get_tcb p' s = Some tcb
\<Longrightarrow> obj_at (same_caps (TCB (tcb \<lparr>tcb_context := nc\<rparr>))) p' s"
apply (drule get_tcb_ko_at [THEN iffD1])
apply (erule ko_at_weakenE)
apply (clarsimp simp add: tcb_cap_cases_def)
done
have NC:
"\<And>p' s tcb P nc. get_tcb p' s = Some tcb
\<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := kheap s(p' \<mapsto> TCB (tcb\<lparr>tcb_context := nc\<rparr>))\<rparr>)
= cte_wp_at P p s"
apply (drule_tac nc=nc in SC)
apply (drule_tac P=P and p=p in cte_wp_at_after_update)
apply (drule sym)
apply (clarsimp)
apply (rule_tac x="s \<lparr> kheap := ?p \<rparr>" in arg_cong)
apply (clarsimp)
done
show ?thesis
apply (case_tac f)
apply (clarsimp)+
apply (clarsimp simp add: as_user_def)
apply (wp set_object_cte_wp_at2 | simp add: split_def)+
apply (clarsimp simp add: NC)
apply (clarsimp simp add: as_user_def)
apply (wp set_object_cte_wp_at2 | simp add: split_def)+
apply (clarsimp simp add: NC)
done
qed
lemma handle_fault_reply_has_no_reply_cap:
"\<lbrace>\<lambda>s. \<not>has_reply_cap t s\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. \<not>has_reply_cap t s\<rbrace>"
apply (clarsimp simp add: has_reply_cap_def)
apply (wp hoare_allI handle_fault_reply_cte_wp_at)
apply (clarsimp)
done
lemma do_reply_invs[wp]:
"\<lbrace>tcb_at t and tcb_at t' and cte_wp_at (op= (cap.ReplyCap t False)) slot and
invs\<rbrace>
do_reply_transfer t' t slot
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: do_reply_transfer_def)
apply (wp | wpc |simp)+
apply (wp sts_invs_minor)
apply (clarsimp)
apply (wp cap_delete_one_st_tcb_at)
apply (rule_tac Q="\<lambda>_. invs
and if_live_then_nonz_cap
and st_tcb_at awaiting_reply t
and (\<lambda>s. \<not>has_reply_cap t s)"
in hoare_strengthen_post [rotated])
apply (clarsimp)
apply (rule conjI, erule(1) st_tcb_ex_cap, clarsimp)
apply (rule conjI)
apply (clarsimp simp add: invs_def valid_state_def valid_idle_def)
apply (drule(1) st_tcb_at_eq)
apply (clarsimp)
apply (rule disjI1)
apply (erule st_tcb_weakenE)
apply (clarsimp)
apply (rule_tac Q="\<lambda>_. invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not>has_reply_cap t s)"
in hoare_strengthen_post [rotated], clarsimp)
apply (wp cap_delete_one_reply_st_tcb_at cap_delete_one_deletes_reply | simp)+
apply (rule_tac Q="\<lambda>_. valid_reply_caps and cte_wp_at (op = (cap.ReplyCap t False)) slot"
in hoare_strengthen_post [rotated], clarsimp)
apply (erule cte_wp_at_weakenE, simp)
apply (wp)
apply (rule do_ipc_transfer_non_null_cte_wp_at2, clarsimp)
apply (clarsimp simp:is_cap_simps)
apply (wp sts_invs_minor|simp split del: split_if)+
apply (wp sts_invs_minor thread_set_no_change_tcb_state)
apply (clarsimp)
apply (clarsimp)
apply (rule conjI)
apply (clarsimp)
apply (wp thread_set_cap_to thread_set_it |
clarsimp simp add: tcb_cap_cases_def)+
apply (rule_tac Q="\<lambda>_. invs
and st_tcb_at awaiting_reply t
and (\<lambda>s. \<not>has_reply_cap t s)"
in hoare_strengthen_post [rotated])
apply (clarsimp)
apply (erule st_tcb_weakenE)
apply (clarsimp)
apply (wp thread_set_invs_trivial thread_set_no_change_tcb_state
thread_set_has_no_reply_cap |
clarsimp simp add: tcb_cap_cases_def)+
apply (rule_tac Q="\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t
and invs
and st_tcb_at awaiting_reply t
and (\<lambda>s. \<not>has_reply_cap t s)"
in hoare_strengthen_post [rotated])
apply (clarsimp)
apply (rule conjI)
apply (erule(1) st_tcb_ex_cap' [where P=awaiting_reply])
apply (clarsimp)
apply (clarsimp simp add: invs_def valid_state_def valid_idle_def)
apply (drule(1) st_tcb_at_eq, clarsimp)
apply (wp handle_fault_reply_has_no_reply_cap)
apply (rule_tac Q="\<lambda>_. st_tcb_at awaiting_reply t and invs and (\<lambda>s. \<not>has_reply_cap t s)"
in hoare_strengthen_post [rotated])
apply (clarsimp)
apply (erule st_tcb_weakenE)
apply (clarsimp)
apply (wp cap_delete_one_deletes_reply cap_delete_one_reply_st_tcb_at)
apply (clarsimp)
apply (wp hoare_drop_imp hoare_allI)[1]
apply (wp assert_wp)
apply (clarsimp)
apply (rule_tac Q="\<lambda>rv. st_tcb_at (op = rv) t
and tcb_at t' and invs
and emptyable slot
and cte_wp_at (op = (cap.ReplyCap t False)) slot"
in hoare_strengthen_post [rotated])
apply (clarsimp simp add: st_tcb_at_tcb_at)
apply (rule conjI, erule st_tcb_weakenE, clarsimp)+
apply (clarsimp simp add: invs_def valid_state_def valid_pspace_def)
apply (rule conjI, erule st_tcb_weakenE, clarsimp)
apply (assumption)
apply (wp gts_sp)
apply (clarsimp)+
apply (erule emptyable_cte_wp_atD)
apply (clarsimp simp add: invs_def valid_state_def is_master_reply_cap_def)+
done
lemmas si_invs[wp] = si_invs'[where Q=\<top>,OF hoare_TrueI hoare_TrueI hoare_TrueI hoare_TrueI,simplified]
lemma pinv_invs[wp]:
"\<lbrace>invs and ct_active and valid_invocation i\<rbrace>
perform_invocation blocking call i \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (case_tac i, simp_all)
apply (wp tcbinv_invs invoke_domain_invs | clarsimp simp:ct_in_state_def
| erule st_tcb_ex_cap
| fastforce simp:ct_in_state_def | rule conjI)+
done
crunch typ_at[wp]: do_reply_transfer "\<lambda>s. P (typ_at T p s)"
(wp: hoare_drop_imps)
crunch typ_at[wp]: invoke_irq_control "\<lambda>s. P (typ_at T p s)"
crunch typ_at[wp]: invoke_irq_handler "\<lambda>s. P (typ_at T p s)"
lemma pinv_tcb[wp]:
"\<lbrace>invs and st_tcb_at active tptr and ct_active and
valid_invocation i\<rbrace>
perform_invocation blocking call i \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>"
apply (case_tac i, simp_all split:option.splits)
apply (wp | simp)+
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (wp tcb_at_typ_at)
apply simp
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (wp tcb_at_typ_at)
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (rule hoare_pre, wp)
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (rule hoare_pre, wp)
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (rule hoare_pre, wp)
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (simp add: tcb_at_typ, rule hoare_pre, wp)
apply (clarsimp simp: st_tcb_at_tcb_at tcb_at_typ[symmetric])
apply (simp add: tcb_at_typ, rule hoare_pre, wp)
apply (clarsimp simp: st_tcb_at_tcb_at tcb_at_typ[symmetric])
apply (wp invoke_arch_tcb)
apply (clarsimp simp: st_tcb_at_tcb_at)
done
lemmas sts_typ_at = set_thread_state_typ_at [where P="\<lambda>x. x"]
lemma cte_wp_cdt_lift:
assumes c: "\<And>P. \<lbrace>cte_wp_at P p\<rbrace> f \<lbrace>\<lambda>r. cte_wp_at P p\<rbrace>"
assumes m: "\<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> f \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>"
shows "\<lbrace>\<lambda>s. cte_wp_at (P (cdt s)) p s\<rbrace> f \<lbrace>\<lambda>r s. cte_wp_at (P (cdt s)) p s\<rbrace>"
apply (clarsimp simp add: valid_def)
apply (frule_tac P1="op = (cdt s)" in use_valid [OF _ m], rule refl)
apply simp
apply (erule use_valid [OF _ c])
apply simp
done
lemma sts_cte_wp_cdt [wp]:
"\<lbrace>\<lambda>s. cte_wp_at (P (cdt s)) p s\<rbrace>
set_thread_state t st
\<lbrace>\<lambda>rv s. cte_wp_at (P (cdt s)) p s\<rbrace>"
apply (rule cte_wp_cdt_lift)
apply wp
done
lemma sts_nasty_bit:
"\<lbrace>\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s
\<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace>
set_thread_state t st
\<lbrace>\<lambda>rv s. \<forall>r\<in>obj_refs cap. \<forall>a b. ptr' \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s
\<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap\<rbrace>"
apply (wp hoare_vcg_const_Ball_lift hoare_vcg_all_lift
hoare_vcg_imp_lift hoare_vcg_disj_lift valid_cte_at_neg_typ
| simp add: cte_wp_at_neg2[where P="\<lambda>c. x \<in> obj_refs c", standard])+
apply (clarsimp simp: o_def cte_wp_at_def)
done
crunch is_original_cap[wp]: set_thread_state "\<lambda>s. P (is_original_cap s)"
lemma sts_no_cap_asid[wp]:
"\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
set_thread_state t st
\<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
by (simp add: no_cap_to_obj_with_diff_ref_def
cte_wp_at_caps_of_state, wp)
lemma sts_valid_inv[wp]:
"\<lbrace>valid_invocation i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_invocation i\<rbrace>"
apply (case_tac i, simp_all add: aep_at_typ ep_at_typ
sts_valid_untyped_inv sts_valid_arch_inv)
apply (wp | simp)+
apply (case_tac tcb_invocation,
(wp set_thread_state_valid_cap|
simp add: tcb_at_typ split: option.split|
safe)+)
apply (case_tac cnode_invocation, simp_all)[1]
apply (case_tac cnode_invocation,
(wp set_thread_state_valid_cap sts_nasty_bit hoare_vcg_const_imp_lift
| simp)+)
apply (case_tac irq_control_invocation,
(wp | simp)+)
apply (case_tac irq_handler_invocation, simp_all)
apply (wp ex_cte_cap_to_pres hoare_vcg_ex_lift set_thread_state_valid_cap)
done
lemma sts_Restart_stay_simple:
"\<lbrace>st_tcb_at simple t\<rbrace>
set_thread_state t' Structures_A.Restart
\<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>"
apply (rule hoare_pre)
apply (wp sts_st_tcb_at_cases)
apply simp
done
lemma decode_inv_inv[wp]:
"\<lbrace>P\<rbrace> decode_invocation label args cap_index slot cap excaps \<lbrace>\<lambda>rv. P\<rbrace>"
apply (case_tac cap, simp_all add: decode_invocation_def)
apply (wp decode_tcb_inv_inv decode_domain_inv_inv | rule conjI | clarsimp
| simp split: bool.split)+
done
lemma diminished_Untyped [simp]:
"diminished (cap.UntypedCap x xa idx) = (\<lambda>c. c = cap.UntypedCap x xa idx)"
apply (rule ext)
apply (case_tac c,
auto simp: diminished_def cap_rights_update_def mask_cap_def)
done
lemma diminished_Reply [simp]:
"diminished (cap.ReplyCap x y) = (\<lambda>c. c = cap.ReplyCap x y)"
apply (rule ext)
apply (case_tac c,
auto simp: diminished_def cap_rights_update_def mask_cap_def)
done
lemma diminished_IRQHandler [simp]:
"diminished (cap.IRQHandlerCap irq) = (\<lambda>c. c = cap.IRQHandlerCap irq)"
apply (rule ext)
apply (case_tac c,
auto simp: diminished_def cap_rights_update_def mask_cap_def)
done
lemma cnode_diminished_strg:
"(\<exists>ptr. cte_wp_at (diminished cap) ptr s)
\<longrightarrow> (is_cnode_cap cap \<longrightarrow> (\<forall>ref \<in> cte_refs cap (interrupt_irq_node s).
ex_cte_cap_wp_to is_cnode_cap ref s))"
apply (clarsimp simp: ex_cte_cap_wp_to_def)
apply (intro exI, erule cte_wp_at_weakenE)
apply (clarsimp simp: diminished_def)
done
lemma obj_refs_cap_rights_update[simp]:
"obj_refs (cap_rights_update rs cap) = obj_refs cap"
by (simp add: cap_rights_update_def acap_rights_update_def
split: cap.split arch_cap.split)
(* FIXME: move to TCB *)
lemma table_cap_ref_mask_cap:
"table_cap_ref (mask_cap R cap) = table_cap_ref cap"
by (clarsimp simp add:mask_cap_def table_cap_ref_def acap_rights_update_def
cap_rights_update_def split:cap.splits arch_cap.splits)
lemma diminished_no_cap_to_obj_with_diff_ref:
"\<lbrakk> cte_wp_at (diminished cap) p s; valid_arch_caps s \<rbrakk>
\<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s"
apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def)
apply (frule(1) unique_table_refs_no_cap_asidD)
apply (clarsimp simp add: no_cap_to_obj_with_diff_ref_def
table_cap_ref_mask_cap diminished_def Ball_def)
done
lemma invs_valid_arch_caps[elim!]:
"invs s \<Longrightarrow> valid_arch_caps s"
by (clarsimp simp: invs_def valid_state_def)
lemma decode_inv_wf[wp]:
"\<lbrace>valid_cap cap and invs and cte_wp_at (diminished cap) slot
and ex_cte_cap_to 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 (interrupt_irq_node s). ex_cte_cap_to r s)
and (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_to r s)
and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile> (fst x))
and (\<lambda>s. \<forall>x \<in> set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s)
and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (diminished (fst x)) (snd x) s)
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 is_cnode_cap (snd x) s)
and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s)\<rbrace>
decode_invocation label args cap_index slot cap excaps
\<lbrace>valid_invocation\<rbrace>,-"
apply (simp add: decode_invocation_def
cong: cap.case_cong if_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp decode_tcb_inv_wf decode_domain_inv_wf[simplified split_def] | wpc |
simp add: o_def uncurry_def split_def del: is_cnode_cap.simps cte_refs.simps)+
apply (strengthen cnode_diminished_strg)
apply (clarsimp simp: valid_cap_def cte_wp_at_eq_simp is_cap_simps
cap_rights_update_def ex_cte_cap_wp_to_weakenE[OF _ TrueI]
cte_wp_at_caps_of_state
split: cap.splits)
apply (thin_tac " \<forall>x\<in>set excaps. ?P x & ?Q x")+
apply (drule (1) bspec)+
apply (subst split_paired_Ex[symmetric], rule exI, simp)
apply (thin_tac " \<forall>x\<in>set excaps. ?P x & ?Q x")+
apply (rule conjI)
apply (subst split_paired_Ex[symmetric], rule_tac x=slot in exI, simp)
apply clarsimp
apply (drule (1) bspec)+
apply (subst split_paired_Ex[symmetric], rule exI, simp)
apply (thin_tac " \<forall>x\<in>set excaps. ?P x & ?Q x")+
apply (drule (1) bspec)+
apply (clarsimp simp add: ex_cte_cap_wp_to_weakenE[OF _ TrueI])
apply (rule diminished_no_cap_to_obj_with_diff_ref)
apply (fastforce simp add: cte_wp_at_caps_of_state)
apply (simp add: invs_valid_arch_caps)
apply (simp add: invs_valid_objs invs_valid_global_refs)
apply (thin_tac " \<forall>x\<in>set excaps. ?P x & ?Q x")+
apply (rule conjI)
apply clarsimp
apply (drule (1) bspec)+
apply (subst split_paired_Ex[symmetric], rule exI, simp)
apply (clarsimp simp add: diminished_def mask_cap_def cap_rights_update_def
split: cap.splits)
apply (thin_tac " \<forall>x\<in>set excaps. ?P x & ?Q x")+
apply (subst split_paired_Ex[symmetric], rule exI, simp)
done
lemma lcs_valid [wp]:
"\<lbrace>invs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, -"
unfolding lookup_cap_and_slot_def
apply (rule hoare_pre)
apply (wp|clarsimp simp: split_def)+
done
lemma lec_valid_cap [wp]:
"\<lbrace>invs\<rbrace> lookup_extra_caps t xa mi \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. s \<turnstile> fst x)\<rbrace>, -"
unfolding lookup_extra_caps_def
apply simp
apply (wp mapME_set)
apply clarsimp
apply wp
done
lemma lcs_ex_cap_to [wp]:
"\<lbrace>invs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_to r s\<rbrace>, -"
unfolding lookup_cap_and_slot_def
apply (rule hoare_pre)
apply (wp | simp add: split_def)+
done
lemma lcs_ex_nonz_cap_to [wp]:
"\<lbrace>invs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s\<rbrace>, -"
unfolding lookup_cap_and_slot_def
apply (rule hoare_pre)
apply (wp | simp add: split_def)+
done
lemma lcs_cte_at[wp]:
"\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>rv. cte_at (snd rv)\<rbrace>,-"
apply (simp add: lookup_cap_and_slot_def split_def)
apply (rule hoare_pre)
apply (wp | simp)+
done
lemma lec_ex_cap_to [wp]:
"\<lbrace>invs\<rbrace>
lookup_extra_caps t xa mi
\<lbrace>\<lambda>rv s. (\<forall>cap \<in> set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_to r s)\<rbrace>, -"
unfolding lookup_extra_caps_def
by (wp mapME_set | simp)+
lemma lec_ex_nonz_cap_to [wp]:
"\<lbrace>invs\<rbrace>
lookup_extra_caps t xa mi
\<lbrace>\<lambda>rv s. (\<forall>cap \<in> set rv. \<forall>r\<in>zobj_refs (fst cap). ex_nonz_cap_to r s)\<rbrace>, -"
unfolding lookup_extra_caps_def
by (wp mapME_set | simp)+
lemma lookup_extras_real_ctes[wp]:
"\<lbrace>valid_objs\<rbrace> lookup_extra_caps t xs info \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. real_cte_at (snd x) s\<rbrace>,-"
apply (simp add: lookup_extra_caps_def
split del: split_if)
apply (rule hoare_pre)
apply (wp mapME_set)
apply (simp add: lookup_cap_and_slot_def split_def)
apply (wp option_cases_weak_wp mapM_wp'
| simp add: load_word_offs_word_def)+
done
lemma lookup_extras_ctes[wp]:
"\<lbrace>valid_objs\<rbrace> lookup_extra_caps t xs info \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. cte_at (snd x) s\<rbrace>,-"
apply (rule hoare_post_imp_R)
apply (rule lookup_extras_real_ctes)
apply (simp add: real_cte_at_cte)
done
lemma lsft_ex_cte_cap_to:
"\<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace>
lookup_slot_for_thread t cref
\<lbrace>\<lambda>rv s. ex_cte_cap_wp_to P (fst rv) s\<rbrace>,-"
apply (simp add: lookup_slot_for_thread_def)
apply (wp rab_cte_cap_to)
apply (clarsimp simp: ex_cte_cap_wp_to_def)
apply (clarsimp dest!: get_tcb_SomeD)
apply (frule cte_wp_at_tcbI[where t="(t', tcb_cnode_index 0)" and P="op = v", standard, simplified])
apply fastforce
apply fastforce
apply (intro exI, erule cte_wp_at_weakenE)
apply clarsimp
done
(* FIXME: move / generalize lemma in GenericLib *)
lemma mapME_wp:
assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>"
shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>"
apply (induct xs)
apply (simp add: mapME_def sequenceE_def)
apply wp
apply (simp add: mapME_Cons)
apply wp
apply simp
apply (simp add: x)
done
lemmas mapME_wp' = mapME_wp [OF _ subset_refl]
(* FIXME: move to CSpace_R *)
lemma resolve_address_bits_valid_fault:
"\<lbrace> valid_objs and valid_cap (fst param)\<rbrace>
resolve_address_bits param
\<lbrace>\<lambda>_. valid_objs\<rbrace>,
\<lbrace>\<lambda>f s. valid_fault (ExceptionTypes_A.fault.CapFault x y f)\<rbrace>"
unfolding resolve_address_bits_def
proof (induct param rule: resolve_address_bits'.induct)
case (1 cap cref)
show ?case
apply (clarsimp simp: validE_R_def validE_def valid_def split: sum.split)
apply (subst (asm) resolve_address_bits'.simps)
apply (split cap.splits)
defer 6 (* cnode *)
apply (simp_all add: spec_validE_def validE_def valid_def
throwError_def return_def valid_fault_def)[11]
apply (simp only: split: cap.splits split_if_asm)
apply (simp add: fail_def)
apply (simp only: K_bind_def in_bindE)
apply (elim conjE exE disjE)
apply ((clarsimp simp: whenE_def bindE_def bind_def lift_def liftE_def
throwError_def returnOk_def return_def valid_fault_def
valid_cap_def2 wellformed_cap_def
split: split_if_asm cap.splits)+)[4]
apply (split split_if_asm)
apply (clarsimp simp: whenE_def bindE_def bind_def lift_def liftE_def
throwError_def returnOk_def return_def valid_fault_def
valid_cap_def2 wellformed_cap_def
split: split_if_asm cap.splits)
apply (simp only: K_bind_def in_bindE)
apply (elim conjE exE disjE)
apply (clarsimp simp: whenE_def bindE_def bind_def lift_def liftE_def
throwError_def returnOk_def return_def valid_fault_def
valid_cap_def2 wellformed_cap_def
split: split_if_asm cap.splits)
apply (split split_if_asm)
apply (frule (8) "1.hyps")
apply (clarsimp simp add: validE_def valid_def whenE_def bindE_def
bind_def lift_def liftE_def throwError_def
returnOk_def return_def valid_fault_def
split: split_if_asm cap.splits sum.splits)
apply (frule in_inv_by_hoareD [OF get_cap_inv])
apply simp
apply (frule (1) post_by_hoare [OF get_cap_valid])
apply (erule_tac x=s in allE, erule impE, simp)
apply (drule (1) bspec, clarsimp)
apply (clarsimp simp add: returnOk_def return_def)
apply (frule in_inv_by_hoareD [OF get_cap_inv])
apply (clarsimp simp: whenE_def bindE_def bind_def throwError_def
returnOk_def return_def
split: split_if_asm cap.splits sum.splits)
done
qed
lemma resolve_address_bits_valid_fault2:
"\<lbrace>invs and valid_cap (fst param)\<rbrace>
resolve_address_bits param
-,\<lbrace>\<lambda>f s. valid_fault (ExceptionTypes_A.fault.CapFault x y f)\<rbrace>"
apply (cut_tac resolve_address_bits_valid_fault[of param x y])
apply (clarsimp simp add: validE_E_def validE_def valid_def
split: sum.splits)
apply (drule invs_valid_objs)
apply fastforce
done
lemma lookup_cap_and_slot_valid_fault:
"\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr
\<lbrace>\<lambda>_. valid_objs\<rbrace>,
\<lbrace>\<lambda>ft s. valid_fault (ExceptionTypes_A.CapFault (of_bl cptr) rp ft)\<rbrace>"
apply (simp add: lookup_cap_and_slot_def split_def lookup_slot_for_thread_def
| wp resolve_address_bits_valid_fault)+
apply (clarsimp simp: objs_valid_tcb_ctable)
done
lemma lookup_cap_and_slot_valid_fault2[wp]:
"\<lbrace>invs\<rbrace> lookup_cap_and_slot thread (to_bl p)
-,\<lbrace>\<lambda>ft s. valid_fault (ExceptionTypes_A.CapFault p rp ft)\<rbrace>"
using lookup_cap_and_slot_valid_fault[of thread "to_bl p"]
apply (clarsimp simp add: validE_E_def validE_def valid_def
split: sum.splits)
apply (drule invs_valid_objs)
apply fastforce
done
lemma lec_valid_fault:
"\<lbrace>valid_objs\<rbrace>
lookup_extra_caps thread buffer info
\<lbrace>\<lambda>_. valid_objs\<rbrace>,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>"
apply (simp add: lookup_extra_caps_def split del: split_if)
apply (wp mapME_wp' lookup_cap_and_slot_valid_fault)
done
lemma lec_valid_fault2[wp]:
"\<lbrace>invs\<rbrace> lookup_extra_caps thread buffer info -,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>"
apply (cut_tac lec_valid_fault[of thread buffer info])
apply (clarsimp simp add: validE_E_def validE_def valid_def
split: sum.splits )
apply (drule invs_valid_objs)
apply fastforce
done
lemma lec_caps_to[wp]:
"\<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> lookup_extra_caps t buffer info
\<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. ex_cte_cap_wp_to P (snd x) s)\<rbrace>,-"
apply (simp add: lookup_extra_caps_def split del: split_if)
apply (rule hoare_pre)
apply (wp mapME_set)
apply (simp add: lookup_cap_and_slot_def split_def)
apply (wp lsft_ex_cte_cap_to mapM_wp'
| simp add: load_word_offs_word_def | wpc)+
done
lemma get_cap_int_derived[wp]:
"\<lbrace>\<top>\<rbrace> get_cap slot \<lbrace>\<lambda>rv. cte_wp_at (interrupt_derived rv) slot\<rbrace>"
apply (wp get_cap_wp)
apply (clarsimp simp: cte_wp_at_caps_of_state interrupt_derived_def)
done
lemma lec_derived[wp]:
"\<lbrace>invs\<rbrace>
lookup_extra_caps t buffer info
\<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s)\<rbrace>,-"
apply (simp add: lookup_extra_caps_def split del: split_if)
apply (rule hoare_pre)
apply (wp mapME_set)
apply (simp add: lookup_cap_and_slot_def split_def)
apply (wp | simp)+
done
lemma lookup_cap_and_slot_dimished [wp]:
"\<lbrace>valid_objs\<rbrace>
lookup_cap_and_slot thread cptr
\<lbrace>\<lambda>x. cte_wp_at (diminished (fst x)) (snd x)\<rbrace>, -"
apply (simp add: lookup_cap_and_slot_def split_def)
apply (wp get_cap_wp)
apply (rule hoare_post_impErr
[where Q="\<lambda>_. valid_objs" and E="\<lambda>_. valid_objs"])
apply wp
apply simp
apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def)
apply (rule exI, rule cap_mask_UNIV[symmetric])
apply (drule (1) caps_of_state_valid_cap, simp add: valid_cap_def2)
apply simp
done
lemma lookup_extra_caps_diminished [wp]:
"\<lbrace>valid_objs\<rbrace> lookup_extra_caps thread xb info
\<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. cte_wp_at (diminished (fst x)) (snd x) s)\<rbrace>,-"
apply (simp add: lookup_extra_caps_def)
apply (wp mapME_set|simp)+
done
crunch tcb_at[wp]: reply_from_kernel "tcb_at t"
(simp: crunch_simps)
(*FIXME: move to NonDetMonadVCG.valid_validE_R *)
lemma valid_validE_R_gen:
"\<lbrakk>\<And>rv s. Q' (Inr rv) s \<Longrightarrow> Q rv s; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -"
by (fastforce simp: validE_R_def validE_def valid_def split_def)
lemma valid_validE_R_eq:
"\<lbrakk>Q = Q'\<circ>Inr; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -"
by (fastforce simp: validE_R_def validE_def valid_def split_def)
crunch tcb_at[wp]: reply_from_kernel "tcb_at t"
(simp: crunch_simps)
lemma ts_Restart_case_helper:
"(case ts of Structures_A.Restart \<Rightarrow> A | _ \<Rightarrow> B)
= (if ts = Structures_A.Restart then A else B)"
by (case_tac ts, simp_all)
crunch st_tcb[wp]: reply_from_kernel "st_tcb_at P t"
(simp: crunch_simps)
crunch cap_to[wp]: reply_from_kernel "ex_nonz_cap_to p"
(simp: crunch_simps)
crunch it[wp]: reply_from_kernel "\<lambda>s. P (idle_thread s)"
(simp: crunch_simps)
crunch cte_wp_at[wp]: reply_from_kernel "cte_wp_at P p"
(simp: crunch_simps)
lemma lcs_ex_cap_to2[wp]:
"\<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace>
lookup_cap_and_slot t cref \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (snd rv)\<rbrace>,-"
apply (rule hoare_pre)
apply (simp add: lookup_cap_and_slot_def split_def)
apply (wp lsft_ex_cte_cap_to | simp)+
done
lemma hoare_vcg_const_imp_lift_E[wp]:
"\<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. F \<longrightarrow> P s\<rbrace> f -, \<lbrace>\<lambda>rv s. F \<longrightarrow> Q rv s\<rbrace>"
apply (cases F) apply auto
apply wp
done
(* FIXME: move *)
lemmas validE_E_combs[wp_comb] =
hoare_vcg_E_conj[where Q'="\<top>\<top>", folded validE_E_def]
valid_validE_E
hoare_vcg_E_conj[where Q'="\<top>\<top>", folded validE_E_def, OF valid_validE_E]
lemma hinv_invs':
assumes perform_invocation_Q[wp]:
"\<And>block class i. \<lbrace>invs and Q and ct_active and valid_invocation i\<rbrace> perform_invocation block class i \<lbrace>\<lambda>_.Q\<rbrace>"
assumes handle_fault_Q[wp]:
"\<And>t f. \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and (\<lambda>_. valid_fault f)\<rbrace>
handle_fault t f
\<lbrace>\<lambda>r. Q\<rbrace>"
assumes reply_from_kernel_Q[wp]:
"\<And>a b. \<lbrace>invs and Q\<rbrace> reply_from_kernel a b \<lbrace>\<lambda>_.Q\<rbrace>"
assumes sts_Q[wp]:
"\<And>a b. \<lbrace>invs and Q\<rbrace> set_thread_state a b \<lbrace>\<lambda>_.Q\<rbrace>"
shows
"\<lbrace>invs and Q and ct_active\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>"
apply (simp add: handle_invocation_def ts_Restart_case_helper split_def
liftE_liftM_liftME liftME_def bindE_assoc)
apply (wp syscall_valid sts_invs_minor2 rfk_invs
hoare_vcg_all_lift hoare_vcg_disj_lift | simp split del: split_if)+
apply (rule_tac Q="\<lambda>st. st_tcb_at (op = st) thread and (invs and Q)"
in hoare_post_imp)
apply (auto elim!: st_tcb_weakenE st_tcb_ex_cap
dest: st_tcb_at_idle_thread
simp: st_tcb_at_tcb_at)[1]
apply (rule gts_sp)
apply wp
apply (simp add: ct_in_state_def conj_ac)
apply wp
apply (rule_tac Q="\<lambda>rv s. st_tcb_at active thread s \<and>
cur_thread s = thread" in hoare_post_imp)
apply simp
apply (wp sts_st_tcb_at')
apply (simp only: simp_thms K_def if_apply_def2)
apply (rule hoare_vcg_E_elim)
apply (wp | simp add: if_apply_def2)+
apply (auto simp: ct_in_state_def elim: st_tcb_ex_cap)
done
lemmas hinv_invs[wp] = hinv_invs'[where Q=\<top>,simplified hoare_post_taut, OF TrueI TrueI TrueI TrueI,simplified]
(* FIXME: move *)
lemma hinv_tcb[wp]:
"\<lbrace>st_tcb_at active t and invs and ct_active\<rbrace>
handle_invocation calling blocking
\<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
apply (simp add: handle_invocation_def split_def
ts_Restart_case_helper
liftE_liftM_liftME liftME_def bindE_assoc)
apply (wp syscall_valid sts_st_tcb_at_cases
ct_in_state_set lec_caps_to
| simp)+
apply (clarsimp simp: st_tcb_at_tcb_at invs_valid_objs
ct_in_state_def)
apply (fastforce elim!: st_tcb_ex_cap)
done
lemma hs_tcb_on_err:
"\<lbrace>st_tcb_at active t and invs and ct_active\<rbrace>
handle_send blocking
-,\<lbrace>\<lambda>e. tcb_at t\<rbrace>"
apply (unfold handle_send_def whenE_def fun_app_def validE_E_def validE_def)
apply (rule hoare_strengthen_post [OF hinv_tcb])
apply (clarsimp split: sum.split)
done
lemma hs_invs[wp]: "\<lbrace>invs and ct_active\<rbrace> handle_send blocking \<lbrace>\<lambda>r. invs\<rbrace>"
apply (rule validE_valid)
apply (simp add: handle_send_def whenE_def)
apply (wp | simp add: ct_in_state_def tcb_at_invs)+
done
lemma tcb_cnode_index_3_reply_or_null:
"\<lbrakk> tcb_at t s; tcb_cap_valid cap (t, tcb_cnode_index 3) s \<rbrakk> \<Longrightarrow> is_reply_cap cap \<or> cap = cap.NullCap"
apply (clarsimp simp: tcb_cap_valid_def st_tcb_def2 tcb_at_def)
apply (clarsimp split: Structures_A.thread_state.split_asm)
done
lemma ex_nonz_cap_to_tcb_strg:
"(\<exists>cref. cte_wp_at (\<lambda>cap. is_thread_cap cap \<and> p \<in> zobj_refs cap) cref s)
\<longrightarrow> ex_nonz_cap_to p s"
by (fastforce simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state)
lemma ex_tcb_cap_to_tcb_at_strg:
"ex_nonz_cap_to p s \<and> tcb_at p s \<and> valid_objs s \<longrightarrow>
(\<exists>cref. cte_wp_at (\<lambda>cap. is_thread_cap cap \<and> p \<in> zobj_refs cap) cref s)"
apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state
zobj_refs_to_obj_refs)
apply (drule(1) caps_of_state_valid_cap[rotated])
apply (drule(2) valid_cap_tcb_at_tcb_or_zomb)
apply fastforce
done
lemma delete_caller_cap_nonz_cap:
"\<lbrace>ex_nonz_cap_to p and tcb_at p and valid_objs\<rbrace>
delete_caller_cap t
\<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>"
apply (simp add: delete_caller_cap_def)
apply (strengthen ex_nonz_cap_to_tcb_strg)
apply (wp hoare_vcg_ex_lift cap_delete_one_cte_wp_at_preserved)
apply (clarsimp simp: is_cap_simps can_fast_finalise_def)
apply (strengthen ex_tcb_cap_to_tcb_at_strg)
apply simp
done
lemma delete_caller_cap_invs[wp]:
"\<lbrace>invs and tcb_at t\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: delete_caller_cap_def, wp)
apply (clarsimp simp: emptyable_def)
done
lemma delete_caller_cap_simple[wp]:
"\<lbrace>st_tcb_at active t\<rbrace> delete_caller_cap t' \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace>"
apply (simp add: delete_caller_cap_def)
apply (wp cap_delete_one_st_tcb_at)
apply simp
done
lemma delete_caller_deletes_caller[wp]:
"\<lbrace>\<top>\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. cte_wp_at (op = cap.NullCap) (t, tcb_cnode_index 3)\<rbrace>"
apply (rule_tac Q="\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 3)"
in hoare_post_imp,
clarsimp elim!: cte_wp_at_weakenE)
apply (simp add: delete_caller_cap_def cap_delete_one_def, wp)
apply (clarsimp simp add: split_if unless_def when_def)
apply (rule conjI [rotated], clarsimp, wp)
apply (clarsimp elim!: cte_wp_at_weakenE | wp get_cap_wp)+
done
lemma delete_caller_cap_deleted[wp]:
"\<lbrace>\<top>\<rbrace> delete_caller_cap thread \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) (thread, tcb_cnode_index 3)\<rbrace>"
by (simp add: delete_caller_cap_def, wp)
lemma invs_valid_tcb_ctable_strengthen:
"invs s \<longrightarrow> ((\<exists>y. get_tcb thread s = Some y) \<longrightarrow>
invs s \<and> s \<turnstile> tcb_ctable (the (get_tcb thread s)))"
by (clarsimp simp: invs_valid_tcb_ctable)
lemma hw_invs[wp]: "\<lbrace>invs and ct_active\<rbrace> handle_wait \<lbrace>\<lambda>r. invs\<rbrace>"
apply (simp add: handle_wait_def Let_def ep_aep_cap_case_helper
cong: if_cong)
apply (wp hoare_drop_imps delete_caller_cap_nonz_cap | simp)+
apply (rule hoare_vcg_E_elim)
apply (simp add: lookup_cap_def lookup_slot_for_thread_def)
apply wp
apply (simp add: split_def)
apply (wp resolve_address_bits_valid_fault2)