-
Notifications
You must be signed in to change notification settings - Fork 1
/
Syscall_AC.thy
1257 lines (1116 loc) · 56.2 KB
/
Syscall_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 Syscall_AC
imports
Ipc_AC
Tcb_AC
Interrupt_AC
DomainSepInv
begin
context begin interpretation Arch . (*FIXME: arch_split*)
definition
authorised_invocation :: "'a PAS \<Rightarrow> Invocations_A.invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"authorised_invocation aag i \<equiv> \<lambda>s. case i of
Invocations_A.InvokeUntyped i' \<Rightarrow> valid_untyped_inv i' s \<and> (authorised_untyped_inv aag i') \<and> ct_active s
| Invocations_A.InvokeEndpoint epptr badge can_grant can_grant_reply \<Rightarrow>
\<exists>ep. ko_at (Endpoint ep) epptr s \<and>
(can_grant \<longrightarrow> (\<forall>r \<in> ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))
\<and> aag_has_auth_to aag Grant epptr \<and> aag_has_auth_to aag Call epptr) \<and>
(can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr)
\<and> aag_has_auth_to aag SyncSend epptr
| Invocations_A.InvokeNotification ep badge \<Rightarrow> aag_has_auth_to aag Notify ep
| Invocations_A.InvokeReply thread slot grant \<Rightarrow>
(grant \<longrightarrow> is_subject aag thread) \<and> is_subject aag (fst slot) \<and> aag_has_auth_to aag Reply thread
| Invocations_A.InvokeTCB i' \<Rightarrow> Tcb_AI.tcb_inv_wf i' s \<and> authorised_tcb_inv aag i'
| Invocations_A.InvokeDomain thread slot \<Rightarrow> False
| Invocations_A.InvokeCNode i' \<Rightarrow> authorised_cnode_inv aag i' s \<and> is_subject aag (cur_thread s)
\<and> cnode_inv_auth_derivations i' s
| Invocations_A.InvokeIRQControl i' \<Rightarrow> authorised_irq_ctl_inv aag i'
| Invocations_A.InvokeIRQHandler i' \<Rightarrow> authorised_irq_hdl_inv aag i'
| Invocations_A.InvokeArchObject i' \<Rightarrow> valid_arch_inv i' s \<and> authorised_arch_inv aag i' \<and> ct_active s"
lemma perform_invocation_pas_refined:
"\<lbrace>pas_refined aag and pas_cur_domain aag
and einvs and simple_sched_action and valid_invocation oper
and is_subject aag \<circ> cur_thread
and authorised_invocation aag oper\<rbrace>
perform_invocation blocking calling oper
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (cases oper, simp_all)
apply (simp add: authorised_invocation_def validE_R_def[symmetric] invs_valid_objs
| wp invoke_untyped_pas_refined send_ipc_pas_refined send_signal_pas_refined
do_reply_transfer_pas_refined invoke_tcb_pas_refined invoke_cnode_pas_refined
invoke_irq_control_pas_refined invoke_irq_handler_pas_refined
invoke_arch_pas_refined decode_cnode_invocation_auth_derived
| fastforce)+
done
lemma ntfn_gives_obj_at:
"invs s \<Longrightarrow>
(\<exists>ntfn. ko_at (Notification ntfn) ntfnptr s
\<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn).
(\<lambda>(t, rt). obj_at (\<lambda>tcb. ko_at tcb t s) t s) x)) = ntfn_at ntfnptr s"
apply (rule iffI)
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at_def is_ntfn)
apply (drule (1) ntfn_queued_st_tcb_at [where P = \<top>, unfolded obj_at_def, simplified])
apply clarsimp
apply clarsimp
apply (clarsimp simp: st_tcb_def2 dest!: get_tcb_SomeD)
done
(* ((=) st) -- too strong, the thread state of the calling thread changes. *)
lemma perform_invocation_respects:
"\<lbrace>pas_refined aag and integrity aag X st
and einvs and simple_sched_action and valid_invocation oper
and authorised_invocation aag oper
and is_subject aag \<circ> cur_thread
and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)
\<rbrace>
perform_invocation blocking calling oper
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
supply [wp] = invoke_untyped_integrity send_ipc_integrity_autarch send_signal_respects
do_reply_transfer_respects invoke_tcb_respects invoke_cnode_respects
invoke_arch_respects invoke_irq_control_respects invoke_irq_handler_respects
supply [simp] = authorised_invocation_def
proof (cases oper)
case InvokeEndpoint
show ?thesis
unfolding InvokeEndpoint
apply (rule hoare_pre)
apply wpsimp
apply (fastforce simp: obj_at_def is_tcb split: if_split_asm)
done
next
case InvokeNotification
show ?thesis
unfolding InvokeNotification
apply (rule hoare_pre)
apply wpsimp
apply fastforce
done
next
case InvokeReply
show ?thesis
unfolding InvokeReply
apply (rule hoare_pre)
apply wpsimp
apply clarsimp
apply (fastforce simp: is_reply_cap_to_def cur_tcb_def dest!: invs_cur)
done
qed (simp, rule hoare_pre, wpsimp, fastforce)+
declare AllowSend_def[simp] AllowRecv_def[simp]
lemma hoare_conjunct1_R:
"\<lbrace> P \<rbrace> f \<lbrace> \<lambda> r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,-"
apply(auto intro: hoare_post_imp_R)
done
lemma hoare_conjunct2_R:
"\<lbrace> P \<rbrace> f \<lbrace> \<lambda> r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q' \<rbrace>,-"
apply(auto intro: hoare_post_imp_R)
done
lemma decode_invocation_authorised:
"\<lbrace>pas_refined aag and valid_cap cap and invs and ct_active and cte_wp_at ((=) 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 ((=) (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)
and (is_subject aag \<circ> cur_thread) and
K (is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap
\<and> (\<forall>slot \<in> set excaps. is_subject aag (fst (snd slot)))
\<and> (\<forall>slot \<in> set excaps. pas_cap_cur_auth aag (fst slot)))
and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
decode_invocation info_label args ptr slot cap excaps
\<lbrace>\<lambda>rv. authorised_invocation aag rv\<rbrace>, -"
unfolding decode_invocation_def
apply (rule hoare_pre)
apply (wp decode_untyped_invocation_authorised
decode_cnode_invocation_auth_derived
decode_cnode_inv_authorised
decode_tcb_invocation_authorised decode_tcb_inv_wf
decode_arch_invocation_authorised
| strengthen cnode_eq_strg
| wpc | simp add: comp_def authorised_invocation_def decode_invocation_def
split del: if_split del: hoare_True_E_R
| wp (once) hoare_FalseE_R)+
apply (clarsimp simp: aag_has_Control_iff_owns split_def aag_cap_auth_def)
apply (cases cap, simp_all)
apply (fastforce simp: cte_wp_at_caps_of_state)
apply (clarsimp simp: valid_cap_def obj_at_def is_ep cap_auth_conferred_def
cap_rights_to_auth_def ball_Un)
apply (fastforce simp: valid_cap_def cap_auth_conferred_def cap_rights_to_auth_def
obj_at_def is_ep
intro!: owns_ep_owns_receivers)
apply (fastforce simp: cap_auth_conferred_def cap_rights_to_auth_def)
apply (clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def
pas_refined_Control[symmetric] reply_cap_rights_to_auth_def)
apply ((clarsimp simp: valid_cap_def is_cap_simps pas_refined_all_auth_is_owns
ex_cte_cap_wp_to_weakenE[OF _ TrueI]
cap_auth_conferred_def cap_rights_to_auth_def
| rule conjI | (subst split_paired_Ex[symmetric], erule exI)
| erule cte_wp_at_weakenE
| drule(1) bspec
| erule eq_no_cap_to_obj_with_diff_ref)+)[1]
apply (simp only: domain_sep_inv_def)
apply (rule impI, erule subst, rule pas_refined_sita_mem [OF sita_controlled],
auto simp: cte_wp_at_caps_of_state)[1]
apply (clarsimp simp add: cap_links_irq_def )
apply (drule (1) pas_refined_Control, simp)
apply (clarsimp simp: cap_links_asid_slot_def label_owns_asid_slot_def)
apply (fastforce dest!: pas_refined_Control)
done
lemma in_extended: "(u,a) \<in> fst (do_extended_op f s) \<Longrightarrow> \<exists>e. a = (trans_state (\<lambda>_. e) s)"
apply (clarsimp simp add: do_extended_op_def bind_def gets_def return_def get_def
mk_ef_def modify_def select_f_def put_def trans_state_update')
apply force
done
lemma set_thread_state_authorised[wp]:
"\<lbrace>authorised_invocation aag i and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace>
set_thread_state thread Structures_A.thread_state.Restart
\<lbrace>\<lambda>rv. authorised_invocation aag i\<rbrace>"
apply (cases i)
apply (simp_all add: authorised_invocation_def)
apply (wp sts_valid_untyped_inv ct_in_state_set
hoare_vcg_ex_lift sts_obj_at_impossible
| simp)+
apply (rename_tac cnode_invocation)
apply (case_tac cnode_invocation,
simp_all add: cnode_inv_auth_derivations_def authorised_cnode_inv_def)[1]
apply (wp set_thread_state_cte_wp_at | simp)+
apply (rename_tac arch_invocation)
apply (case_tac arch_invocation, simp_all add: valid_arch_inv_def)[1]
apply (rename_tac page_table_invocation)
apply (case_tac page_table_invocation, simp_all add: valid_pti_def)[1]
apply (wp sts_typ_ats sts_obj_at_impossible ct_in_state_set
hoare_vcg_ex_lift hoare_vcg_conj_lift
| simp add: valid_pdi_def)+
apply (rename_tac asid_control_invocation)
apply (case_tac asid_control_invocation, simp_all add: valid_aci_def)
apply (wp ct_in_state_set | simp)+
apply (rename_tac asid_pool_invocation)
apply (case_tac asid_pool_invocation; simp add: valid_apinv_def)
apply (wp sts_obj_at_impossible ct_in_state_set
hoare_vcg_ex_lift
| simp)+
done
lemma sts_first_restart:
"\<lbrace>(=) st and (\<lambda>s. thread = cur_thread s)\<rbrace>
set_thread_state thread Structures_A.thread_state.Restart
\<lbrace>\<lambda>rv s. \<forall>p ko. kheap s p = Some ko \<longrightarrow>
(is_tcb ko \<longrightarrow> p \<noteq> cur_thread st) \<longrightarrow> kheap st p = Some ko\<rbrace>"
unfolding set_thread_state_def
by (wpsimp wp: set_object_wp dxo_wp_weak simp: is_tcb)
lemma lcs_reply_owns:
"\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
lookup_cap_and_slot thread ptr
\<lbrace>\<lambda>rv s. \<forall>ep. (\<exists>m R. fst rv = cap.ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep\<rbrace>, -"
apply (rule hoare_post_imp_R)
apply (rule hoare_pre)
apply (rule hoare_vcg_conj_lift_R [where S = "K (pas_refined aag)"])
apply (rule lookup_cap_and_slot_cur_auth)
apply (simp | wp lookup_cap_and_slot_inv)+
apply (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
dest: aag_Control_into_owns)
done
crunch pas_refined[wp]: reply_from_kernel "pas_refined aag"
(simp: split_def)
lemma lookup_cap_and_slot_valid_fault3:
"\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr
-,
\<lbrace>\<lambda>ft s. valid_fault (ExceptionTypes_A.CapFault (of_bl cptr) rp ft)\<rbrace>"
apply (unfold validE_E_def)
apply (rule hoare_post_impErr)
apply (rule lookup_cap_and_slot_valid_fault)
apply auto
done
definition guarded_pas_domain
where
"guarded_pas_domain aag \<equiv>
\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow>
pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)"
lemma guarded_pas_domain_lift:
assumes a: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>"
assumes b: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>"
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>"
shows "\<lbrace>guarded_pas_domain aag\<rbrace> f \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>"
apply (simp add: guarded_pas_domain_def)
apply (rule hoare_pre)
apply (wps a b c)
apply wp
apply simp
done
lemma guarded_to_cur_domain:
"\<lbrakk>invs s; ct_in_state x s; \<not> x IdleThreadState; guarded_pas_domain aag s;
is_subject aag (cur_thread s)\<rbrakk>
\<Longrightarrow> pas_cur_domain aag s"
by (auto simp: invs_def valid_state_def valid_idle_def pred_tcb_at_def obj_at_def
ct_in_state_def guarded_pas_domain_def)
lemma handle_invocation_pas_refined:
shows "\<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'
and einvs and ct_active and schact_is_rct
and is_subject aag \<circ> cur_thread\<rbrace>
handle_invocation calling blocking
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: handle_invocation_def split_def)
apply (cases blocking, simp)
apply (rule hoare_pre)
by (((wp syscall_valid without_preemption_wp
handle_fault_pas_refined set_thread_state_pas_refined
set_thread_state_runnable_valid_sched
perform_invocation_pas_refined
hoare_vcg_conj_lift hoare_vcg_all_lift
| wpc
| rule hoare_drop_imps
| simp add: if_apply_def2 conj_comms split del: if_split
del: hoare_True_E_R)+),
((wp lookup_extra_caps_auth lookup_extra_caps_authorised
decode_invocation_authorised
lookup_cap_and_slot_authorised
lookup_cap_and_slot_cur_auth
as_user_pas_refined
lookup_cap_and_slot_valid_fault3
| simp add: comp_def runnable_eq_active)+),
(auto intro: guarded_to_cur_domain
simp: ct_in_state_def st_tcb_at_def live_def hyp_live_def
intro: if_live_then_nonz_capD)[1])+
lemma handle_invocation_respects:
"\<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'
and einvs and ct_active and schact_is_rct
and is_subject aag \<circ> cur_thread
and ((=) st)\<rbrace>
handle_invocation calling blocking
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: handle_invocation_def split_def)
apply (wp syscall_valid without_preemption_wp handle_fault_integrity_autarch
reply_from_kernel_integrity_autarch
set_thread_state_integrity_autarch
hoare_vcg_conj_lift
hoare_vcg_all_lift_R hoare_vcg_all_lift
| rule hoare_drop_imps
| wpc
| simp add: if_apply_def2
split del: if_split)+
apply (simp add: conj_comms pred_conj_def comp_def if_apply_def2 split del: if_split
| wp perform_invocation_respects set_thread_state_pas_refined
set_thread_state_authorised
set_thread_state_runnable_valid_sched
set_thread_state_integrity_autarch
sts_first_restart
decode_invocation_authorised
lookup_extra_caps_auth lookup_extra_caps_authorised
set_thread_state_integrity_autarch
lookup_cap_and_slot_cur_auth lookup_cap_and_slot_authorised
hoare_vcg_const_imp_lift perform_invocation_pas_refined
set_thread_state_ct_st hoare_vcg_const_imp_lift_R
lookup_cap_and_slot_valid_fault3
| (rule valid_validE, strengthen invs_vobjs_strgs))+
by (fastforce intro: st_tcb_ex_cap' guarded_to_cur_domain
simp: ct_in_state_def runnable_eq_active)
crunch pas_refined[wp]: delete_caller_cap "pas_refined aag"
lemma invs_sym_refs_strg:
"invs s \<longrightarrow> sym_refs (state_refs_of s)" by clarsimp
lemma handle_recv_pas_refined:
"\<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace>
handle_recv is_blocking
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: handle_recv_def Let_def lookup_cap_def split_def)
apply (wp handle_fault_pas_refined receive_ipc_pas_refined receive_signal_pas_refined
get_cap_auth_wp [where aag=aag] lookup_slot_for_cnode_op_authorised
lookup_slot_for_thread_authorised lookup_slot_for_thread_cap_fault
hoare_vcg_all_lift_R get_simple_ko_wp
| wpc | simp
| (rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread
\<and> (pasSubject aag, Receive, pasObjectAbs aag thread) \<in> pasPolicy aag"
in hoare_strengthen_post,
wp, clarsimp simp: invs_valid_objs invs_sym_refs))+
apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s
\<and> cur_thread s = thread \<and> is_subject aag (cur_thread s)
\<and> is_subject aag thread" in hoare_post_imp_R [rotated])
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
cap_rights_to_auth_def valid_fault_def)
apply (wp user_getreg_inv | strengthen invs_vobjs_strgs invs_sym_refs_strg | simp)+
apply clarsimp
done
crunch respects[wp]: delete_caller_cap "integrity aag X st"
lemma invs_mdb_strgs: "invs s \<longrightarrow> valid_mdb s"
by auto
lemma handle_recv_integrity:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread
and K(valid_mdb st \<and> valid_objs st)\<rbrace>
handle_recv is_blocking
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: handle_recv_def Let_def lookup_cap_def split_def)
apply (wp handle_fault_integrity_autarch receive_ipc_integrity_autarch
receive_signal_integrity_autarch lookup_slot_for_thread_authorised
lookup_slot_for_thread_cap_fault get_cap_auth_wp [where aag=aag] get_simple_ko_wp
| wpc
| simp
| rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread
\<and> (pasSubject aag, Receive, pasObjectAbs aag thread) \<in> pasPolicy aag"
in hoare_strengthen_post, wp, clarsimp simp: invs_valid_objs invs_sym_refs)+
apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> einvs s \<and> is_subject aag (cur_thread s)
\<and> tcb_at thread s \<and> cur_thread s = thread
\<and> is_subject aag thread \<and> integrity aag X st s" in hoare_post_imp_R [rotated])
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
cap_rights_to_auth_def valid_fault_def)
apply (wp user_getreg_inv
| strengthen invs_vobjs_strgs invs_sym_refs_strg invs_mdb_strgs
| simp)+
apply clarsimp
done
lemma handle_reply_pas_refined[wp]:
"\<lbrace> pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace>
handle_reply
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
unfolding handle_reply_def
apply (rule hoare_pre)
apply (wp do_reply_transfer_pas_refined get_cap_auth_wp [where aag = aag]| wpc)+
by (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
intro: aag_Control_into_owns)
lemma handle_reply_respects:
"\<lbrace>integrity aag X st and pas_refined aag
and einvs
and is_subject aag \<circ> cur_thread\<rbrace>
handle_reply
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
unfolding handle_reply_def
apply (rule hoare_pre)
apply (wp do_reply_transfer_respects get_cap_auth_wp [where aag = aag]| wpc)+
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
cur_tcb_def cte_wp_at_caps_of_state is_reply_cap_to_def
intro: aag_Control_into_owns
dest: invs_cur)
done
lemma ethread_set_time_slice_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace>
ethread_set (tcb_time_slice_update f) thread
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: ethread_set_def set_eobject_def | wp)+
apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def)
apply (erule_tac x="(a, b)" in ballE)
apply force
apply (erule notE)
apply (erule domains_of_state_aux.cases, simp add: get_etcb_def split: if_split_asm)
apply (force intro: domtcbs)+
done
lemma thread_set_time_slice_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace>
thread_set_time_slice tptr time
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: thread_set_time_slice_def | wp)+
done
lemma dec_domain_time_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace>
dec_domain_time
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: dec_domain_time_def | wp)+
apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def)
done
crunch pas_refined[wp]: timer_tick "pas_refined aag"
(wp_del: timer_tick_extended.pas_refined_tcb_domain_map_wellformed)
lemma handle_interrupt_pas_refined:
"\<lbrace>pas_refined aag\<rbrace>
handle_interrupt irq
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: handle_interrupt_def)
apply (rule conjI; rule impI;rule hoare_pre)
apply (wp send_signal_pas_refined get_cap_wp
| wpc
| simp add: get_irq_slot_def get_irq_state_def handle_reserved_irq_def)+
done
lemma dec_domain_time_integrity[wp]:
"\<lbrace>integrity aag X st\<rbrace>
dec_domain_time
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: dec_domain_time_def | wp)+
apply (clarsimp simp: integrity_subjects_def)
done
lemma timer_tick_integrity[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
timer_tick
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: timer_tick_def)
apply (wp ethread_set_integrity_autarch gts_wp
| wpc | simp add: thread_set_time_slice_def split del: if_split)+
apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def)
done
lemma handle_interrupt_integrity_autarch:
"\<lbrace>integrity aag X st and pas_refined aag
and invs and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))
and K (is_subject_irq aag irq)\<rbrace>
handle_interrupt irq
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: handle_interrupt_def cong: irq_state.case_cong maskInterrupt_def
ackInterrupt_def resetTimer_def )
apply (rule conjI; rule impI; rule hoare_pre)
apply (wp (once) send_signal_respects get_cap_auth_wp [where aag = aag] dmo_mol_respects
| simp add: get_irq_slot_def get_irq_state_def ackInterrupt_def resetTimer_def
handle_reserved_irq_def
| wp dmo_no_mem_respects
| wpc)+
apply (fastforce simp: is_cap_simps aag_cap_auth_def cap_auth_conferred_def
cap_rights_to_auth_def)
done
lemma hacky_ipc_Send:
"\<lbrakk> (pasObjectAbs aag (interrupt_irq_node s irq), Notify, pasObjectAbs aag p) \<in> pasPolicy aag;
pas_refined aag s; pasMaySendIrqs aag \<rbrakk>
\<Longrightarrow> aag_has_auth_to aag Notify p"
unfolding pas_refined_def
apply (clarsimp simp: policy_wellformed_def irq_map_wellformed_aux_def)
apply (drule spec [where x = "pasIRQAbs aag irq"], drule spec [where x = "pasObjectAbs aag p"],
erule mp)
apply simp
done
lemma handle_interrupt_integrity:
"\<lbrace>integrity aag X st and pas_refined aag and invs
and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal)
and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
handle_interrupt irq
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: handle_interrupt_def maskInterrupt_def ackInterrupt_def resetTimer_def
cong: irq_state.case_cong bind_cong)
apply (rule conjI; rule impI; rule hoare_pre)
apply (wp (once) send_signal_respects get_cap_wp dmo_mol_respects dmo_no_mem_respects
| wpc
| simp add: get_irq_slot_def get_irq_state_def ackInterrupt_def resetTimer_def
handle_reserved_irq_def)+
apply clarsimp
apply (rule conjI, fastforce)+ \<comment> \<open>valid_objs etc.\<close>
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (rule_tac s = s in hacky_ipc_Send [where irq = irq])
apply (drule (1) cap_auth_caps_of_state)
apply (clarsimp simp: aag_cap_auth_def is_cap_simps cap_auth_conferred_def
cap_rights_to_auth_def split: if_split_asm)
apply assumption+
done
lemma handle_vm_fault_integrity:
"\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace>
handle_vm_fault thread vmfault_type
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (cases vmfault_type, simp_all)
apply (rule hoare_pre)
apply (wp as_user_integrity_autarch dmo_wp | simp add: getDFSR_def getFAR_def getIFSR_def)+
done
lemma handle_vm_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace>
handle_vm_fault thread vmfault_type
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (cases vmfault_type, simp_all)
apply (wp | simp)+
done
crunch pas_refined[wp]: handle_hypervisor_fault "pas_refined aag"
crunch cur_thread[wp]: handle_hypervisor_fault "\<lambda>s. P (cur_thread s)"
crunch integrity[wp]: handle_hypervisor_fault "integrity aag X st"
lemma handle_vm_cur_thread [wp]:
"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace>
handle_vm_fault thread vmfault_type
\<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
apply (cases vmfault_type, simp_all)
apply (wp | simp)+
done
lemma handle_vm_state_refs_of [wp]:
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
handle_vm_fault thread vmfault_type
\<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>"
apply (cases vmfault_type, simp_all)
apply (wp | simp)+
done
lemma handle_yield_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace>
handle_yield
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
by (simp add: handle_yield_def | wp)+
lemma handle_event_pas_refined:
"\<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'
and einvs and schact_is_rct
and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> is_subject aag (cur_thread s))
and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) \<rbrace>
handle_event ev
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (case_tac ev; simp)
apply (rename_tac syscall)
apply (case_tac syscall; simp add: handle_send_def handle_call_def)
apply ((wp handle_invocation_pas_refined handle_recv_pas_refined
handle_fault_pas_refined
| simp | clarsimp)+)
apply (fastforce simp: valid_fault_def)
apply (wp handle_fault_pas_refined
| simp)+
apply (fastforce simp: valid_fault_def)
apply (wp handle_interrupt_pas_refined handle_fault_pas_refined
hoare_vcg_conj_lift hoare_vcg_all_lift
| wpc
| rule hoare_drop_imps
| strengthen invs_vobjs_strgs
| simp)+
done
lemma valid_fault_Unknown [simp]:
"valid_fault (UnknownSyscallException x)"
by (simp add: valid_fault_def)
lemma valid_fault_User [simp]:
"valid_fault (UserException word1 word2)"
by (simp add: valid_fault_def)
declare hy_inv[wp del]
lemma handle_yield_integrity[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace>
handle_yield
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
by (simp add: handle_yield_def | wp)+
lemma ct_in_state_machine_state_update[simp]: "ct_in_state s (st\<lparr>machine_state := x\<rparr>) = ct_in_state s st"
apply (simp add: ct_in_state_def)
done
lemma handle_event_integrity:
"\<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'
and einvs and schact_is_rct
and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and ((=) st)\<rbrace>
handle_event ev
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (case_tac "ev \<noteq> Interrupt")
apply (case_tac ev; simp)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all add: handle_send_def handle_call_def)
apply (wp handle_recv_integrity handle_invocation_respects
handle_reply_respects handle_fault_integrity_autarch
handle_interrupt_integrity handle_vm_fault_integrity
handle_reply_pas_refined handle_vm_fault_valid_fault
handle_reply_valid_sched
hoare_vcg_conj_lift hoare_vcg_all_lift alternative_wp select_wp
| rule dmo_wp
| wpc
| simp add: getActiveIRQ_def domain_sep_inv_def
| clarsimp
| rule conjI hoare_vcg_E_elim
| strengthen invs_vobjs_strgs invs_mdb_strgs
| fastforce)+
done
lemma set_thread_state_restart_to_running_respects:
"\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Restart) thread
and K (pasMayActivate aag)\<rbrace>
do pc \<leftarrow> as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Structures_A.thread_state.Running
od
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def as_user_def split_def setNextPC_def
getRestartPC_def setRegister_def bind_assoc getRegister_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: in_monad fun_upd_def[symmetric] cong: if_cong)
apply (cases "is_subject aag thread")
apply (cut_tac aag=aag in integrity_update_autarch, simp+)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def)
apply (clarsimp dest!: get_tcb_SomeD)
apply (rule_tac tro_tcb_activate[OF refl refl])
apply (simp add: tcb_bound_notification_reset_integrity_def)+
done
lemma activate_thread_respects:
"\<lbrace>integrity aag X st and K (pasMayActivate aag)\<rbrace>
activate_thread
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: activate_thread_def arch_activate_idle_thread_def)
apply (rule hoare_pre)
apply (wp set_thread_state_restart_to_running_respects thread_get_wp'
| wpc | simp add: arch_activate_idle_thread_def get_thread_state_def)+
apply (clarsimp simp: st_tcb_at_def obj_at_def)
done
lemma activate_thread_integrity:
"\<lbrace>integrity aag X st and (\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and valid_idle\<rbrace>
activate_thread
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: activate_thread_def arch_activate_idle_thread_def)
apply (rule hoare_pre)
apply (wp gts_wp set_thread_state_integrity_autarch as_user_integrity_autarch | wpc | simp add: arch_activate_idle_thread_def)+
apply(clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
done
lemma activate_thread_pas_refined:
"\<lbrace> pas_refined aag \<rbrace>
activate_thread
\<lbrace>\<lambda>rv. pas_refined aag \<rbrace>"
unfolding activate_thread_def arch_activate_idle_thread_def
get_thread_state_def thread_get_def
apply (rule hoare_pre)
apply (wp set_thread_state_pas_refined hoare_drop_imps
| wpc | simp)+
done
lemma integrity_exclusive_state [iff]:
"integrity aag X st (s\<lparr>machine_state := machine_state s \<lparr>exclusive_state := es \<rparr>\<rparr>)
= integrity aag X st s"
unfolding integrity_def
by simp
lemma dmo_clearExMonitor_respects_globals[wp]:
"\<lbrace>integrity aag X st\<rbrace>
do_machine_op clearExMonitor
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_pre)
apply (simp add: clearExMonitor_def | wp dmo_wp)+
done
lemma integrity_cur_thread [iff]:
"integrity aag X st (s\<lparr>cur_thread := v\<rparr>) = integrity aag X st s"
unfolding integrity_def by simp
lemma tcb_sched_action_dequeue_integrity_pasMayEditReadyQueues:
"\<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<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)
done
lemma as_user_set_register_respects_indirect:
"\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at receive_blocked thread st
\<and> bound_tcb_at ((=) (Some ntfnptr)) thread st)
\<and> (aag_has_auth_to aag Notify ntfnptr)) \<rbrace>
as_user thread (setRegister r v)
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: as_user_def split_def set_object_def get_object_def)
apply wp
apply (clarsimp simp: in_monad setRegister_def)
apply (cases "is_subject aag thread")
apply (erule (1) integrity_update_autarch [unfolded fun_upd_def])
apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
apply (simp split: thread_state.split_asm)
apply (rule send_upd_ctxintegrity [OF disjI2, unfolded fun_upd_def],
auto simp: st_tcb_def2 indirect_send_def pred_tcb_def2 dest: sym)
done
lemma switch_to_thread_respects_pasMayEditReadyQueues:
notes tcb_sched_action_dequeue_integrity[wp del]
shows
"\<lbrace>integrity aag X st and pas_refined aag
and K (pasMayEditReadyQueues aag)\<rbrace>
switch_to_thread t
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
unfolding switch_to_thread_def arch_switch_to_thread_def
apply (simp add: spec_valid_def)
apply (wp tcb_sched_action_dequeue_integrity_pasMayEditReadyQueues
| simp add: clearExMonitor_def)+
done
lemma switch_to_thread_respects:
"\<lbrace>integrity aag X st and pas_refined aag
and K (is_subject aag t) \<rbrace>
switch_to_thread t
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
unfolding switch_to_thread_def arch_switch_to_thread_def
apply (simp add: spec_valid_def)
apply (wp | simp add: clearExMonitor_def)+
done
text \<open>
Variants of scheduling lemmas without is_subject assumption.
See comment for @{thm tcb_sched_action_dequeue_integrity'}
\<close>
lemma switch_to_thread_respects':
"\<lbrace>integrity aag X st and pas_refined aag
and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t)))) \<rbrace>
switch_to_thread t
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
unfolding switch_to_thread_def arch_switch_to_thread_def
apply (simp add: spec_valid_def)
apply (wp tcb_sched_action_dequeue_integrity'
| simp add: clearExMonitor_def)+
done
lemma switch_to_idle_thread_respects:
"\<lbrace>integrity aag X st\<rbrace>
switch_to_idle_thread
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
unfolding switch_to_idle_thread_def arch_switch_to_idle_thread_def
by (wp | simp)+
lemma choose_thread_respects_pasMayEditReadyQueues:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and valid_queues and K (pasMayEditReadyQueues aag ) \<rbrace>
choose_thread
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
by (simp add: choose_thread_def guarded_switch_to_def
| wp switch_to_thread_respects_pasMayEditReadyQueues switch_to_idle_thread_respects gts_wp)+
text \<open>integrity for @{const choose_thread} without @{const pasMayEditReadyQueues}\<close>
lemma choose_thread_respects:
"\<lbrace>integrity aag X st and pas_refined aag and pas_cur_domain aag and einvs and valid_queues\<rbrace>
choose_thread
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: choose_thread_def guarded_switch_to_def
| wp switch_to_thread_respects' switch_to_idle_thread_respects gts_wp)+
apply (clarsimp simp: pas_refined_def)
apply (clarsimp simp: tcb_domain_map_wellformed_aux_def)
apply (clarsimp simp: valid_queues_def is_etcb_at_def)
apply (erule_tac x="cur_domain s" in allE)
apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE)
apply clarsimp
apply (erule_tac x="hd (max_non_empty_queue (ready_queues s (cur_domain s)))" in ballE)
apply (clarsimp simp: etcb_at_def)
(* thread we're switching to is in cur_domain *)
apply (rule_tac s = "cur_domain s" in subst)
apply (clarsimp simp: max_non_empty_queue_def)
apply (frule tcb_at_ekheap_dom[OF st_tcb_at_tcb_at])
apply (simp add: valid_sched_def)
apply (clarsimp simp: max_non_empty_queue_def)
apply (metis (mono_tags, lifting) setcomp_Max_has_prop hd_in_set)
(* pas_cur_domain *)
apply assumption
done
lemma guarded_switch_to_respects:
"\<lbrace> integrity aag X st
and pas_refined aag and (\<lambda>s. is_subject aag x)\<rbrace>
guarded_switch_to x
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: guarded_switch_to_def)
apply (simp add: choose_thread_def guarded_switch_to_def
| wp switch_to_thread_respects switch_to_idle_thread_respects gts_wp)+
done
lemma next_domain_integrity [wp]:
"\<lbrace>integrity aag X st\<rbrace>
next_domain
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def | wp)+
apply (clarsimp simp: get_etcb_def integrity_subjects_def lfp_def)
done
lemma next_domain_tcb_domain_map_wellformed [wp]:
"\<lbrace>tcb_domain_map_wellformed aag\<rbrace>
next_domain
\<lbrace>\<lambda>rv. tcb_domain_map_wellformed aag\<rbrace>"
by (simp add: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def | wp)+
lemma valid_blocked_2_valid_blocked_except[simp]:
"valid_blocked_2 queues kh sa ct \<Longrightarrow> valid_blocked_except_2 t queues kh sa ct"
by (clarsimp simp: valid_blocked_def valid_blocked_except_def)
(* clagged from Schedule_R *)
lemma next_domain_valid_sched:
"\<lbrace> valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> next_domain \<lbrace> \<lambda>_. valid_sched \<rbrace>"
apply (simp add: next_domain_def Let_def)
apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def)
apply (simp add:valid_blocked_2_def)
done
text \<open>
We need to use the domain of t instead of @{term "is_subject aag t"}
because t's domain may contain multiple labels. See the comment for
@{thm tcb_sched_action_dequeue_integrity'}
\<close>
lemma valid_sched_action_switch_subject_thread:
"\<lbrakk> scheduler_action s = switch_thread t ; valid_sched_action s ;
valid_etcbs s ; pas_refined aag s ; pas_cur_domain aag s \<rbrakk>
\<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) \<and>
pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t)))"
apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_2_def
switch_in_cur_domain_2_def in_cur_domain_2_def valid_etcbs_def
etcb_at_def st_tcb_at_def obj_at_def is_etcb_at_def)
apply (rule conjI)
apply (force simp: pas_refined_def tcb_domain_map_wellformed_aux_def
intro: domtcbs)
apply force
done
lemma schedule_choose_new_thread_integrity:
"\<lbrace> invs and valid_sched and valid_list and integrity aag X st and pas_refined aag
and K (pasMayEditReadyQueues aag)
and (\<lambda>s. scheduler_action s = choose_new_thread) \<rbrace>
schedule_choose_new_thread
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
unfolding schedule_choose_new_thread_def
by (wpsimp wp: choose_thread_respects_pasMayEditReadyQueues
next_domain_valid_sched next_domain_valid_queues
simp: schedule_choose_new_thread_def valid_sched_def)
lemma schedule_integrity:
"\<lbrace>einvs and integrity aag X st and pas_refined aag and pas_cur_domain aag
and (\<lambda>s. domain_time s \<noteq> 0) \<rbrace>
schedule
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: schedule_def)
apply (rule hoare_pre)
supply ethread_get_wp[wp del]
apply (wp|wpc|simp only: schedule_choose_new_thread_def)+
apply (wpsimp wp: alternative_wp switch_to_thread_respects' select_wp switch_to_idle_thread_respects
guarded_switch_to_lift choose_thread_respects gts_wp hoare_drop_imps
set_scheduler_action_cnt_valid_sched append_thread_queued enqueue_thread_queued
tcb_sched_action_enqueue_valid_blocked_except
tcb_sched_action_append_integrity'
wp_del: ethread_get_wp
| wpc
| simp add: allActiveTCBs_def schedule_choose_new_thread_def
| rule hoare_pre_cont[where a=next_domain])+
apply (auto simp: obj_at_def st_tcb_at_def not_cur_thread_2_def valid_sched_def
valid_sched_action_def weak_valid_sched_action_def
valid_sched_action_switch_subject_thread schedule_choose_new_thread_def)
done
lemma valid_sched_valid_sched_action:
"valid_sched s \<Longrightarrow> valid_sched_action s"
by (simp add: valid_sched_def)
lemma schedule_integrity_pasMayEditReadyQueues:
"\<lbrace>einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag
and K (pasMayEditReadyQueues aag) \<rbrace>
schedule
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
supply ethread_get_wp[wp del]
supply schedule_choose_new_thread_integrity[wp]
supply if_split[split del]
apply (simp add: schedule_def wrap_is_highest_prio_def[symmetric])
apply (wp, wpc)
(* resume current thread *)
apply wp
prefer 2
(* choose thread *)
apply wp
(* switch_to *)
apply (wpsimp wp: set_scheduler_action_cnt_valid_sched enqueue_thread_queued append_thread_queued
tcb_sched_action_append_integrity_pasMayEditReadyQueues
guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues)+
(* is_highest_prio *)
apply (simp add: wrap_is_highest_prio_def)
apply ((wp (once) hoare_drop_imp)+)[1]
apply (wpsimp wp: tcb_sched_action_enqueue_valid_blocked_except hoare_vcg_imp_lift' gts_wp)+
apply (clarsimp simp: if_apply_def2 cong: imp_cong conj_cong)
apply (safe ; ((solves \<open>clarsimp simp: valid_sched_def not_cur_thread_def valid_sched_action_def
weak_valid_sched_action_def\<close>
)?))
apply (clarsimp simp: obj_at_def pred_tcb_at_def)+
done
lemma pas_refined_cur_thread [iff]:
"pas_refined aag (s\<lparr>cur_thread := v\<rparr>) = pas_refined aag s"
unfolding pas_refined_def
by (simp add: state_objs_to_policy_def)
lemma switch_to_thread_pas_refined:
"\<lbrace>pas_refined aag\<rbrace>
switch_to_thread t
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
unfolding switch_to_thread_def arch_switch_to_thread_def
by (wp do_machine_op_pas_refined | simp)+
lemma switch_to_idle_thread_pas_refined:
"\<lbrace>pas_refined aag\<rbrace>
switch_to_idle_thread
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
unfolding switch_to_idle_thread_def arch_switch_to_idle_thread_def
by (wp do_machine_op_pas_refined | simp)+
crunch pas_refined[wp]: choose_thread "pas_refined aag" (wp: switch_to_thread_pas_refined switch_to_idle_thread_pas_refined crunch_wps)
lemma schedule_pas_refined:
"\<lbrace>pas_refined aag\<rbrace>
schedule
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: schedule_def allActiveTCBs_def)
apply (wp add: alternative_wp guarded_switch_to_lift switch_to_thread_pas_refined select_wp
switch_to_idle_thread_pas_refined gts_wp
guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues
choose_thread_respects_pasMayEditReadyQueues
next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps
set_scheduler_action_cnt_valid_sched enqueue_thread_queued
tcb_sched_action_enqueue_valid_blocked_except
del: ethread_get_wp
| wpc | simp add: schedule_choose_new_thread_def)+
done
lemma handle_interrupt_arch_state [wp]:
"\<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
unfolding handle_interrupt_def
apply (rule hoare_if)