-
Notifications
You must be signed in to change notification settings - Fork 108
/
Ipc_AC.thy
2872 lines (2546 loc) · 135 KB
/
Ipc_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 Ipc_AC
imports ArchFinalise_AC "Lib.MonadicRewrite"
begin
section\<open>Notifications\<close>
subsection\<open>@{term "pas_refined"}\<close>
crunch do_machine_op
for thread_bound_ntfns[wp]: "\<lambda>s. P (thread_bound_ntfns s)"
lemma cancel_ipc_receive_blocked_caps_of_state:
"\<lbrace>\<lambda>s. P (caps_of_state s) \<and> st_tcb_at receive_blocked t s\<rbrace>
cancel_ipc t
\<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
apply (clarsimp simp: cancel_ipc_def)
apply (rule bind_wp[OF _ gts_sp])
apply (rule hoare_pre)
apply (wp gts_wp | wpc | simp)+
apply (rule hoare_pre_cont)+
apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
apply (clarsimp split: thread_state.splits)
done
lemma send_signal_caps_of_state[wp]:
"send_signal ntfnptr badge \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>"
apply (clarsimp simp: send_signal_def)
apply (rule bind_wp[OF _ get_simple_ko_sp])
apply (wpsimp wp: dxo_wp_weak cancel_ipc_receive_blocked_caps_of_state gts_wp hoare_weak_lift_imp
simp: update_waiting_ntfn_def)
apply (clarsimp simp: fun_upd_def[symmetric] st_tcb_def2)
done
crunch blocked_cancel_ipc, update_waiting_ntfn
for mdb[wp]: "\<lambda>s. P (cdt (s :: det_ext state))"
(wp: crunch_wps unless_wp dxo_wp_weak simp: crunch_simps)
lemma cancel_ipc_receive_blocked_mdb:
"\<lbrace>\<lambda>s :: det_ext state. P (cdt s) \<and> st_tcb_at receive_blocked t s\<rbrace>
cancel_ipc t
\<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>"
apply (clarsimp simp: cancel_ipc_def)
apply (rule bind_wp[OF _ gts_sp])
apply (rule hoare_pre)
apply (wp gts_wp | wpc | simp)+
apply (rule hoare_pre_cont)+
apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
apply (clarsimp split: thread_state.splits)
done
lemma send_signal_mdb[wp]:
"send_signal ntfnptr badge \<lbrace>\<lambda>s :: det_ext state. P (cdt s)\<rbrace>"
apply (clarsimp simp: send_signal_def)
apply (rule bind_wp[OF _ get_simple_ko_sp])
apply (rule hoare_pre)
apply (wp dxo_wp_weak gts_wp cancel_ipc_receive_blocked_mdb | wpc | simp)+
apply (clarsimp simp: st_tcb_def2)
done
crunch possible_switch_to
for tcb_domain_map_wellformed[wp]: "tcb_domain_map_wellformed aag"
lemma update_waiting_ntfn_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
and ko_at (Notification ntfn) ntfnptr and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace>
update_waiting_ntfn ntfnptr queue badge val
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
by (wpsimp wp: set_thread_state_pas_refined set_simple_ko_pas_refined simp: update_waiting_ntfn_def)
lemma cancel_ipc_receive_blocked_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs
and valid_arch_state and st_tcb_at receive_blocked t\<rbrace>
cancel_ipc t
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (clarsimp simp: cancel_ipc_def)
apply (rule bind_wp[OF _ gts_sp])
apply (wp gts_wp | wpc | simp)+
apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
done
lemma send_signal_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
send_signal ntfnptr badge
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: send_signal_def)
apply (rule bind_wp[OF _ get_simple_ko_sp])
apply (wpsimp wp: set_simple_ko_pas_refined update_waiting_ntfn_pas_refined gts_wp
set_thread_state_pas_refined cancel_ipc_receive_blocked_pas_refined)
apply (fastforce simp: st_tcb_def2)
done
lemma receive_signal_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
and K (\<forall>ntfnptr \<in> obj_refs_ac cap. abs_has_auth_to aag Receive thread ntfnptr)\<rbrace>
receive_signal thread cap is_blocking
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: receive_signal_def)
apply (cases cap, simp_all)
apply (rule bind_wp [OF _ get_simple_ko_sp])
apply (wpsimp wp: set_simple_ko_pas_refined set_thread_state_pas_refined
simp: do_nbrecv_failed_transfer_def)
done
subsection\<open>integrity\<close>
subsubsection\<open>autarchy\<close>
text\<open>
For the case when the currently-running thread owns the receiver
(i.e. receiver last to the notification rendezvous or sender owns
receiver).
\<close>
lemma st_tcb_at_tcb_states_of_state:
"(st_tcb_at stf p s) = (\<exists>st. tcb_states_of_state s p = Some st \<and> stf st)"
unfolding tcb_states_of_state_def st_tcb_def2 by auto
lemma st_tcb_at_tcb_states_of_state_eq:
"(st_tcb_at ((=) st) p s) = (tcb_states_of_state s p = Some st)"
unfolding tcb_states_of_state_def st_tcb_def2 by auto
lemma ipc_buffer_has_auth_None [simp]:
"ipc_buffer_has_auth aag receiver None"
unfolding ipc_buffer_has_auth_def by simp
lemma set_notification_respects:
"\<lbrace>integrity aag X st and K (aag_has_auth_to aag auth epptr \<and> auth \<in> {Receive, Notify, Reset})\<rbrace>
set_notification epptr ntfn'
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_simple_ko_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def partial_inv_def a_type_def)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def tro_ntfn integrity_asids_kh_upds)
done
lemma receive_signal_integrity_autarch:
"\<lbrace>integrity aag X st and pas_refined aag and valid_objs and
K ((\<forall>ntfnptr \<in> obj_refs_ac cap. aag_has_auth_to aag Receive ntfnptr) \<and> is_subject aag thread)\<rbrace>
receive_signal thread cap is_blocking
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: receive_signal_def)
apply (cases cap, simp_all)
apply (rule bind_wp [OF _ get_simple_ko_sp])
apply (wpsimp wp: set_notification_respects[where auth=Receive]
set_thread_state_integrity_autarch as_user_integrity_autarch
simp: do_nbrecv_failed_transfer_def)
done
subsubsection\<open>Non-autarchy: the sender is running\<close>
locale Ipc_AC_1 =
fixes aag :: "'a PAS"
assumes arch_derive_cap_auth_derived:
"\<lbrace>\<top>\<rbrace>
arch_derive_cap acap
\<lbrace>\<lambda>rv _ :: det_ext state. rv \<noteq> NullCap \<longrightarrow> auth_derived rv (ArchObjectCap acap)\<rbrace>, -"
and lookup_ipc_buffer_has_auth[wp]:
"\<lbrace>pas_refined aag and valid_objs\<rbrace>
lookup_ipc_buffer True receiver
\<lbrace>\<lambda>rv _. ipc_buffer_has_auth aag receiver rv\<rbrace>"
and cap_insert_ext_integrity_asids[wp]:
"cap_insert_ext a b c d e \<lbrace>integrity_asids aag subjects x asid (st :: det_ext state)\<rbrace>"
and make_fault_message_inv[wp]:
"\<And>P. make_fault_msg ft t \<lbrace>\<lambda>s :: det_ext state. P s\<rbrace>"
and tcb_context_no_change:
"\<exists>ctxt. (tcb :: tcb) = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\<rparr>"
(* This assumption excludes x64 (its valid_arch_state includes caps) *)
and transfer_caps_loop_valid_arch[wp]:
"transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
begin
lemma send_upd_ctxintegrity:
"\<lbrakk> direct_send {pasSubject aag} aag ep tcb
\<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb;
integrity aag X st s; st_tcb_at ((=) Running) thread s;
get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'\<rbrakk>
\<Longrightarrow> integrity aag X st
(s\<lparr>kheap := (kheap s)
(thread \<mapsto> TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))\<rparr>)"
apply (clarsimp simp: integrity_def tcb_states_of_state_preserved st_tcb_def2)
apply (rule conjI)
prefer 2
apply (fastforce dest: get_tcb_ko_atI simp: integrity_asids_kh_upds obj_at_def)
apply (drule get_tcb_SomeD)+
apply (drule spec[where x=thread], simp)
apply (cases "is_subject aag thread")
apply (rule tro_lrefl, solves\<open>simp\<close>)
(* slow 5s *)
by (erule integrity_objE;
(* eliminate all TCB unrelated cases and simplifies the other *)
clarsimp;
(* deal with the orefl case *)
(solves \<open>simp add:direct_send_def indirect_send_def\<close>
(* deal with the other case by applying either the reply,
call or send rules and then the generic rule *)
| rule tro_trans_spec,
(rule tro_tcb_reply'[OF refl refl refl] tro_tcb_call[OF refl refl refl]
tro_tcb_send[OF refl refl refl];
blast),
rule tro_trans_spec,
(rule tro_tcb_generic'[OF refl refl refl]; simp),
rule tro_orefl, simp, rule tcb.equality; solves simp))
lemma as_user_set_register_respects:
"\<lbrace>integrity aag X st and st_tcb_at ((=) Running) thread and
K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st) \<and>
(aag_has_auth_to aag SyncSend ep \<or> aag_has_auth_to aag Notify ep))\<rbrace>
as_user thread (set_register r v)
\<lbrace>\<lambda>_. 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)
apply (cases "is_subject aag thread")
apply (erule (1) integrity_update_autarch [unfolded fun_upd_def])
apply (clarsimp simp: st_tcb_def2)
apply (rule send_upd_ctxintegrity [OF disjI1, unfolded fun_upd_def])
apply (auto simp: direct_send_def st_tcb_def2)
done
end
lemma set_thread_state_respects_in_signalling:
"\<lbrace>\<lambda>s. integrity aag X st s \<and> aag_has_auth_to aag Notify ntfnptr \<and>
(is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s)\<rbrace>
set_thread_state thread Running
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def get_object_def)
apply wp
apply (clarsimp)
apply (cases "is_subject aag thread")
apply (erule(1) integrity_update_autarch [unfolded fun_upd_def])
apply (erule integrity_trans)
apply (drule get_tcb_SomeD)
apply (clarsimp simp: integrity_def st_tcb_def2 integrity_asids_kh_upds)
apply (clarsimp dest!: get_tcb_SomeD)
apply (rule tro_tcb_send [OF refl refl])
apply (rule tcb.equality; simp; rule arch_tcb_context_set_eq[symmetric])
apply (auto simp: indirect_send_def direct_send_def)
done
lemma set_notification_obj_at:
"\<lbrace>obj_at P ptr and K (ptr \<noteq> ntfnptr)\<rbrace>
set_notification ntfnptr queue
\<lbrace>\<lambda>_. obj_at P ptr\<rbrace>"
apply (simp add: set_simple_ko_def set_object_def)
apply (wp get_object_wp)
apply (auto simp: obj_at_def)
done
lemma set_ntfn_valid_objs_at:
"\<lbrace>valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)\<rbrace>
set_notification p ntfn
\<lbrace>\<lambda>rv. valid_objs\<rbrace>"
unfolding set_simple_ko_def
apply (rule hoare_pre)
apply (wp set_object_valid_objs get_object_wp)
apply (clarsimp simp: valid_obj_def obj_at_def is_ntfn partial_inv_def
split: kernel_object.splits)
done
lemma integrity_receive_blocked_chain:
"\<lbrakk> st_tcb_at (receive_blocked_on ep) p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk> \<Longrightarrow> st_tcb_at (receive_blocked_on ep) p st"
apply (clarsimp simp: integrity_def st_tcb_at_tcb_states_of_state)
apply (drule (1) tsos_tro [where p = p] )
apply (fastforce simp: tcb_states_of_state_def)
apply simp
apply simp
done
crunch possible_switch_to
for integrity[wp]: "integrity aag X st"
(ignore: tcb_sched_action)
abbreviation
"integrity_once_ts_upd t ts aag X st s \<equiv>
integrity aag X st (s\<lparr>kheap := (kheap s)(t := Some (TCB ((the (get_tcb t s))\<lparr>tcb_state := ts\<rparr>)))\<rparr>)"
lemma set_scheduler_action_integrity_once_ts_upd:
"set_scheduler_action sa \<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply clarsimp
apply (erule rsubst[where P="\<lambda>x. x"])
apply (rule trans, rule_tac f="\<lambda>x. sa" in eintegrity_sa_update[symmetric])
apply (rule arg_cong[where f="integrity aag X st"])
apply (simp add: get_tcb_def)
done
crunch set_thread_state_ext
for integrity_once_ts_upd: "integrity_once_ts_upd t ts aag X st"
lemma set_thread_state_integrity_once_ts_upd:
"set_thread_state t ts' \<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace>"
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp set_thread_state_ext_integrity_once_ts_upd)
apply (clarsimp simp: fun_upd_def dest!: get_tcb_SomeD)
apply (simp add: get_tcb_def cong: if_cong)
done
lemma get_tcb_recv_blocked_implies_receive:
"\<lbrakk> pas_refined aag s; get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb) \<rbrakk>
\<Longrightarrow> abs_has_auth_to aag Receive t ep"
apply (erule pas_refined_mem[rotated])
apply (rule sta_ts)
apply (simp add: thread_st_auth_def tcb_states_of_state_def)
apply (case_tac "tcb_state tcb", simp_all)
done
lemma cancel_ipc_receive_blocked_respects:
"\<lbrace>integrity aag X st and pas_refined aag and st_tcb_at (receive_blocked) t and
(sym_refs o state_refs_of) and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and
K (abs_has_auth_to aag Receive t ntfnptr \<and> aag_has_auth_to aag Notify ntfnptr)\<rbrace>
cancel_ipc t
\<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace>"
apply (clarsimp simp: cancel_ipc_def bind_assoc)
apply (rule bind_wp[OF _ gts_sp])
apply (rule hoare_name_pre_state)
apply (subgoal_tac "case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False")
apply (simp add: blocked_cancel_ipc_def bind_assoc set_simple_ko_def set_object_def
get_ep_queue_def get_blocking_object_def
split: thread_state.splits)
apply (rule hoare_pre)
apply (wp set_thread_state_integrity_once_ts_upd get_object_wp get_simple_ko_wp
| wpc)+
apply (clarsimp simp: st_tcb_at_def2 obj_at_def)
apply (rename_tac ep payload s tcb ntfn)
apply (drule_tac t="tcb_state tcb" in sym)
apply (subgoal_tac "st_tcb_at ((=) (tcb_state tcb)) t s")
apply (drule(1) sym_refs_st_tcb_atD)
apply (clarsimp simp: obj_at_def ep_q_refs_of_def fun_upd_def get_tcb_def
split: endpoint.splits cong: if_cong)
apply (intro impI conjI, simp_all)[1]
apply (erule integrity_trans)
apply (simp add: integrity_def)
apply (intro impI conjI allI)
apply clarsimp
apply (rule tro_ep_unblock; simp?)
apply (erule get_tcb_recv_blocked_implies_receive, erule get_tcb_rev; solves\<open>simp\<close>)
apply (rule_tac ep=ep in tro_tcb_send[OF refl refl];
fastforce intro!: tcb.equality arch_tcb_context_set_eq[symmetric]
simp: indirect_send_def pred_tcb_at_def obj_at_def)
apply (fastforce simp: integrity_asids_kh_upds)
apply (fastforce simp: indirect_send_def pred_tcb_at_def obj_at_def)
apply (fastforce simp: pred_tcb_at_def obj_at_def receive_blocked_def)
done
lemma set_thread_state_integrity':
"\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def)
by (wpsimp wp: set_object_wp)
context Ipc_AC_1 begin
lemma as_user_set_register_respects_indirect:
"\<lbrace>integrity aag X st and st_tcb_at ((=) 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 (set_register r v)
\<lbrace>\<lambda>_. 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 )
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])
by (auto simp: st_tcb_def2 indirect_send_def pred_tcb_def2 dest: sym)
end
lemma integrity_receive_blocked_chain':
"\<lbrakk> st_tcb_at receive_blocked p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk>
\<Longrightarrow> st_tcb_at receive_blocked p st"
apply (clarsimp simp: integrity_def st_tcb_at_tcb_states_of_state receive_blocked_def)
apply (simp split: thread_state.split_asm)
apply (rename_tac word pl)
apply (drule_tac ep=word in tsos_tro [where p = p], simp+ )
done
lemma tba_Some:
"thread_bound_ntfns s t = Some a \<Longrightarrow> bound_tcb_at ((=) (Some a)) t s"
by (clarsimp simp: thread_bound_ntfns_def pred_tcb_at_def obj_at_def get_tcb_def
split: option.splits kernel_object.splits)
lemma tsos_tro':
"\<lbrakk> \<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x);
thread_bound_ntfns s' p = Some a; pasObjectAbs aag p \<notin> subjects \<rbrakk>
\<Longrightarrow> thread_bound_ntfns s p = Some a"
apply (drule_tac x=p in spec)
apply (erule integrity_objE;
simp?;
fastforce simp: thread_bound_ntfns_def get_tcb_def
tcb_bound_notification_reset_integrity_def)
done
lemma integrity_receive_blocked_chain_bound:
"\<lbrakk> bound_tcb_at ((=) (Some ntfnptr)) p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk>
\<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) p st"
apply (clarsimp simp: integrity_def)
apply (drule bound_tcb_at_thread_bound_ntfns)
apply (drule tsos_tro' [where p = p], simp+ )
apply (clarsimp simp:tba_Some)
done
context Ipc_AC_1 begin
lemma send_signal_respects:
"\<lbrace>integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of
and K (aag_has_auth_to aag Notify ntfnptr)\<rbrace>
send_signal ntfnptr badge
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: send_signal_def)
apply (rule bind_wp[OF _ get_simple_ko_sp])
apply (rule hoare_name_pre_state)
apply (case_tac "ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None")
\<comment> \<open>ntfn-binding case\<close>
apply (rule hoare_pre)
apply (wp set_notification_respects[where auth=Notify]
as_user_set_register_respects_indirect[where ntfnptr=ntfnptr]
set_thread_state_integrity' sts_st_tcb_at' hoare_weak_lift_imp
cancel_ipc_receive_blocked_respects[where ntfnptr=ntfnptr]
gts_wp
| wpc | simp)+
apply (clarsimp, rule conjI, clarsimp simp: st_tcb_def2)
apply (clarsimp simp: receive_blocked_def)
apply (simp split: thread_state.split_asm)
apply (clarsimp simp: obj_at_def)
apply (drule (3) ntfn_bound_tcb_at[where ntfnptr=ntfnptr and P="\<lambda>ntfn. ntfn = Some ntfnptr"], simp+)[1]
apply (rule conjI)
apply (drule_tac x=ntfnptr and t=y in bound_tcb_at_implies_receive)
apply (clarsimp simp: pred_tcb_at_def obj_at_def, simp)
apply clarsimp
apply (rule conjI)
apply (rule_tac s=sa in integrity_receive_blocked_chain')
apply (clarsimp simp add: pred_tcb_at_def obj_at_def receive_blocked_def)
apply (fastforce split: thread_state.split)
apply simp+
apply (rule_tac s=sa in integrity_receive_blocked_chain_bound)
apply (clarsimp simp: pred_tcb_at_def obj_at_def)
apply simp+
apply (rule hoare_pre)
apply clarsimp
apply (wpc, clarsimp)
apply (wp set_notification_respects[where auth=Notify]
sts_st_tcb_at' as_user_set_register_respects
set_thread_state_pas_refined set_simple_ko_pas_refined
set_thread_state_respects_in_signalling [where ntfnptr = ntfnptr]
set_ntfn_valid_objs_at hoare_vcg_disj_lift hoare_weak_lift_imp
| wpc
| simp add: update_waiting_ntfn_def)+
apply clarsimp
apply (subgoal_tac "st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa")
prefer 2
apply (rule ntfn_queued_st_tcb_at', assumption)
apply (fastforce simp: obj_at_def valid_obj_def valid_ntfn_def)
apply assumption+
apply simp
apply simp
apply (intro impI conjI)
\<comment> \<open>st_tcb_at receive_blocked st\<close>
apply (erule (2) integrity_receive_blocked_chain)
apply clarsimp
done
end
section\<open>Sync IPC\<close>
text\<open>
When transferring caps, i.e. when the grant argument is true on the
IPC operations, the currently-running thread owns the receiver. Either
it is the receiver (and ?thesis by well-formedness) or it is the
sender, and that can send arbitrary caps, hence ?thesis by sbta_ipc
etc.
\<close>
subsection\<open>auxiliary\<close>
lemma cap_master_cap_masked_as_full:
"cap_master_cap (masked_as_full a a) = cap_master_cap a "
by (clarsimp simp: cap_master_cap_def masked_as_full_def split: cap.splits)
lemma cap_badge_masked_as_full:
"(cap_badge (masked_as_full a a), cap_badge a) \<in> capBadge_ordering False"
by (cases a, simp_all add: masked_as_full_def)
lemma masked_as_full_double:
"masked_as_full (masked_as_full ab ab) cap' = masked_as_full ab ab"
by (cases ab, simp_all add: masked_as_full_def)
lemma transfer_caps_loop_pres_dest_aux:
assumes x: "\<And>cap src dest.
\<lbrace>\<lambda>s. P s \<and> dest \<in> slots' \<and> src \<in> snd ` caps' \<and> valid_objs s \<and> real_cte_at dest s \<and>
s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and>
cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap\<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>_. P\<rbrace>"
assumes eb: "\<And>b n'. n' \<le> N \<Longrightarrow> set_extra_badge buffer b n' \<lbrace>P\<rbrace>"
shows "n + length caps \<le> N \<Longrightarrow>
\<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> valid_objs s \<and>
valid_mdb s \<and> distinct slots \<and> (\<forall>x \<in> set slots. real_cte_at x s) \<and>
(\<forall>x \<in> set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and>
cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x
\<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>_. P\<rbrace>" (is "?L \<Longrightarrow> ?P n caps slots mi")
proof (induct caps arbitrary: slots n mi)
case Nil
thus ?case by (simp, wp, simp)
next
case (Cons m ms)
hence nN: "n \<le> N" by simp
from Cons have "\<And>slots mi. ?P (n + 1) ms slots mi" by clarsimp
thus ?case
apply (cases m)
apply (clarsimp simp add: Let_def split_def whenE_def
cong: if_cong list.case_cong split del: if_split)
apply (rule hoare_pre)
apply (wp eb [OF nN] hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift
| assumption | simp split del: if_split)+
apply (rule cap_insert_assume_null)
apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at)+
(* cannot blindly use derive_cap_is_derived_foo here , need to first hoist
out of the postcondition the conjunct that the return value is derived,
and solve this using derived_cap_is_derived, and then solve the rest
using derive_cap_is_derived_foo *)
apply (rule_tac Q'="\<lambda>r s. S r s \<and> Q r s" for S Q in hoare_strengthen_postE_R)
apply (rule hoare_vcg_conj_liftE_R)
apply (rule derive_cap_is_derived)
prefer 2
apply clarsimp
apply assumption
apply (wp derive_cap_is_derived_foo)+
apply (simp only: tl_drop_1[symmetric])
apply (clarsimp simp: cte_wp_at_caps_of_state
ex_cte_cap_to_cnode_always_appropriate_strg
real_cte_tcb_valid caps_of_state_valid
split del: if_split)
apply (clarsimp simp: remove_rights_def caps_of_state_valid
neq_Nil_conv cte_wp_at_caps_of_state
imp_conjR[symmetric] cap_master_cap_masked_as_full
cap_badge_masked_as_full
split del: if_split)
apply (intro conjI)
apply clarsimp
apply (case_tac "cap = a",clarsimp simp: remove_rights_def)
apply (clarsimp simp:masked_as_full_def is_cap_simps)
apply (clarsimp simp: cap_master_cap_simps remove_rights_def split:if_splits)
apply clarsimp
apply (intro conjI)
apply (clarsimp split:if_splits elim!: image_eqI[rotated])
apply (clarsimp split:if_splits simp: remove_rights_def)
apply (rule ballI)
apply (drule(1) bspec)
apply clarsimp
apply (intro conjI)
apply clarsimp
apply clarsimp
apply (case_tac "capa = ab",clarsimp simp: masked_as_full_def is_cap_simps split: if_splits)
apply (clarsimp simp: masked_as_full_double)
done
qed
(* FIXME: move *)
lemma transfer_caps_loop_pres_dest:
assumes x: "\<And>cap src dest.
\<lbrace>\<lambda>s. P s \<and> dest \<in> set slots \<and> src \<in> snd ` set caps \<and> valid_objs s \<and>
real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and>
cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap \<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>_. P\<rbrace>"
assumes eb: "\<And>b n'. n' \<le> n + length caps \<Longrightarrow> \<lbrace>P\<rbrace> set_extra_badge buffer b n' \<lbrace>\<lambda>_. P\<rbrace>"
shows "\<lbrace>\<lambda>s. P s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x \<in> set slots. real_cte_at x s) \<and>
(\<forall>x \<in> set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and>
cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x
\<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>_. P\<rbrace>"
apply (rule hoare_pre)
apply (rule transfer_caps_loop_pres_dest_aux [OF x eb])
apply assumption
apply simp
apply simp
done
subsection\<open>pas_refined\<close>
lemma lookup_slot_for_thread_authorised:
"\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
lookup_slot_for_thread thread cref
\<lbrace>\<lambda>rv _. is_subject aag (fst (fst rv))\<rbrace>,-"
unfolding lookup_slot_for_thread_def
apply wp
apply (clarsimp simp: owns_thread_owns_cspace)
done
lemma cnode_cap_all_auth_owns:
"(\<exists>s. is_cnode_cap cap \<and> pas_refined aag s \<and>
(\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. aag_has_auth_to aag auth x))
\<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)"
apply (clarsimp simp: is_cap_simps)
apply (clarsimp simp: cap_auth_conferred_def pas_refined_all_auth_is_owns)
done
lemma get_receive_slots_authorised:
"\<lbrace>pas_refined aag and K (\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver)\<rbrace>
get_receive_slots receiver recv_buf
\<lbrace>\<lambda>rv _. \<forall>slot \<in> set rv. is_subject aag (fst slot)\<rbrace>"
apply (rule hoare_gen_asm)
apply (cases recv_buf)
apply (simp, wp, simp)
apply clarsimp
apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
| rule hoare_drop_imps
| simp add: lookup_cap_def split_def)+
apply (strengthen cnode_cap_all_auth_owns, simp add: aag_cap_auth_def)
apply (wp hoare_vcg_all_liftE_R hoare_drop_imps)+
apply clarsimp
apply (fastforce simp: is_cap_simps)
done
crunch set_extra_badge
for pas_refined[wp]: "pas_refined aag"
lemma remove_rights_clas[simp]:
"cap_links_asid_slot aag p (remove_rights R cap) = cap_links_asid_slot aag p cap"
unfolding cap_links_asid_slot_def remove_rights_def cap_rights_update_def
by (clarsimp split: cap.splits)
lemma remove_rights_cap_auth_conferred_subset:
"x \<in> cap_auth_conferred (remove_rights R cap) \<Longrightarrow> x \<in> cap_auth_conferred cap"
unfolding remove_rights_def cap_rights_update_def
apply (clarsimp split: if_split_asm cap.splits bool.splits
simp: cap_auth_conferred_def
validate_vm_rights_def vm_read_only_def vm_kernel_only_def)
apply (erule set_mp [OF cap_rights_to_auth_mono, rotated], clarsimp)+
apply (fastforce simp: cap_rights_to_auth_def reply_cap_rights_to_auth_def)
apply (simp add: Diff_eq)
apply (erule set_rev_mp[OF _ acap_auth_conferred_acap_rights_update])
done
lemma remove_rights_cli[simp]:
"cap_links_irq aag l (remove_rights R cap) = cap_links_irq aag l cap"
unfolding remove_rights_def cap_rights_update_def
by (clarsimp split: cap.splits simp: cap_links_irq_def)
lemma remove_rights_untyped_range[simp]:
"untyped_range (remove_rights R c) = untyped_range c"
unfolding remove_rights_def cap_rights_update_def
by (clarsimp split: cap.splits simp: cap_links_irq_def)
lemma obj_refs_remove_rights[simp]:
"obj_refs_ac (remove_rights rs cap) = obj_refs_ac cap"
unfolding remove_rights_def
by (cases cap, simp_all add: cap_rights_update_def)
lemma remove_rights_cur_auth:
"pas_cap_cur_auth aag cap \<Longrightarrow> pas_cap_cur_auth aag (remove_rights R cap)"
unfolding aag_cap_auth_def
by (clarsimp dest!: remove_rights_cap_auth_conferred_subset)
(* FIXME MOVE *)
lemmas hoare_gen_asmE2 = hoare_gen_asmE[where P'=\<top>,simplified pred_top_left_neutral]
lemma derive_cap_is_transferable:
"\<lbrace>K (is_transferable_cap cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv _. is_transferable_cap rv\<rbrace>, -"
apply (rule hoare_gen_asmE2)
by (erule is_transferable_capE; wpsimp simp: derive_cap_def)
lemma auth_derived_refl[simp]:
"auth_derived cap cap"
by (simp add: auth_derived_def)
crunch set_extra_badge
for valid_arch_state[wp]: valid_arch_state
context Ipc_AC_1 begin
lemma derive_cap_auth_derived:
"\<lbrace>\<top>\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s :: det_ext state. rv \<noteq> NullCap \<longrightarrow> auth_derived rv cap\<rbrace>, -"
by (cases cap; wpsimp wp: arch_derive_cap_auth_derived simp: derive_cap_def)
(* FIXME MOVE *)
lemma auth_derived_pas_cur_auth:
"\<lbrakk> auth_derived cap cap'; pas_cap_cur_auth aag cap' \<rbrakk>
\<Longrightarrow> pas_cap_cur_auth aag cap"
by (force simp: aag_cap_auth_def auth_derived_def cap_links_asid_slot_def cap_links_irq_def)
lemma derive_cap_is_derived_foo':
"\<lbrace>\<lambda>s :: det_ext state.
\<forall>cap'. (valid_objs s \<and> cap' \<noteq> NullCap \<and>
cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and>
(cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and>
cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s
\<longrightarrow> cte_at slot s) \<and>
(s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and>
(cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and>
\<not> is_zombie cap \<and> cap \<noteq> IRQControlCap)
\<longrightarrow> Q cap' s\<rbrace>
derive_cap slot cap
\<lbrace>Q\<rbrace>, -"
apply (clarsimp simp: validE_R_def validE_def valid_def split: sum.splits)
apply (frule in_inv_by_hoareD[OF derive_cap_inv], clarsimp)
apply (erule allE)
apply (erule impEM)
apply (frule use_validE_R[OF _ cap_derive_not_null_helper, OF _ _ imp_refl])
apply (rule derive_cap_inv[THEN valid_validE_R])
apply (intro conjI)
apply (clarsimp simp: cte_wp_at_caps_of_state)+
apply (erule(1) use_validE_R[OF _ derive_cap_valid_cap])
apply simp
apply (erule use_validE_R[OF _ derive_cap_auth_derived],simp)
apply simp
done
(* FIXME: cleanup *)
lemma transfer_caps_loop_presM_extended:
fixes P vo em ex buffer slots caps n mi
assumes x: "\<And>cap src dest.
\<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s
\<and> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s
\<and> s \<turnstile> cap \<and> Psrc src \<and> Pdest dest \<and> Pcap cap
\<and> tcb_cap_valid cap dest s \<and> real_cte_at src s
\<and> cte_wp_at (is_derived (cdt s) src cap) src s
\<and> cap \<noteq> NullCap)
\<and> (em \<longrightarrow> cte_wp_at ((=) NullCap) dest s)
\<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>_ s :: det_ext state. P s\<rbrace>"
assumes eb: "\<And>b n. set_extra_badge buffer b n \<lbrace>P\<rbrace>"
assumes pcap_auth_derived: "\<And>cap cap'. \<lbrakk> auth_derived cap cap'; Pcap cap' \<rbrakk> \<Longrightarrow> Pcap cap"
shows "\<lbrace>\<lambda>s. P s \<and> (vo \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s
\<and> valid_objs s \<and> valid_mdb s \<and> distinct slots
\<and> (\<forall>x \<in> set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s
\<and> real_cte_at x s \<and> Pdest x)
\<and> (\<forall>x \<in> set caps. valid_cap (fst x) s \<and> Psrc (snd x) \<and> Pcap (fst x)
\<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x
\<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s
\<and> real_cte_at (snd x) s))
\<and> (ex \<longrightarrow> (\<forall>x \<in> set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>_. P\<rbrace>"
apply (induct caps arbitrary: slots n mi)
apply (simp, wp, simp)
apply (clarsimp simp add: Let_def split_def whenE_def
cong: if_cong list.case_cong split del: if_split)
apply (rule hoare_pre)
apply (wp eb hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift hoare_weak_lift_imp
| assumption | simp split del: if_split)+
apply (rule cap_insert_assume_null)
apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at hoare_weak_lift_imp)+
apply (rule hoare_vcg_conj_liftE_R')
apply (rule derive_cap_is_derived_foo')
apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> NullCap \<longrightarrow>
cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s) \<and>
(cap'\<noteq> NullCap \<longrightarrow> QM s cap')" for QM in hoare_strengthen_postE_R)
prefer 2
apply clarsimp
apply assumption
apply (rule hoare_vcg_conj_liftE_R')
apply (rule hoare_vcg_const_imp_liftE_R)
apply (rule derive_cap_is_derived)
apply (wp derive_cap_is_derived_foo')+
apply (clarsimp simp: cte_wp_at_caps_of_state
ex_cte_cap_to_cnode_always_appropriate_strg
real_cte_tcb_valid caps_of_state_valid
split del: if_split)
apply (clarsimp simp: remove_rights_def caps_of_state_valid
neq_Nil_conv cte_wp_at_caps_of_state
imp_conjR[symmetric] conj_comms
split del: if_split)
apply (rule conjI)
apply clarsimp
apply (case_tac "cap = a",clarsimp)
apply (clarsimp simp:masked_as_full_def is_cap_simps)
apply (fastforce simp: cap_master_cap_simps split: if_splits)
apply (clarsimp split del: if_split)
apply (intro conjI)
apply (fastforce split: if_split elim!: pcap_auth_derived)
apply (fastforce)
apply (clarsimp)
apply (rule ballI)
apply (drule(1) bspec)
apply clarsimp
apply (intro conjI)
apply (case_tac "capa = ac",clarsimp+)
apply (case_tac "capa = ac")
by (clarsimp simp: masked_as_full_def is_cap_simps split: if_splits)+
lemma transfer_caps_loop_pas_refined:
"\<lbrace>\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and>
valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and>
(\<forall>x \<in> set caps. valid_cap (fst x) s \<and> real_cte_at (snd x) s
\<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and>
(\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and>
(\<forall>slot \<in> set slots. is_subject aag (fst slot)) \<and>
(\<forall>x \<in> set caps. is_subject aag (fst (snd x)) \<and>
pas_cap_cur_auth aag (fst x)) \<and> distinct slots\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_pre)
apply (rule transfer_caps_loop_presM_extended
[where vo=True and em=True and ex=False and
Psrc="\<lambda>slot . is_subject aag (fst slot)" and
Pcap="pas_cap_cur_auth aag" and
Pdest="\<lambda>slot . is_subject aag (fst slot)"])
apply (wp cap_insert_pas_refined)
apply (fastforce simp: cte_wp_at_caps_of_state elim!: is_derived_is_transferable)
apply (rule set_extra_badge_pas_refined)
apply (erule(1) auth_derived_pas_cur_auth)
apply (fastforce elim: cte_wp_at_weakenE)
done
lemma transfer_caps_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs
and valid_arch_state and valid_objs and valid_mdb
and (\<lambda>s. (\<forall>x \<in> set caps. valid_cap (fst x) s
\<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s
\<and> real_cte_at (snd x) s))
and K (is_subject aag receiver \<and>
(\<forall>x \<in> set caps. is_subject aag (fst (snd x))) \<and>
(\<forall>x \<in> set caps. pas_cap_cur_auth aag (fst x)))\<rbrace>
transfer_caps info caps endpoint receiver recv_buf
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
unfolding transfer_caps_def
by (wp transfer_caps_loop_pas_refined get_receive_slots_authorised get_recv_slot_inv
hoare_vcg_const_imp_lift hoare_vcg_all_lift grs_distinct
| wpc | simp del: get_receive_slots.simps add: ball_conj_distrib)+
end
lemma copy_mrs_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
copy_mrs sender sbuf receiver rbuf n
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
unfolding copy_mrs_def
apply (rule_tac Q'="\<lambda>_. pas_refined aag and pspace_aligned
and valid_vspace_objs
and valid_arch_state"
in hoare_strengthen_post[rotated], clarsimp)
apply (wpsimp wp: mapM_wp_inv)
done
lemma lookup_cap_and_slot_authorised:
"\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
lookup_cap_and_slot thread xs
\<lbrace>\<lambda>rv _. is_subject aag (fst (snd rv))\<rbrace>, -"
unfolding lookup_cap_and_slot_def
by (wp lookup_slot_for_thread_authorised | simp add: split_def)+
lemma lookup_extra_caps_authorised:
"\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
lookup_extra_caps thread buffer mi
\<lbrace>\<lambda>rv _. \<forall>cap \<in> set rv. is_subject aag (fst (snd cap))\<rbrace>, -"
unfolding lookup_extra_caps_def
by (wpsimp wp: mapME_set lookup_cap_and_slot_authorised)
lemma lookup_cap_and_slot_cur_auth:
"\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
lookup_cap_and_slot thread xs
\<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>, -"
unfolding lookup_cap_and_slot_def
by (wp get_cap_auth_wp [where aag = aag] lookup_slot_for_thread_authorised | simp add: split_def)+
lemma lookup_extra_caps_auth:
"\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
lookup_extra_caps thread buffer mi
\<lbrace>\<lambda>rv _. \<forall>cap \<in> set rv. pas_cap_cur_auth aag (fst cap)\<rbrace>, -"
unfolding lookup_extra_caps_def
by (wpsimp wp: mapME_set lookup_cap_and_slot_cur_auth)
lemma transfer_caps_empty_inv:
"transfer_caps mi [] endpoint receiver rbuf \<lbrace>P\<rbrace>"
unfolding transfer_caps_def by wpsimp
lemma lcs_valid':
"\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread xs \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, -"
unfolding lookup_cap_and_slot_def by wpsimp
lemma lec_valid_cap':
"\<lbrace>valid_objs\<rbrace> lookup_extra_caps thread xa mi \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. s \<turnstile> fst x)\<rbrace>, -"
unfolding lookup_extra_caps_def
by (wpsimp wp: mapME_set lcs_valid')
(* FIXME: MOVE *)
lemma hoare_conjDR1:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -"
by (simp add:validE_def validE_R_def valid_def) blast
lemma hoare_conjDR2:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -"
by (simp add:validE_def validE_R_def valid_def) blast
context Ipc_AC_1 begin
crunch do_fault_transfer
for pas_refined[wp]: "\<lambda>s :: det_ext state. pas_refined aag s"
crunch transfer_caps, copy_mrs
for valid_arch_state[wp]: "valid_arch_state :: det_ext state \<Rightarrow> _"
(wp: crunch_wps)
lemma do_normal_transfer_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
and valid_objs and valid_mdb
and K (grant \<longrightarrow> is_subject aag sender)
and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace>
do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
proof(cases grant)
case True thus ?thesis
apply -
apply (rule hoare_gen_asm)
apply (simp add: do_normal_transfer_def)
by (wpsimp wp: copy_mrs_pas_refined transfer_caps_pas_refined
lec_valid_cap' copy_mrs_cte_wp_at hoare_vcg_ball_lift
lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR1]
lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR2]
lookup_extra_caps_authorised lookup_extra_caps_auth
simp: ball_conj_distrib)
next
case False thus ?thesis
apply (simp add: do_normal_transfer_def)
by (wpsimp wp: copy_mrs_pas_refined copy_mrs_cte_wp_at transfer_caps_empty_inv)
qed
lemma do_ipc_transfer_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
and valid_objs and valid_mdb
and K (grant \<longrightarrow> is_subject aag sender)
and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace>
do_ipc_transfer sender ep badge grant receiver
\<lbrace>\<lambda>_ s :: det_ext state. pas_refined aag s\<rbrace>"
unfolding do_ipc_transfer_def
by (wpsimp wp: do_normal_transfer_pas_refined hoare_vcg_all_lift hoare_drop_imps)
end
(* FIXME MOVE*)
lemma cap_insert_pas_refined_transferable:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
K (is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and>
abs_has_auth_to aag DeleteDerived (fst src_slot) (fst dest_slot))\<rbrace>
cap_insert new_cap src_slot dest_slot
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: cap_insert_def)
apply (rule hoare_pre)
apply (wp set_cap_pas_refined set_cdt_pas_refined update_cdt_pas_refined hoare_vcg_imp_lift
hoare_weak_lift_imp hoare_vcg_all_lift set_cap_caps_of_state2
set_untyped_cap_as_full_cdt_is_original_cap get_cap_wp
tcb_domain_map_wellformed_lift hoare_vcg_disj_lift
set_untyped_cap_as_full_is_transferable'
| simp split del: if_split del: split_paired_All fun_upd_apply
| strengthen update_one_strg)+
by (fastforce split: if_split_asm
simp: cte_wp_at_caps_of_state pas_refined_refl valid_mdb_def2
mdb_cte_at_def Option.is_none_def
simp del: split_paired_All
dest: aag_cdt_link_Control aag_cdt_link_DeleteDerived cap_auth_caps_of_state
intro: aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed])
lemma setup_caller_cap_pas_refined:
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
K ((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and>
abs_has_auth_to aag Reply receiver sender)\<rbrace>
setup_caller_cap sender receiver grant
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: setup_caller_cap_def)
apply (rule conjI)
(* if grant *)
apply clarsimp
apply (wpsimp wp: cap_insert_pas_refined set_thread_state_pas_refined)
apply (fastforce simp: aag_cap_auth_def clas_no_asid cli_no_irqs pas_refined_refl)
(* if not grant *)
apply clarsimp
apply (wp cap_insert_pas_refined_transferable set_thread_state_pas_refined)
by (fastforce simp: aag_cap_auth_def cap_links_irq_def cap_links_asid_slot_def
cap_auth_conferred_def reply_cap_rights_to_auth_def