-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathFinalise_AC.thy
1314 lines (1158 loc) · 57.8 KB
/
Finalise_AC.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory Finalise_AC
imports ArchArch_AC
begin
text \<open>
NB: the @{term is_subject} assumption is not appropriate for some of
the scheduler lemmas. This is because a scheduler domain may have
threads from multiple labels, hence the thread being acted upon
might not be in the same label as the current subject.
In some of the scheduling lemmas, we replace the @{term is_subject}
assumption with a statement that the scheduled thread is in one of
the current subject's domains.
\<close>
locale Finalise_AC_1 =
fixes aag :: "'a PAS"
assumes sbn_st_vrefs:
"\<And>P. \<lbrace>(\<lambda>s. P (state_vrefs s)) and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
set_bound_notification ref ntfn
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
and arch_finalise_cap_auth':
"\<lbrace>pas_refined aag\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>"
and arch_finalise_cap_obj_refs:
"\<And>P. \<lbrace>\<lambda>_ :: det_ext state. \<forall>x \<in> aobj_ref' acap. P x\<rbrace>
arch_finalise_cap acap slot
\<lbrace>\<lambda>rv _. \<forall>x \<in> obj_refs_ac (fst rv). P x\<rbrace>"
and prepare_thread_delete_st_tcb_at_halted[wp]:
"prepare_thread_delete t \<lbrace>\<lambda>s :: det_ext state. st_tcb_at halted t s\<rbrace>"
and arch_finalise_cap_makes_halted:
"\<lbrace>\<top>\<rbrace> arch_finalise_cap acap ex \<lbrace>\<lambda>rv s :: det_ext state. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>"
and arch_cap_cleanup_wf:
"\<lbrakk> arch_cap_cleanup_opt acap \<noteq> NullCap; \<not> is_arch_cap (arch_cap_cleanup_opt acap) \<rbrakk>
\<Longrightarrow> (\<exists>irq. arch_cap_cleanup_opt acap = IRQHandlerCap irq \<and> is_subject_irq aag irq)"
and finalise_cap_valid_list[wp]:
"finalise_cap param_a param_b \<lbrace>valid_list\<rbrace>"
and arch_finalise_cap_pas_refined[wp]:
"\<lbrace>pas_refined aag and invs and valid_arch_cap acap\<rbrace>
arch_finalise_cap acap ex
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
and prepare_thread_delete_pas_refined[wp]:
"prepare_thread_delete p \<lbrace>pas_refined aag\<rbrace>"
and prepare_thread_delete_respects[wp]:
"prepare_thread_delete p \<lbrace>integrity aag X st\<rbrace>"
and finalise_cap_replaceable:
"\<lbrace>\<lambda>s :: det_ext state. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s \<and>
cte_wp_at ((=) cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and>
(cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and>
(is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and>
valid_arch_state s \<and> valid_arch_caps s)\<rbrace>
finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>"
and arch_finalise_cap_respects[wp]:
"\<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (ArchObjectCap acap)
and K (pas_cap_cur_auth aag (ArchObjectCap acap))\<rbrace>
arch_finalise_cap acap final
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
and arch_post_cap_deletion[wp]:
"arch_post_cap_deletion acap \<lbrace>\<lambda>s :: det_ext state. pspace_aligned s\<rbrace>"
and arch_post_cap_deletion_valid_vspace_objs[wp]:
"arch_post_cap_deletion acap \<lbrace>\<lambda>s :: det_ext state. valid_vspace_objs s\<rbrace>"
and arch_post_cap_deletion_valid_arch_state[wp]:
"arch_post_cap_deletion acap \<lbrace>\<lambda>s :: det_ext state. valid_arch_state s\<rbrace>"
begin
lemma tcb_sched_action_dequeue_integrity':
"\<lbrace>integrity aag X st and pas_refined aag and
(\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (wpsimp simp: tcb_sched_action_def)
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
split: option.splits)
done
lemma tcb_sched_action_dequeue_integrity[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag thread)\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
split: option.splits)
apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
apply (auto intro: domtcbs)
done
lemma tcb_sched_action_enqueue_integrity[wp]:
"tcb_sched_action tcb_sched_enqueue thread \<lbrace>integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def tcb_at_def get_etcb_def
tcb_sched_enqueue_def etcb_at_def
split: option.splits)
apply (metis append.simps(2))
done
text \<open>See comment for @{thm tcb_sched_action_dequeue_integrity'}\<close>
lemma tcb_sched_action_append_integrity':
"\<lbrace>integrity aag X st and
(\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\<rbrace>
tcb_sched_action tcb_sched_append thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def etcb_at_def
split: option.splits)
done
lemma tcb_sched_action_append_integrity[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag thread)\<rbrace>
tcb_sched_action tcb_sched_append thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
split: option.splits)
apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
apply (auto intro: domtcbs)
done
lemma tcb_sched_action_append_integrity_pasMayEditReadyQueues:
"\<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace>
tcb_sched_action tcb_sched_append thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def split: option.splits)
done
lemma reschedule_required_integrity[wp]:
"reschedule_required \<lbrace>integrity aag X st\<rbrace>"
apply (simp add: integrity_def reschedule_required_def)
apply (wp | wpc)+
apply simp
done
lemma cancel_badged_sends_respects[wp]:
"\<lbrace>integrity aag X st and einvs and valid_objs
and (sym_refs \<circ> state_refs_of)
and K (aag_has_auth_to aag Reset epptr)\<rbrace>
cancel_badged_sends epptr badge
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: cancel_badged_sends_def filterM_mapM
cong: endpoint.case_cong)
apply (wp set_endpoint_respects | wpc | simp)+
apply (rule mapM_mapM_x_valid[THEN iffD1])
apply (simp add: exI[where x=Reset])
apply (rule mapM_x_inv_wp2
[where V="\<lambda>q s. distinct q \<and> (\<forall>x \<in> set q. st_tcb_at (blocked_on epptr) x s)"
and Q="P" and I="P" for P])
apply simp
apply (simp add: bind_assoc)
apply (rule bind_wp[OF _ gts_sp])
apply (rule hoare_pre)
apply (wp sts_respects_restart_ep hoare_vcg_const_Ball_lift sts_st_tcb_at_neq)
apply clarsimp
apply fastforce
apply (wp set_endpoint_respects hoare_vcg_const_Ball_lift get_simple_ko_wp)+
apply clarsimp
apply (frule(1) sym_refs_ko_atD)
apply (frule ko_at_state_refs_ofD)
apply (rule obj_at_valid_objsE, assumption, assumption)
apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_def2)
apply (clarsimp simp: obj_at_def is_ep valid_obj_def valid_ep_def)
apply auto
done
lemma cancel_all_ipc_respects [wp]:
"\<lbrace>integrity aag X st and valid_objs and (sym_refs \<circ> state_refs_of)
and K (\<exists>auth. aag_has_auth_to aag Reset epptr)\<rbrace>
cancel_all_ipc epptr
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (clarsimp simp: cancel_all_ipc_def get_ep_queue_def cong: endpoint.case_cong)
apply (wp mapM_x_inv_wp2
[where I="integrity aag X st"
and V="\<lambda>q s. distinct q \<and> (\<forall>x \<in> set q. st_tcb_at (blocked_on epptr) x s)"]
sts_respects_restart_ep sts_st_tcb_at_neq hoare_vcg_ball_lift
set_endpoint_respects get_simple_ko_wp
| wpc | clarsimp | blast)+
apply (frule ko_at_state_refs_ofD)
apply (rule obj_at_valid_objsE, assumption, assumption)
apply (rename_tac ep ko)
apply (subgoal_tac "\<forall>x \<in> ep_q_refs_of ep. st_tcb_at (blocked_on epptr) (fst x) s")
apply (fastforce simp: valid_obj_def valid_ep_def obj_at_def is_ep_def
split: endpoint.splits)
apply clarsimp
apply (erule (1) ep_queued_st_tcb_at')
apply simp_all
done
end
crunch blocked_cancel_ipc, cancel_signal
for pas_refined[wp]: "pas_refined aag"
crunch reschedule_required
for tcb_domain_map_wellformed[wp]: "tcb_domain_map_wellformed aag"
(* FIXME move to AInvs *)
lemma tcb_sched_action_ekheap[wp]:
"tcb_sched_action p1 p2 \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (simp add: etcb_at_def)
done
(* FIXME move to CNode *)
lemma scheduler_action_update_pas_refined[simp]:
"pas_refined aag (scheduler_action_update (\<lambda>_. param_a) s) = pas_refined aag s"
by (simp add: pas_refined_def)
lemma set_bound_notification_ekheap[wp]:
"set_bound_notification t st \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (wp set_scheduler_action_wp | simp)+
done
lemma sbn_thread_st_auth[wp]:
"set_bound_notification t ntfn \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp dxo_wp_weak)
apply (clarsimp simp: get_tcb_def thread_st_auth_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext])
done
crunch fast_finalise
for valid_mdb[wp]: "valid_mdb :: det_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps)
crunch fast_finalise
for valid_objs[wp]: "valid_objs :: det_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps)
context Finalise_AC_1 begin
lemma sbn_pas_refined[wp]:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
K (case ntfn of None \<Rightarrow> True
| Some ntfn' \<Rightarrow> \<forall>auth \<in> {Receive, Reset}. abs_has_auth_to aag auth t ntfn')\<rbrace>
set_bound_notification t ntfn
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: pas_refined_def state_objs_to_policy_def)
apply (rule hoare_pre)
apply (wp tcb_domain_map_wellformed_lift sbn_st_vrefs | wps)+
apply (clarsimp dest!: auth_graph_map_memD)
apply (erule state_bits_to_policy.cases)
by (auto intro: state_bits_to_policy.intros auth_graph_map_memI
split: if_split_asm)
lemma unbind_notification_pas_refined[wp]:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
unbind_notification tptr
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (clarsimp simp: unbind_notification_def)
apply (wp set_simple_ko_pas_refined hoare_drop_imps | wpc | simp)+
done
lemma unbind_maybe_notification_pas_refined[wp]:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
unbind_maybe_notification nptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (clarsimp simp: unbind_maybe_notification_def)
apply (wp set_simple_ko_pas_refined hoare_drop_imps | wpc | simp)+
done
lemma cancel_all_ipc_pas_refined[wp]:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
cancel_all_ipc epptr
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (clarsimp simp: cancel_all_ipc_def get_ep_queue_def cong: endpoint.case_cong)
apply (rule_tac Q'="\<lambda>_. pas_refined aag and pspace_aligned
and valid_vspace_objs
and valid_arch_state"
in hoare_strengthen_post)
apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+
done
lemma cancel_all_signals_pas_refined[wp]:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and
valid_arch_state\<rbrace>
cancel_all_signals ntfnptr
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (clarsimp simp: cancel_all_signals_def cong: ntfn.case_cong)
apply (rule_tac Q'="\<lambda>_. pas_refined aag and pspace_aligned
and valid_vspace_objs
and valid_arch_state"
in hoare_strengthen_post)
apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+
done
crunch unbind_maybe_notification, cancel_all_ipc, cancel_all_signals,
fast_finalise, blocked_cancel_ipc, cap_move
for pspace_aligned[wp]: pspace_aligned
and valid_vspace_objs[wp]: valid_vspace_objs
and valid_arch_state[wp]: valid_arch_state
(ignore: cap_move_ext tcb_sched_action reschedule_required wp: dxo_wp_weak mapM_x_inv_wp)
crunch cap_delete_one
for pas_refined_transferable[wp_transferable]: "pas_refined aag"
and pas_refined[wp, wp_not_transferable]: "pas_refined aag"
(wp: crunch_wps simp: crunch_simps)
end
(* FIXME MOVE next to thread_set_tcb_fault_set_invs in DetSchedSchedule *)
lemma thread_set_tcb_fault_reset_invs:
"thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>invs\<rbrace>"
by (rule thread_set_invs_trivial) (clarsimp simp: ran_tcb_cap_cases)+
(* FIXME MOVE next to IpcCancel_AI.reply_cap_descends_from_master *)
lemma reply_cap_descends_from_master0:
"\<lbrakk> invs s; tcb_at t s \<rbrakk>
\<Longrightarrow> \<forall>sl\<in>descendants_of (t, tcb_cnode_index 2) (cdt s).
\<exists>R. caps_of_state s sl = Some (ReplyCap t False R)"
apply (subgoal_tac "cte_wp_at (\<lambda>c. (is_master_reply_cap c \<and> obj_ref_of c = t) \<or> c = NullCap)
(t, tcb_cnode_index 2) s")
apply (clarsimp simp: invs_def valid_state_def valid_mdb_def2 is_cap_simps
valid_reply_caps_def cte_wp_at_caps_of_state)
apply (erule disjE)
apply (unfold reply_mdb_def reply_masters_mdb_def)[1]
apply (elim conjE)
apply (erule_tac x="(t, tcb_cnode_index 2)" in allE)
apply (erule_tac x=t in allE)+
apply (fastforce simp: unique_reply_caps_def is_cap_simps)
apply (fastforce dest: mdb_cte_at_Null_descendants)
apply (clarsimp simp: tcb_cap_wp_at invs_valid_objs
tcb_cap_cases_def is_cap_simps)
done
context Finalise_AC_1 begin
lemma reply_cancel_ipc_pas_refined[wp]:
"\<lbrace>pas_refined aag and invs and tcb_at t and K (is_subject aag t)\<rbrace>
reply_cancel_ipc t
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: reply_cancel_ipc_def)
apply (wp add: wp_transferable del: wp_not_transferable)
apply (rule hoare_strengthen_post[where Q'="\<lambda>_. invs and tcb_at t and pas_refined aag"])
apply (wpsimp wp: hoare_wp_combs thread_set_tcb_fault_reset_invs thread_set_pas_refined)+
apply (frule(1) reply_cap_descends_from_master0)
apply (fastforce simp: cte_wp_at_caps_of_state intro:it_Reply)
apply fastforce
done
lemma deleting_irq_handler_pas_refined[wp]:
"\<lbrace>pas_refined aag and invs and K (is_subject_irq aag irq)\<rbrace>
deleting_irq_handler irq
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: deleting_irq_handler_def get_irq_slot_def)
apply wp
apply (fastforce simp: pas_refined_def irq_map_wellformed_aux_def)
done
crunch suspend
for pspace_aligned[wp]: "\<lambda>s :: det_ext state. pspace_aligned s"
and valid_vspace_objs[wp]: "\<lambda>s :: det_ext state. valid_vspace_objs s"
and valid_arch_state[wp]: "\<lambda>s :: det_ext state. valid_arch_state s"
(wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps simp: tcb_cap_cases_def)
crunch suspend
for pas_refined[wp]: "pas_refined aag"
lemma finalise_cap_pas_refined[wp]:
"\<lbrace>pas_refined aag and invs and valid_cap cap and K (pas_cap_cur_auth aag cap)\<rbrace>
finalise_cap cap fin
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (cases cap; simp only: finalise_cap.simps)
apply (wpsimp wp: unbind_notification_invs
simp: aag_cap_auth_def cap_auth_conferred_def valid_cap_simps
cap_links_irq_def pas_refined_Control[symmetric]
| strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+
done
lemma cancel_all_signals_respects[wp]:
"\<lbrace>integrity aag X st and valid_objs and (sym_refs \<circ> state_refs_of)
and K (aag_has_auth_to aag Reset epptr)\<rbrace>
cancel_all_signals epptr
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (clarsimp simp add: cancel_all_signals_def)
apply (rule bind_wp[OF _ get_simple_ko_sp], rule hoare_pre)
apply (wp mapM_x_inv_wp2
[where I="integrity aag X st"
and V="\<lambda>q s. distinct q \<and> (\<forall>x \<in> set q. st_tcb_at (blocked_on epptr) x s)"]
sts_respects_restart_ep sts_st_tcb_at_neq hoare_vcg_ball_lift set_ntfn_respects
| wpc | clarsimp | blast)+
apply (frule sym_refs_ko_atD, clarsimp+)
apply (rule obj_at_valid_objsE, assumption, assumption)
apply (clarsimp simp: valid_obj_def valid_ntfn_def st_tcb_at_refs_of_rev st_tcb_def2
split: option.splits)
apply fastforce+
done
end
lemma sbn_unbind_respects[wp]:
"\<lbrace>integrity aag X st and
(\<lambda>s. (\<exists>ntfn. bound_tcb_at (\<lambda>a. a = Some ntfn) t s \<and> aag_has_auth_to aag Reset ntfn))\<rbrace>
set_bound_notification t None
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def pred_tcb_at_def integrity_asids_kh_upds)
apply (rule tro_tcb_unbind)
apply (fastforce dest!: get_tcb_SomeD)
apply (fastforce dest!: get_tcb_SomeD)
apply simp
apply (simp add: tcb_bound_notification_reset_integrity_def)
done
lemma bound_tcb_at_thread_bound_ntfns:
"bound_tcb_at ((=) ntfn) t s \<Longrightarrow> thread_bound_ntfns s t = ntfn"
by (clarsimp simp: thread_bound_ntfns_def pred_tcb_at_def obj_at_def get_tcb_def
split: option.splits)
lemma bound_tcb_at_implies_receive:
"\<lbrakk> pas_refined aag s; bound_tcb_at ((=) (Some x)) t s \<rbrakk>
\<Longrightarrow> abs_has_auth_to aag Receive t x"
by (fastforce dest!: bound_tcb_at_thread_bound_ntfns sta_bas pas_refined_mem)
lemma bound_tcb_at_implies_reset:
"\<lbrakk> pas_refined aag s; bound_tcb_at ((=) (Some x)) t s \<rbrakk>
\<Longrightarrow> abs_has_auth_to aag Reset t x"
by (fastforce dest!: bound_tcb_at_thread_bound_ntfns sta_bas pas_refined_mem)
lemma unbind_notification_respects:
"\<lbrace>integrity aag X st and pas_refined aag and
bound_tcb_at (\<lambda>a. case a of None \<Rightarrow> True | Some ntfn \<Rightarrow> aag_has_auth_to aag Reset ntfn) t\<rbrace>
unbind_notification t
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (clarsimp simp: unbind_notification_def)
apply (rule bind_wp[OF _ gbn_sp])
apply (wp set_ntfn_respects hoare_vcg_ex_lift gbn_wp | wpc | simp)+
apply (clarsimp simp: pred_tcb_at_def obj_at_def split: option.splits)
apply blast
done
lemma unbind_maybe_notification_respects:
"\<lbrace>integrity aag X st and invs and pas_refined aag and
obj_at (\<lambda>ko. \<exists>ntfn. ko = (Notification ntfn) \<and>
(case (ntfn_bound_tcb ntfn) of None \<Rightarrow> True
| Some t \<Rightarrow> aag_has_auth_to aag Reset a)) a\<rbrace>
unbind_maybe_notification a
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (clarsimp simp: unbind_maybe_notification_def)
apply (rule hoare_pre)
apply (wp set_ntfn_respects get_simple_ko_wp hoare_vcg_ex_lift gbn_wp | wpc | simp)+
apply clarsimp
apply (frule_tac P="\<lambda>ntfn. ntfn = Some a"
in ntfn_bound_tcb_at[OF invs_sym_refs invs_valid_objs], (simp add: obj_at_def)+)
apply (auto simp: pred_tcb_at_def obj_at_def split: option.splits)
done
context Finalise_AC_1 begin
lemma fast_finalise_respects[wp]:
"\<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap cap
and K (pas_cap_cur_auth aag cap)\<rbrace>
fast_finalise cap fin
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (cases cap; simp)
apply (wpsimp wp: unbind_maybe_notification_valid_objs get_simple_ko_wp
unbind_maybe_notification_respects
simp: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def when_def
| fastforce)+
apply (clarsimp simp: obj_at_def valid_cap_def is_ntfn invs_def valid_state_def valid_pspace_def
split: option.splits)+
apply (wp, simp)
done
lemma cap_delete_one_respects[wp,wp_not_transferable]:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))\<rbrace>
cap_delete_one slot
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: cap_delete_one_def unless_def bind_assoc)
apply (wpsimp wp: hoare_drop_imps get_cap_auth_wp [where aag = aag])
apply (fastforce simp: caps_of_state_valid)
done
end
lemma fast_finalise_is_transferable[wp_transferable]:
"\<lbrace>P and K (is_transferable (Some cap))\<rbrace>
fast_finalise cap final
\<lbrace>\<lambda>_. P\<rbrace>"
by (rule hoare_gen_asm) (erule is_transferable.cases; simp)
lemma cap_delete_one_respects_transferable[wp_transferable]:
"\<lbrace>integrity aag X st and pas_refined aag and einvs
and cte_wp_at (\<lambda>c. is_transferable (Some c)) slot
and cdt_change_allowed' aag slot\<rbrace>
cap_delete_one slot
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: cap_delete_one_def unless_def bind_assoc)
apply (wp add: hoare_drop_imps get_cap_wp wp_transferable del: wp_not_transferable | simp)+
apply (fastforce simp: caps_of_state_valid cte_wp_at_caps_of_state)
done
lemma thread_set_tcb_state_trivial:
"(\<And>tcb. tcb_state (f tcb) = tcb_state tcb)
\<Longrightarrow> thread_set f t \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace>"
apply (simp add: thread_set_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD)
by (auto simp: tcb_states_of_state_def get_tcb_def)
lemma reply_cancel_ipc_respects[wp]:
"\<lbrace>integrity aag X st and einvs and tcb_at t and K (is_subject aag t) and pas_refined aag\<rbrace>
reply_cancel_ipc t
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: reply_cancel_ipc_def)
apply (rule hoare_pre)
apply (wp add: wp_transferable del:wp_not_transferable)
apply simp
apply (rule hoare_lift_Pf2[where f="cdt"])
apply (wpsimp wp: hoare_vcg_const_Ball_lift thread_set_integrity_autarch
thread_set_invs_trivial[OF ball_tcb_cap_casesI] thread_set_tcb_state_trivial
thread_set_not_state_valid_sched hoare_weak_lift_imp thread_set_cte_wp_at_trivial
thread_set_pas_refined
simp: ran_tcb_cap_cases)+
apply (strengthen invs_psp_aligned invs_vspace_objs invs_arch_state, clarsimp)
apply (rule conjI)
apply (fastforce simp: cte_wp_at_caps_of_state intro:is_transferable.intros
dest!: reply_cap_descends_from_master0)
apply (rule cdt_change_allowed_all_children[where aag=aag, THEN all_children_descendants_of])
by fastforce+
lemma cancel_signal_respects[wp]:
"\<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag t \<and>
(\<exists>auth. aag_has_auth_to aag auth ntfnptr \<and> (auth = Receive \<or> auth = Notify))\<rbrace>
cancel_signal t ntfnptr
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: cancel_signal_def)
apply (rule bind_wp[OF _ get_simple_ko_sp])
apply (rule hoare_pre)
apply (wp set_thread_state_integrity_autarch set_ntfn_respects | wpc | fastforce)+
done
lemma cancel_ipc_respects[wp]:
"\<lbrace>integrity aag X st and einvs and tcb_at t and K (is_subject aag t) and pas_refined aag\<rbrace>
cancel_ipc t
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: cancel_ipc_def)
apply (rule bind_wp[OF _ gts_sp])
apply (rule hoare_pre)
apply (wp set_thread_state_integrity_autarch set_endpoint_respects get_simple_ko_wp
| wpc
| simp (no_asm) add: blocked_cancel_ipc_def get_ep_queue_def get_blocking_object_def)+
apply clarsimp
apply (frule st_tcb_at_to_thread_st_auth, clarsimp+)
apply (fastforce simp: obj_at_def is_ep_def dest: pas_refined_mem[OF sta_ts_mem])
done
lemma update_restart_pc_integrity_autarch[wp]:
"\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace>
update_restart_pc t
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: get_thread_state_def thread_get_def update_restart_pc_def)
apply (wpsimp wp: as_user_integrity_autarch)
done
context Finalise_AC_1 begin
lemma suspend_respects[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and tcb_at t and K (is_subject aag t)\<rbrace>
suspend t
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: suspend_def)
apply (wp set_thread_state_integrity_autarch set_thread_state_pas_refined)
apply (rule hoare_conjI)
apply (wp hoare_drop_imps)+
apply wpsimp+
apply fastforce
done
end
lemma finalise_is_fast_finalise:
"can_fast_finalise cap
\<Longrightarrow> finalise_cap cap fin = do fast_finalise cap fin; return (NullCap, NullCap) od"
by (cases cap, simp_all add: can_fast_finalise_def liftM_def)
lemma get_irq_slot_owns[wp]:
"\<lbrace>pas_refined aag and K (is_subject_irq aag irq)\<rbrace>
get_irq_slot irq
\<lbrace>\<lambda>rv _. is_subject aag (fst rv)\<rbrace>"
unfolding get_irq_slot_def
apply wp
apply (rule pas_refined_Control [symmetric])
apply (clarsimp simp: pas_refined_def irq_map_wellformed_aux_def aag_wellformed_refl)
apply fastforce
done
lemma pas_refined_Control_into_is_subject_asid:
"\<lbrakk> pas_refined aag s; (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag \<rbrakk>
\<Longrightarrow> is_subject_asid aag asid"
apply (drule (1) pas_refined_Control)
apply (blast intro: sym)
done
context Finalise_AC_1 begin
lemma finalise_cap_respects[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and valid_cap cap
and K (pas_cap_cur_auth aag cap)\<rbrace>
finalise_cap cap final
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (cases cap; simp; safe?;
(solves \<open>(wp | simp add: if_apply_def2 split del: if_split
| clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def is_cap_simps
pas_refined_all_auth_is_owns aag_cap_auth_def
deleting_irq_handler_def cap_links_irq_def invs_valid_objs
split del: if_split
elim!: pas_refined_Control [symmetric])+\<close>)?)
(*NTFN Cap*)
apply ((wp unbind_maybe_notification_valid_objs get_simple_ko_wp
unbind_maybe_notification_respects
| wpc
| simp add: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def
split: if_split_asm
| fastforce)+;
clarsimp simp: obj_at_def valid_cap_def is_ntfn invs_def
valid_state_def valid_pspace_def
split: option.splits)
(* tcb cap *)
apply (wp unbind_notification_respects unbind_notification_invs
| clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def
unbind_maybe_notification_def
elim!: pas_refined_Control[symmetric]
| simp add: if_apply_def2 split del: if_split )+
apply (clarsimp simp: valid_cap_def pred_tcb_at_def obj_at_def is_tcb
dest!: tcb_at_ko_at)
apply (clarsimp split: option.splits elim!: pas_refined_Control[symmetric])
apply (frule pas_refined_Control, simp+)
apply (fastforce dest: bound_tcb_at_implies_reset
simp add: pred_tcb_at_def obj_at_def)
done
lemma finalise_cap_auth:
"\<lbrace>(\<lambda>s. final \<longrightarrow> is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s) and K (pas_cap_cur_auth aag cap)\<rbrace>
finalise_cap cap final
\<lbrace>\<lambda>rv _. \<forall>x \<in> obj_refs_ac (fst rv). \<forall>a \<in> cap_auth_conferred (fst rv). aag_has_auth_to aag a x\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_strengthen_post, rule finalise_cap_cases)
apply (elim disjE, clarsimp+)
apply (clarsimp simp: is_cap_simps cap_auth_conferred_def aag_cap_auth_def)
apply (simp add: fst_cte_ptrs_def split: cap.split_asm)
done
end
lemma aag_cap_auth_recycle_EndpointCap:
"\<lbrakk> pas_refined aag s; has_cancel_send_rights (EndpointCap word1 word2 f) \<rbrakk>
\<Longrightarrow> pas_cap_cur_auth aag (EndpointCap word1 word2 f) = is_subject aag word1"
unfolding aag_cap_auth_def
by (auto simp: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns
has_cancel_send_rights_def cap_rights_to_auth_def all_rights_def pas_refined_refl)
lemma aag_cap_auth_Zombie:
"pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (Zombie word a b) = is_subject aag word"
unfolding aag_cap_auth_def
by (simp add: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns)
lemma aag_cap_auth_CNode:
"pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (CNodeCap word a b) = is_subject aag word"
unfolding aag_cap_auth_def
by (simp add: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns)
lemma aag_cap_auth_Thread:
"pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (ThreadCap word) = is_subject aag word"
unfolding aag_cap_auth_def
by (simp add: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns)
context Finalise_AC_1 begin
lemma finalise_cap_auth':
"\<lbrace>pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace>
finalise_cap cap final
\<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>"
including classic_wp_pre
apply (rule hoare_gen_asm)
apply (cases cap, simp_all split del: if_split)
apply (wp | simp add: comp_def hoare_TrueI[where P = \<top>] split del: if_split
| fastforce simp: aag_cap_auth_Zombie aag_cap_auth_CNode aag_cap_auth_Thread)+
apply (rule hoare_pre)
apply (wp | simp)+
apply (wp arch_finalise_cap_auth')
done
lemma finalise_cap_obj_refs:
"\<lbrace>\<lambda>_ :: det_ext state. \<forall>x \<in> obj_refs_ac cap. P x\<rbrace>
finalise_cap cap slot
\<lbrace>\<lambda>rv _. \<forall>x \<in> obj_refs_ac (fst rv). P x\<rbrace>"
by (cases cap) (wpsimp wp: arch_finalise_cap_obj_refs simp: o_def | rule conjI)+
end
lemma zombie_ptr_emptyable:
"\<lbrakk> caps_of_state s cref = Some (Zombie ptr zbits n); invs s \<rbrakk>
\<Longrightarrow> emptyable (ptr, cref_half) s"
apply (clarsimp simp: emptyable_def tcb_at_def st_tcb_def2)
apply (rule ccontr)
apply (clarsimp simp: get_tcb_ko_at)
apply (drule if_live_then_nonz_capD[rotated])
apply (auto simp: live_def)[2]
apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state
zobj_refs_to_obj_refs)
apply (drule(2) zombies_final_helperE, clarsimp, simp+)
apply (simp add: is_cap_simps)
done
context Finalise_AC_1 begin
lemma finalise_cap_makes_halted:
"\<lbrace>invs and valid_cap cap and (\<lambda>s. ex = is_final_cap' cap s) and cte_wp_at ((=) cap) slot\<rbrace>
finalise_cap cap ex
\<lbrace>\<lambda>rv s :: det_ext state. \<forall>t \<in> obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>"
apply (case_tac cap, simp_all)
apply (wp unbind_notification_valid_objs
| clarsimp simp: o_def valid_cap_def cap_table_at_typ is_tcb
obj_at_def halted_if_tcb_def
split: option.split
| intro impI conjI
| rule hoare_drop_imp)+
apply (fastforce simp: st_tcb_at_def obj_at_def is_tcb live_def
dest!: final_zombie_not_live)
apply (wp arch_finalise_cap_makes_halted)
done
end
lemma aag_Control_into_owns_irq:
"\<lbrakk> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag; pas_refined aag s \<rbrakk>
\<Longrightarrow> is_subject_irq aag irq"
apply (drule (1) pas_refined_Control)
apply simp
done
lemma owns_slot_owns_irq:
"\<lbrakk> is_subject aag (fst slot); pas_refined aag s;
caps_of_state s slot = Some rv; cap_irq_opt rv = Some irq \<rbrakk>
\<Longrightarrow> is_subject_irq aag irq"
apply (rule aag_Control_into_owns_irq[rotated], assumption)
apply (drule (1) cli_caps_of_state)
apply (clarsimp simp: cap_links_irq_def cap_irq_opt_def split: cap.splits)
done
lemma replaceable_zombie_not_transferable:
"replaceable s slot (Zombie ref sz n) cap \<Longrightarrow> \<not> is_transferable (Some cap)"
by (intro notI) (erule is_transferable.cases; simp add:replaceable_def)
declare finalise_cap_valid_list[wp]
context Finalise_AC_1 begin
lemma rec_del_respects'_pre':
"s \<turnstile>
\<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and
simple_sched_action and valid_rec_del_call call and emptyable (slot_rdcall call) and
(\<lambda>s. \<not> exposed_rdcall call \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall call) s) and
K (is_subject aag (fst (slot_rdcall call))) and
K (case call of ReduceZombieCall cap sl _ \<Rightarrow> \<forall>x \<in> obj_refs_ac cap. is_subject aag x | _ \<Rightarrow> True)\<rbrace>
rec_del call
\<lbrace>\<lambda>rv. (\<lambda>s. trp \<longrightarrow> (case call of FinaliseSlotCall sl _ \<Rightarrow> (cleanup_info_wf (snd rv) aag)
| _ \<Rightarrow> True) \<and> integrity aag X st s) and pas_refined aag\<rbrace>,
\<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>"
proof (induct arbitrary: st rule: rec_del.induct, simp_all only: rec_del_fails)
case (1 slot exposed s)
show ?case
apply (rule hoare_spec_gen_asm)+
apply (subst rec_del.simps)
apply (simp only: split_def)
apply (rule hoare_pre_spec_validE)
apply (rule split_spec_bindE)
apply (wp hoare_weak_lift_imp)
apply (rule spec_strengthen_postE)
apply (rule spec_valid_conj_liftE1)
apply (rule valid_validE_R, rule rec_del_valid_list, rule preemption_point_inv';
solves\<open>simp\<close>)
apply (rule spec_valid_conj_liftE1)
apply (rule valid_validE_R, rule rec_del_invs)
apply (rule "1.hyps"[simplified rec_del_call.simps slot_rdcall.simps])
apply auto
done
next
case (2 slot exposed s)
show ?case
apply (rule hoare_spec_gen_asm)+
apply (subst rec_del.simps)
apply (simp only: split_def)
apply (rule hoare_pre_spec_validE)
apply (wp set_cap_integrity_autarch set_cap_pas_refined_not_transferable "2.hyps" hoare_weak_lift_imp)
apply ((wp preemption_point_inv' | simp add: integrity_subjects_def pas_refined_def)+)[1]
apply (simp(no_asm))
apply (rule spec_strengthen_postE)
apply (rule spec_valid_conj_liftE1, rule valid_validE_R, rule rec_del_invs)
apply (rule spec_valid_conj_liftE1, rule reduce_zombie_cap_to)
apply (rule spec_valid_conj_liftE1, rule rec_del_emptyable)
apply (rule spec_valid_conj_liftE1, rule valid_validE_R, rule rec_del_valid_sched')
apply (rule spec_valid_conj_liftE1, rule valid_validE_R, rule rec_del_valid_list,
rule preemption_point_inv')
apply simp
apply simp
apply (rule "2.hyps", assumption+)
apply simp
apply (simp add: conj_comms)
apply (wp set_cap_integrity_autarch set_cap_pas_refined_not_transferable replace_cap_invs
final_cap_same_objrefs set_cap_cte_cap_wp_to
set_cap_cte_wp_at hoare_vcg_const_Ball_lift hoare_weak_lift_imp
| rule finalise_cap_not_reply_master
| simp add: in_monad)+
apply (rule hoare_strengthen_post)
apply (rule_tac Q="\<lambda>fin s. einvs s \<and> simple_sched_action s \<and> replaceable s slot (fst fin) rv
\<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> (fst fin)
\<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s
\<and> emptyable slot s
\<and> (\<forall>t\<in>obj_refs_ac (fst fin). halted_if_tcb t s)
\<and> pas_refined aag s \<and> (trp \<longrightarrow> integrity aag X st s)
\<and> pas_cap_cur_auth aag (fst fin)"
in hoare_vcg_conj_lift)
apply (wp finalise_cap_invs[where slot=slot]
finalise_cap_replaceable[where sl=slot]
finalise_cap_makes_halted[where slot=slot]
finalise_cap_auth' hoare_weak_lift_imp)[1]
apply (rule finalise_cap_cases[where slot=slot])
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (erule disjE)
apply (clarsimp simp: cap_cleanup_opt_def arch_cap_cleanup_wf split: cap.split_asm)
apply (fastforce intro: owns_slot_owns_irq)
apply (clarsimp simp: is_cap_simps cap_auth_conferred_def clas_no_asid aag_cap_auth_def
pas_refined_all_auth_is_owns cli_no_irqs)
apply (drule appropriate_Zombie[symmetric, THEN trans, symmetric])
apply (clarsimp simp: gen_obj_refs_eq)
apply (erule_tac s = "{r}" in subst)
subgoal by (fastforce simp: replaceable_zombie_not_transferable)
apply (simp add: is_final_cap_def)
apply (wp get_cap_auth_wp [where aag = aag])+
apply (clarsimp simp: pas_refined_wellformed cte_wp_at_caps_of_state conj_comms)
apply (frule (1) caps_of_state_valid)
apply (frule if_unsafe_then_capD [OF caps_of_state_cteD], clarsimp+)
apply auto
done
next
case (3 ptr bits n slot s)
show ?case
apply (simp add: spec_validE_def)
apply (wp hoare_weak_lift_imp)
apply clarsimp
done
next
case (4 ptr bits n slot s)
show ?case
apply (rule hoare_spec_gen_asm)+
apply (subst rec_del.simps)
apply (rule hoare_pre_spec_validE)
apply (rule split_spec_bindE)
apply (rule split_spec_bindE[rotated])
apply (rule_tac Q'="\<lambda>rv s. invs s \<and> Q rv s" and Q="\<lambda>rv s. invs s \<and> Q rv s" for Q
in spec_strengthen_postE[rotated])
apply assumption
apply (rule spec_valid_conj_liftE1)
apply (wpsimp wp: rec_del_invs)
apply (rule "4.hyps", assumption+)
apply (wpsimp wp: set_cap_integrity_autarch set_cap_pas_refined_not_transferable
get_cap_wp hoare_weak_lift_imp)+
apply (clarsimp simp: invs_psp_aligned invs_vspace_objs invs_arch_state
cte_wp_at_caps_of_state clas_no_asid cli_no_irqs aag_cap_auth_def)
apply (drule_tac auth=auth in sta_caps, simp+)
apply (simp add: cap_auth_conferred_def aag_cap_auth_def)
apply (drule(1) pas_refined_mem)
apply (simp add: cap_auth_conferred_def is_cap_simps)
apply (wp | simp)+
apply (clarsimp simp add: zombie_is_cap_toE)
apply (clarsimp simp: cte_wp_at_caps_of_state zombie_ptr_emptyable)
done
qed
lemma rec_del_respects'_pre:
"s \<turnstile>
\<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and
simple_sched_action and valid_rec_del_call call and emptyable (slot_rdcall call) and
(\<lambda>s. \<not> exposed_rdcall call \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall call) s) and
K (is_subject aag (fst (slot_rdcall call))) and
K (case call of ReduceZombieCall cap sl _ \<Rightarrow> \<forall>x \<in> obj_refs_ac cap. is_subject aag x | _ \<Rightarrow> True)\<rbrace>
rec_del call
\<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>,
\<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>"
apply (rule spec_strengthen_postE[OF rec_del_respects'_pre'])
by simp
lemmas rec_del_respects'' = rec_del_respects'_pre[THEN use_spec(2), THEN validE_valid]
lemmas rec_del_respects =
rec_del_respects''[of True, THEN hoare_conjD1, simplified]
rec_del_respects''[of False, THEN hoare_conjD2, simplified]
end
lemma finalise_cap_transferable:
"\<lbrace>P and K (is_transferable_cap cap)\<rbrace>
finalise_cap cap final
\<lbrace>\<lambda>rv s. rv = (NullCap, NullCap) \<and> P s\<rbrace>"
by (rule hoare_gen_asm) (erule is_transferable_capE; wpsimp+)
lemma rec_del_Finalise_transferable:
"\<lbrace>(\<lambda>s. is_transferable (caps_of_state s slot)) and P\<rbrace>
rec_del (FinaliseSlotCall slot exposed)
\<lbrace>\<lambda>rv. K (rv = (True,NullCap)) and P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>"
apply (subst rec_del.simps[abs_def])
apply (wp hoare_K_bind | wpc )+
apply ((simp only: validE_R_def validE_E_def)?, rule hoare_FalseE)
apply ((simp only: validE_R_def validE_E_def)?, rule hoare_FalseE)
apply ((simp only: validE_R_def validE_E_def)?, rule hoare_FalseE)
apply (wp without_preemption_wp)
apply (rule hoare_post_imp[of "\<lambda>rv s. rv = (NullCap,NullCap) \<and> P s" for P])
apply (clarsimp; assumption)
apply (wp finalise_cap_transferable without_preemption_wp get_cap_wp)+
by (fastforce simp:cte_wp_at_caps_of_state)
context Finalise_AC_1 begin
lemma rec_del_respects_CTEDelete_transferable':
"\<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and
simple_sched_action and emptyable slot and cdt_change_allowed' aag slot and
(\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrace>
rec_del (CTEDeleteCall slot exposed)
\<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>,
\<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>"
apply (cases "is_subject aag (fst slot)")
apply (wp rec_del_respects'')
apply (solves \<open>simp\<close>)
apply (subst rec_del.simps[abs_def])
apply (wpsimp wp: wp_transferable hoare_weak_lift_imp)
apply (rule hoare_strengthen_postE,rule rec_del_Finalise_transferable)
apply simp apply simp
apply (rule hoare_strengthen_postE,rule rec_del_Finalise_transferable)
apply simp apply simp
apply (clarsimp)
apply (frule(3) cca_to_transferable_or_subject[OF invs_valid_objs invs_mdb])
by (safe; simp)
lemmas rec_del_respects_CTEDelete_transferable =
rec_del_respects_CTEDelete_transferable'[of True,THEN validE_valid,THEN hoare_conjD1,simplified]
rec_del_respects_CTEDelete_transferable'[of False,THEN validE_valid,THEN hoare_conjD2,simplified]
end
(* TODO section change *)
(* FIXME: CLAG *)
lemmas dmo_valid_cap[wp] = valid_cap_typ[OF do_machine_op_obj_at]
context Finalise_AC_1 begin
lemma set_eobject_integrity_autarch:
"\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace>
set_eobject ptr obj
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_eobject_def)
apply wp
apply (simp add: integrity_subjects_def)
done
lemma cancel_badged_sends_pas_refined[wp]:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>