-
Notifications
You must be signed in to change notification settings - Fork 109
/
Copy pathIpc_IF.thy
2230 lines (1995 loc) · 101 KB
/
Ipc_IF.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 2022, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory Ipc_IF
imports ArchFinalise_IF
begin
section "reads_respects"
subsection "Notifications"
definition ipc_buffer_has_read_auth :: "'a PAS \<Rightarrow> 'a \<Rightarrow> obj_ref option \<Rightarrow> bool" where
"ipc_buffer_has_read_auth aag l \<equiv>
case_option True
(\<lambda>buf'. is_aligned buf' msg_align_bits \<and>
(\<forall>x \<in> ptr_range buf' msg_align_bits. (l,Read,pasObjectAbs aag x) \<in> (pasPolicy aag)))"
abbreviation aag_can_read_or_affect where
"aag_can_read_or_affect aag l x \<equiv>
aag_can_read aag x \<or> aag_can_affect aag l x"
lemma get_cap_reads_respects:
"reads_respects aag l (K (aag_can_read aag (fst slot) \<or> aag_can_affect aag l (fst slot))) (get_cap slot)"
apply (simp add: get_cap_def split_def)
apply (wp get_object_reads_respects | wpc | simp)+
done
lemma set_thread_state_ext_runnable_equiv_but_for_labels:
"\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and st_tcb_at runnable thread\<rbrace>
set_thread_state_ext thread
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
apply (simp add: set_thread_state_ext_def)
apply (wp gts_wp | rule hoare_pre_cont)+
apply (force simp: st_tcb_at_def obj_at_def)
done
definition all_to_which_has_auth where
"all_to_which_has_auth aag auth source \<equiv> {t. (source,auth,t) \<in> pasPolicy aag}"
definition all_with_auth_to where
"all_with_auth_to aag auth target \<equiv> {x. (x, auth, target) \<in> pasPolicy aag}"
lemma valid_ntfn_WaitingNtfn_tl:
"\<lbrakk> ntfn_obj ntfn = (WaitingNtfn list); valid_ntfn ntfn s;
tl list \<noteq> []; ntfn' = ntfn\<lparr>ntfn_obj := (WaitingNtfn (tl list))\<rparr> \<rbrakk>
\<Longrightarrow> valid_ntfn ntfn' s"
apply (case_tac list, simp_all)
apply (rename_tac a lista)
apply (case_tac lista, simp_all)
apply (clarsimp simp: valid_ntfn_def split: option.splits)
done
lemma tcb_sched_action_equiv_but_for_labels:
"\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and pas_refined aag\<rbrace>
tcb_sched_action action thread
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: etcb_at_def equiv_but_for_labels_def split: option.splits)
apply (rule states_equiv_forI)
apply (fastforce intro!: equiv_forI elim!: states_equiv_forE dest: equiv_forD[where f=kheap])
apply (simp add: states_equiv_for_def)
apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt])
apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ekheap])
apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt_list])
apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=is_original_cap])
apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_states])
apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_irq_node])
apply (fastforce simp: equiv_asids_def elim: states_equiv_forE)
apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def split: option.splits)
apply (rule equiv_forI)
apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ready_queues])
apply (force intro: domtcbs)
done
lemma possible_switch_to_equiv_but_for_labels:
"\<lbrace>equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s)
and K (pasObjectAbs aag target \<in> L) and pas_refined aag\<rbrace>
possible_switch_to target
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
apply (simp add: possible_switch_to_def)
apply (wp tcb_sched_action_equiv_but_for_labels)
(* possible_switch_to does not modify scheduler action if target is in different domain *)
apply (rule hoare_pre_cont)
apply (wp tcb_sched_action_equiv_but_for_labels)
apply (rule hoare_pre_cont)
apply (wp tcb_sched_action_equiv_but_for_labels)+
apply (clarsimp simp: etcb_at_def split: option.splits)
done
crunch set_thread_state_ext, set_thread_state, set_simple_ko
for etcb_at_cdom[wp]: "\<lambda>s. etcb_at (P (cur_domain s)) t s"
(wp: crunch_wps)
locale Ipc_IF_1 =
fixes aag :: "'a subject_label PAS"
assumes lookup_ipc_buffer_reads_respects:
"reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread))
(lookup_ipc_buffer is_receiver thread)"
and as_user_equiv_but_for_labels:
"\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace>
as_user thread (f :: unit user_monad)
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
and storeWord_equiv_but_for_labels:
"\<lbrace>\<lambda>ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>) \<and>
for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) p\<rbrace>
storeWord p v
\<lbrace>\<lambda>_ ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>"
and set_thread_state_runnable_equiv_but_for_labels:
"runnable tst
\<Longrightarrow> \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace>
set_thread_state thread tst
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
and set_endpoint_equiv_but_for_labels:
"\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag epptr \<in> L)\<rbrace>
set_endpoint epptr ep
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
and lookup_ipc_buffer_has_read_auth:
"\<lbrace>pas_refined aag and valid_objs\<rbrace>
lookup_ipc_buffer is_receiver thread
\<lbrace>\<lambda>rv _. ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrace>"
and dmo_loadWord_reads_respects:
"reads_respects aag l (K (for_each_byte_of_word (\<lambda> x. aag_can_read_or_affect aag l x) p))
(do_machine_op (loadWord p))"
and arch_derive_cap_reads_respects:
"reads_respects aag l \<top> (arch_derive_cap acap)"
and arch_derive_cap_rev:
"reads_equiv_valid_inv A aag \<top> (arch_derive_cap acap)"
and cptrs_in_ipc_buffer:
"\<lbrakk> n \<in> set [buffer_cptr_index ..< buffer_cptr_index + unat (mi_extra_caps mi)];
is_aligned p msg_align_bits;
buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
\<Longrightarrow> ptr_range (p + of_nat n * of_nat word_size) word_size_bits \<subseteq> ptr_range p msg_align_bits"
and msg_in_ipc_buffer:
"\<lbrakk> n = msg_max_length \<or> n < msg_max_length; is_aligned p msg_align_bits;
unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
\<Longrightarrow> ptr_range (p + of_nat n * of_nat word_size) word_size_bits \<subseteq> ptr_range p msg_align_bits"
and captransfer_in_ipc_buffer:
"\<lbrakk> is_aligned (buf :: obj_ref) msg_align_bits; p \<in> {0..2} \<rbrakk>
\<Longrightarrow> ptr_range (buf + (2 + (of_nat msg_max_length + of_nat msg_max_extra_caps))
* word_size + p * word_size) word_size_bits
\<subseteq> ptr_range buf msg_align_bits"
and mrs_in_ipc_buffer:
"\<lbrakk> n \<in> set [length msg_registers + 1 ..< Suc n'];
is_aligned buf msg_align_bits; n' < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
\<Longrightarrow> ptr_range (buf + of_nat n * of_nat word_size) word_size_bits
\<subseteq> ptr_range buf msg_align_bits"
and complete_signal_reads_respects:
"pas_domains_distinct aag
\<Longrightarrow> reads_respects aag l (K (aag_can_read aag nptr \<or> aag_can_affect aag l nptr))
(complete_signal nptr receiver)"
and handle_arch_fault_reply_reads_respects:
"reads_respects aag l (K (aag_can_read aag thread)) (handle_arch_fault_reply afault thread x y)"
and arch_get_sanitise_register_info_reads_respects[wp]:
"reads_respects aag l \<top> (arch_get_sanitise_register_info t)"
and arch_get_sanitise_register_info_valid_global_objs[wp]:
"arch_get_sanitise_register_info t \<lbrace>\<lambda>s :: det_state. valid_global_objs s\<rbrace>"
and handle_arch_fault_reply_valid_global_objs[wp]:
"handle_arch_fault_reply vmf thread x y \<lbrace>\<lambda>s :: det_state. valid_global_objs s\<rbrace>"
and lookup_ipc_buffer_ptr_range':
"\<lbrace>valid_objs\<rbrace>
lookup_ipc_buffer True t
\<lbrace>\<lambda>rv s :: det_state. rv = Some buf' \<longrightarrow> auth_ipc_buffers s t = ptr_range buf' msg_align_bits\<rbrace>"
and lookup_ipc_buffer_aligned':
"\<lbrace>valid_objs\<rbrace>
lookup_ipc_buffer True t
\<lbrace>\<lambda>rv s :: det_state. rv = Some buf' \<longrightarrow> is_aligned buf' msg_align_bits\<rbrace>"
and handle_arch_fault_reply_globals_equiv:
"\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
handle_arch_fault_reply vmf thread x y
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
and handle_arch_fault_reply_valid_arch_state[wp]:
"handle_arch_fault_reply vmf thread x y \<lbrace>\<lambda>s :: det_state. valid_arch_state s\<rbrace>"
(* FIXME IF: This assumption precludes X64 (its valid_arch_state includes caps) *)
and transfer_caps_loop_valid_arch[wp]:
"transfer_caps_loop epptr_opt buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
begin
lemma store_word_offs_equiv_but_for_labels:
"\<lbrace>equiv_but_for_labels aag L st and
K (for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + of_nat offs * of_nat word_size))\<rbrace>
store_word_offs ptr offs v
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
unfolding store_word_offs_def
apply (wp modify_wp | simp add: do_machine_op_def split_def)+
apply clarsimp
apply (erule use_valid[OF _ storeWord_equiv_but_for_labels])
apply simp
done
(* FIXME: many redundant conditions *)
lemma update_waiting_ntfn_reads_respects:
assumes domains_distinct[wp]: "pas_domains_distinct aag"
shows
"reads_respects aag l (valid_objs and sym_refs \<circ> state_refs_of and pas_refined aag
and pas_cur_domain aag and ko_at (Notification ntfn) nptr
and (\<lambda>s. is_subject aag (cur_thread s))
and K (ntfn_obj ntfn = WaitingNtfn queue))
(update_waiting_ntfn nptr queue bound_tcb badge)"
unfolding update_waiting_ntfn_def fun_app_def
apply (wp assert_sp possible_switch_to_reads_respects gets_cur_thread_ev | simp add: split_def)+
by (wp as_user_set_register_reads_respects' set_thread_state_reads_respects
set_simple_ko_reads_respects set_thread_state_pas_refined
set_simple_ko_valid_objs hoare_vcg_disj_lift set_simple_ko_pas_refined
| simp add: split_def)+
lemma update_waiting_ntfn_equiv_but_for_labels:
"\<lbrace>equiv_but_for_labels aag L st and pas_refined aag and
valid_objs and ko_at (Notification ntfn) nptr and sym_refs \<circ> state_refs_of and
(\<lambda>s. \<forall>t\<in> set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and
K (ntfn_obj ntfn = WaitingNtfn list \<and> pasObjectAbs aag nptr \<in> L \<and>
all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L \<and>
\<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L)\<rbrace>
update_waiting_ntfn nptr list boundtcb badge
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
unfolding update_waiting_ntfn_def
apply (wp hoare_weak_lift_imp as_user_equiv_but_for_labels set_thread_state_runnable_equiv_but_for_labels
set_thread_state_pas_refined set_notification_equiv_but_for_labels
set_simple_ko_pred_tcb_at set_simple_ko_pas_refined
hoare_vcg_disj_lift possible_switch_to_equiv_but_for_labels
| wpc | simp add: split_def)+
apply clarsimp
apply (frule_tac P="receive_blocked_on nptr" and t="hd list" in ntfn_queued_st_tcb_at')
apply (fastforce)
apply assumption
apply assumption
apply simp
apply (subgoal_tac "pasObjectAbs aag (hd list) \<in> all_with_auth_to aag Receive (pasObjectAbs aag nptr)")
apply (fastforce)
apply (clarsimp simp: all_with_auth_to_def)
apply (erule pas_refined_mem[rotated])
apply (rule sta_ts)
apply (clarsimp simp: thread_st_auth_def tcb_states_of_state_def st_tcb_def2)
apply (case_tac "tcb_state tcb", simp_all)
done
end
lemma invisible_ntfn_invisible_receivers_and_ipcbuffers:
"\<lbrakk> labels_are_invisible aag l {pasObjectAbs aag nptr};
(pasSubject aag, Notify, pasObjectAbs aag nptr) \<in> pasPolicy aag\<rbrakk>
\<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag nptr} \<union>
all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<union>
\<Union>(all_to_which_has_auth aag Write
` all_with_auth_to aag Receive (pasObjectAbs aag nptr)))"
by (auto simp: labels_are_invisible_def aag_can_affect_label_def
all_to_which_has_auth_def all_with_auth_to_def
dest: reads_read_page_read_thread reads_read_queued_thread_read_ep)
lemma invisible_ntfn_invisible_receivers_and_receivers[rotated 1]:
"\<lbrakk> auth \<in> {Notify,Receive,SyncSend}; labels_are_invisible aag l {pasObjectAbs aag nptr};
(pasSubject aag, auth, pasObjectAbs aag nptr) \<in> pasPolicy aag \<rbrakk>
\<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag nptr} \<union>
all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<union>
(\<Union>(all_to_which_has_auth aag Receive
` all_with_auth_to aag Receive (pasObjectAbs aag nptr))) \<union>
(\<Union>(all_to_which_has_auth aag Write
` all_with_auth_to aag Receive (pasObjectAbs aag nptr))))"
by (auto simp: labels_are_invisible_def aag_can_affect_label_def
all_to_which_has_auth_def all_with_auth_to_def
dest: read_sync_ep_read_senders read_sync_ep_read_receivers
reads_read_queued_thread_read_ep reads_read_page_read_thread reads_ep)
lemma read_queued_thread_reads_ntfn:
"\<lbrakk> ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s;
sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue;
(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<rbrakk>
\<Longrightarrow> aag_can_read aag ntfnptr"
apply (frule_tac P="receive_blocked_on ntfnptr" and t=t in ntfn_queued_st_tcb_at')
apply (fastforce)
apply assumption
apply assumption
apply simp
apply (rule_tac t="pasObjectAbs aag t" and auth="Receive" and auth'="Notify"
in reads_read_queued_thread_read_ep)
apply assumption
apply simp
apply (erule pas_refined_mem[rotated])
apply (rule sta_ts)
apply (clarsimp simp: thread_st_auth_def tcb_states_of_state_def st_tcb_def2)
apply (case_tac "tcb_state tcb", simp_all)[1]
apply simp
apply simp
done
lemma not_etcb_at_not_cdom_can_read:
assumes domains_distinct[wp]: "pas_domains_distinct aag"
shows "\<lbrakk> \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s;
tcb_at t s; valid_etcbs s; pas_refined aag s; pas_cur_domain aag s \<rbrakk>
\<Longrightarrow> aag_can_read aag t"
apply (clarsimp simp: valid_etcbs_def tcb_at_st_tcb_at etcb_at_def is_etcb_at_def
pas_refined_def tcb_domain_map_wellformed_aux_def)
apply (erule_tac x="(t, cur_domain s)" in ballE)
apply (force dest: domains_distinct[THEN pas_domains_distinct_inj])
apply (force intro: domtcbs)
done
lemma tcb_at_ntfn_queue:
"\<lbrakk> valid_objs s; t \<in> set q; ko_at (Notification ntfn) nptr s; ntfn_obj ntfn = WaitingNtfn q \<rbrakk>
\<Longrightarrow> tcb_at t s"
by (fastforce simp: obj_at_def valid_obj_def valid_ntfn_def)
lemma invisible_ep_invisible_receiver:
"\<lbrakk> labels_are_invisible aag l {pasObjectAbs aag epptr};
(pasObjectAbs aag tcb, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag;
(pasObjectAbs aag tcb, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<rbrakk>
\<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag epptr} \<union> {pasObjectAbs aag tcb})"
by (auto simp: labels_are_invisible_def aag_can_affect_label_def all_with_auth_to_def
dest: reads_ep reads_read_queued_thread_read_ep)
lemma no_fail_gts:
"no_fail (tcb_at tcb) (get_thread_state tcb)"
apply (clarsimp simp: get_thread_state_def thread_get_def)
apply (rule no_fail_pre)
apply wp
by (clarsimp simp: get_tcb_def tcb_at_def)
lemma sts_noop:
"monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s))
(set_thread_state_ext tcb) (return ())"
unfolding set_thread_state_ext_def when_def
apply (monadic_rewrite_l monadic_rewrite_if_l_False \<open>wpsimp wp: gts_wp\<close>)
apply (monadic_rewrite_symb_exec_l_drop)+
apply (rule monadic_rewrite_refl)
by (auto simp: pred_tcb_at_def obj_at_def is_tcb_def get_tcb_def)
lemma sts_to_modify':
"monadic_rewrite True True (tcb_at tcb and (\<lambda>s :: det_state. tcb \<noteq> cur_thread s))
(set_thread_state tcb st)
(modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))"
apply (clarsimp simp: set_thread_state_def set_object_def)
apply (monadic_rewrite_l sts_noop \<open>wpsimp wp: get_object_wp\<close>)
apply (simp add: bind_assoc)
apply monadic_rewrite_symb_exec_l+
apply (rule_tac P="\<lambda>s'. s' = s \<and> tcba = the (get_tcb tcb s)" in monadic_rewrite_pre_imp_eq)
apply (clarsimp simp: put_def modify_def get_def bind_def)
apply (wpsimp wp: get_object_wp)+
by (clarsimp simp: get_tcb_def tcb_at_def)
lemma sts_no_fail:
"no_fail (\<lambda>s :: det_state. tcb_at tcb s) (set_thread_state tcb st)"
apply (simp add: set_thread_state_def set_object_def)
apply (simp add: set_thread_state_ext_def get_thread_state_def
thread_get_def set_scheduler_action_def)
apply (rule no_fail_pre)
apply (wpsimp wp: get_object_wp)+
apply (clarsimp simp: get_tcb_def tcb_at_def obj_at_def a_type_def is_tcb_def
split: kernel_object.splits option.splits)
by (metis kernel_object.exhaust option.inject)
lemmas sts_to_modify =
monadic_rewrite_weaken_failure[OF sts_to_modify' sts_no_fail no_fail_modify,simplified]
definition "blocked_cancel_ipc_nosts tcb \<equiv>
do state <- get_thread_state tcb;
epptr \<leftarrow> get_blocking_object state;
ep \<leftarrow> get_endpoint epptr;
queue \<leftarrow> get_ep_queue ep;
queue' \<leftarrow> return $ remove1 tcb queue;
ep' \<leftarrow> return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue');
set_endpoint epptr ep';
set_thread_state tcb Running
od"
lemma cancel_ipc_to_blocked_nosts:
"monadic_rewrite False False (\<lambda>s :: det_state. st_tcb_at receive_blocked tcb s \<and> cur_thread s \<noteq> tcb)
(blocked_cancel_ipc_nosts tcb)
(cancel_ipc tcb >>= (\<lambda>_. set_thread_state tcb Running))"
apply (simp add: cancel_ipc_def bind_assoc blocked_cancel_ipc_nosts_def)
apply (rule monadic_rewrite_bind_tail)
apply (rule monadic_rewrite_transverse)
apply (rename_tac state)
apply (rule_tac P="\<lambda>_. \<exists>xa pl. state = BlockedOnReceive xa pl" in monadic_rewrite_bind_head)
apply (rule monadic_rewrite_gen_asm[where Q=\<top>,simplified])
apply clarsimp
apply (rule monadic_rewrite_refl)
apply (simp add: blocked_cancel_ipc_def blocked_cancel_ipc_nosts_def bind_assoc)
apply (rule monadic_rewrite_bind_tail)
apply (rule monadic_rewrite_bind_tail)
apply (rule monadic_rewrite_bind_tail)
apply (rule monadic_rewrite_bind_tail)
apply (rule monadic_rewrite_trans)
apply (rule sts_to_modify)
apply (rule monadic_rewrite_transverse)
apply (rule monadic_rewrite_bind)
apply (rule sts_to_modify)
apply (rule sts_to_modify)
apply (rule hoare_modifyE_var[where P="tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)"])
apply (clarsimp simp: tcb_at_def get_tcb_def)
apply (simp add: modify_modify)
apply (rule monadic_rewrite_is_refl)
apply (fastforce simp add: simpler_modify_def o_def get_tcb_def)
apply (wp gts_wp)+
apply (simp add: set_thread_state_def bind_assoc gets_the_def)
apply (clarsimp simp: pred_tcb_at_def receive_blocked_def obj_at_def is_tcb_def)
by (case_tac "tcb_state tcba"; fastforce)
lemma gts_reads_respects:
"reads_respects aag l (K (aag_can_read aag t \<or> aag_can_affect aag l t)) (get_thread_state t)"
unfolding get_thread_state_def
by (wp thread_get_reads_respects)
lemma ev2_invisible_simple:
assumes domains_distinct: "pas_domains_distinct aag"
shows "\<lbrakk> labels_are_invisible aag l L; modifies_at_most aag L Q f \<rbrakk>
\<Longrightarrow> reads_respects aag l Q (f :: (det_state, unit) nondet_monad)"
apply (simp add: equiv_valid_def2)
apply (rule equiv_valid_2_guard_imp)
apply (rule ev2_invisible[OF domains_distinct])
by fastforce+
crunch blocked_cancel_ipc_nosts
for silc_inv[wp]: "silc_inv aag st"
context Ipc_IF_1 begin
lemma blocked_cancel_ipc_nosts_equiv_but_for_labels:
"\<lbrace>pas_refined aag and st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t
and bound_tcb_at ((=) (Some ntfnptr)) t
and equiv_but_for_labels aag L st
and K (pasObjectAbs aag x \<in> L)
and K (pasObjectAbs aag t \<in> L)\<rbrace>
blocked_cancel_ipc_nosts t
\<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
unfolding blocked_cancel_ipc_nosts_def get_blocking_object_def
apply (wp set_endpoint_equiv_but_for_labels get_object_wp gts_wp
set_thread_state_runnable_equiv_but_for_labels
| wpc | simp)+
by (clarsimp simp: pred_tcb_at_def obj_at_def)
lemma blocked_cancel_ipc_nosts_reads_respects:
assumes domains_distinct[wp]: "pas_domains_distinct aag"
shows
"reads_respects aag l
(pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = (BlockedOnReceive x pl)) t
and bound_tcb_at ((=) (Some ntfnptr)) t
and (\<lambda>s. is_subject aag (cur_thread s))
and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
\<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
\<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag))
(blocked_cancel_ipc_nosts t)"
unfolding blocked_cancel_ipc_nosts_def
apply (simp only:bind_assoc[symmetric])
apply (rule bind_ev[where P''=\<top>,simplified])
apply (wp set_thread_state_runnable_reads_respects,simp)
subgoal proof (cases "aag_can_read_label aag (pasObjectAbs aag x) \<or> aag_can_affect aag l x")
case True thus ?thesis \<comment> \<open>boring case, can read or affect ep\<close>
unfolding blocked_cancel_ipc_nosts_def get_blocking_object_def
apply clarsimp
apply (rule pre_ev)
apply (wpsimp wp: set_thread_state_reads_respects get_ep_queue_reads_respects
get_simple_ko_reads_respects get_blocking_object_reads_respects
gts_reads_respects set_simple_ko_reads_respects gts_wp
simp: get_blocking_object_def get_thread_state_rev)+
apply (clarsimp simp: pred_tcb_at_def obj_at_def)
by (fastforce dest:read_sync_ep_read_receivers )
next
case False thus ?thesis apply - \<comment> \<open>can't read or affect ep\<close>
apply (rule gen_asm_ev)
apply (drule label_is_invisible[THEN iffD2])
apply clarsimp
apply (rule ev2_invisible_simple[OF domains_distinct],assumption)
apply (simp add: get_blocking_object_def)
apply (rule modifies_at_mostI)
apply (rule hoare_pre)
apply (wpsimp wp: set_thread_state_runnable_equiv_but_for_labels
set_endpoint_equiv_but_for_labels get_object_wp gts_wp
set_thread_state_runnable_equiv_but_for_labels)+
by (fastforce simp: pred_tcb_at_def obj_at_def)
qed
by wp
lemmas blocked_cancel_ipc_nosts_reads_respects_f =
reads_respects_f[where Q=\<top>, simplified,
OF blocked_cancel_ipc_nosts_reads_respects
blocked_cancel_ipc_nosts_silc_inv,
simplified]
end
lemma monadic_rewrite_reads_respects:
"\<lbrakk> monadic_rewrite False False P f f'; reads_respects aag l P' (do x <- f; g x od) \<rbrakk>
\<Longrightarrow> reads_respects aag l (P and P') (do x <- f'; g x od)"
apply (clarsimp simp: monadic_rewrite_def spec_equiv_valid_def
equiv_valid_def equiv_valid_2_def bind_def)
apply (frule_tac x=st in spec)
apply (drule_tac x=t in spec)
by fastforce
lemmas cancel_ipc_reads_respects_rewrite =
monadic_rewrite_reads_respects[OF cancel_ipc_to_blocked_nosts, simplified bind_assoc]
lemmas cancel_ipc_valid_rewrite =
monadic_rewrite_is_valid[OF cancel_ipc_to_blocked_nosts, simplified bind_assoc]
crunch blocked_cancel_ipc_nosts
for etcb_at[wp]: "etcb_at P t"
crunch blocked_cancel_ipc_nosts
for cur_domain[wp]: "\<lambda>s. P (cur_domain s)"
crunch blocked_cancel_ipc_nosts
for pas_refined[wp]: "pas_refined aag"
crunch blocked_cancel_ipc_nosts
for cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
lemma BlockedOnReceive_inj:
"x = (case (BlockedOnReceive x pl) of BlockedOnReceive x pl \<Rightarrow> x)"
"pl = (case (BlockedOnReceive x pl) of BlockedOnReceive x pl \<Rightarrow> pl)"
by auto
lemma receive_blockedD:
"receive_blocked st \<Longrightarrow> \<exists>epptr pl. st = BlockedOnReceive epptr pl"
by (cases st; simp add: receive_blocked_def)
context Ipc_IF_1 begin
lemma send_signal_reads_respects:
assumes domains_distinct[wp]: "pas_domains_distinct aag"
notes set_thread_state_owned_reads_respects[wp del]
cancel_ipc_pas_refined[wp del]
shows
"reads_respects aag l
(pas_refined aag and pas_cur_domain aag
and (\<lambda>s. is_subject aag (cur_thread s))
and valid_etcbs and ct_active
and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs
and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))
(send_signal ntfnptr badge)"
unfolding send_signal_def fun_app_def
subgoal proof (cases "aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr")
case True
note visible = this
show ?thesis
apply (rule pre_ev)
apply (simp split del: if_split
| rule_tac ntfnptr=ntfnptr in blocked_cancel_ipc_nosts_reads_respects
| rule cancel_ipc_reads_respects_rewrite
| wp (once) set_simple_ko_reads_respects possible_switch_to_reads_respects
as_user_set_register_reads_respects' set_thread_state_pas_refined
set_simple_ko_reads_respects cancel_ipc_receive_blocked_pas_refined
gts_reads_respects gts_wp hoare_vcg_imp_lift get_simple_ko_wp
get_simple_ko_reads_respects update_waiting_ntfn_reads_respects
| wpc
| simp )+
apply (insert visible)
apply clarsimp
apply (rule conjI[rotated])
apply fastforce
apply (rule disjI2)
apply (intro impI allI)
apply (simp add: obj_at_def)
apply (rule conjI)
apply (frule (3) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl])
apply (frule (1) bound_tcb_at_implies_receive)
apply (elim disjE)
apply (rule disjI1)
apply (fastforce dest:read_sync_ep_read_receivers)
apply (rule disjI2)
apply (fastforce dest:read_sync_ep_read_receivers)
apply (clarsimp)
apply (frule (1) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl])
apply (fastforce simp: obj_at_def)
apply assumption
apply (rule conjI)
apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def)
apply (rule conjI[rotated])
apply (frule (1) bound_tcb_at_implies_receive)
apply (frule (1) bound_tcb_at_implies_reset)
apply (clarsimp simp: pred_tcb_at_def get_tcb_def obj_at_def)
apply (rule context_conjI)
apply (fastforce dest!: receive_blockedD intro: BlockedOnReceive_inj)
apply (frule_tac t=x and tcb=tcb and ep = "case (tcb_state tcb) of BlockedOnReceive a pl \<Rightarrow> a"
in get_tcb_recv_blocked_implies_receive)
apply (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def)
apply (fastforce simp: receive_blocked_def split:thread_state.splits)
apply (fastforce simp: receive_blocked_def intro!: BlockedOnReceive_inj)
by (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def receive_blocked_def ct_in_state_def)
next
case False note invisible = this show ?thesis
apply (insert label_is_invisible[THEN iffD2, OF invisible])
apply (rule gen_asm_ev)
apply (drule (1) invisible_ntfn_invisible_receivers_and_receivers)
apply simp
apply (rule ev2_invisible_simple[OF domains_distinct],assumption)
apply (rule modifies_at_mostI)
apply (simp split del: if_split
| rule cancel_ipc_valid_rewrite
| wp (once) set_thread_state_pas_refined set_notification_equiv_but_for_labels
possible_switch_to_equiv_but_for_labels as_user_equiv_but_for_labels
set_thread_state_runnable_equiv_but_for_labels get_simple_ko_wp
gts_wp update_waiting_ntfn_equiv_but_for_labels
blocked_cancel_ipc_nosts_equiv_but_for_labels
\<comment> \<open>FIXME: The following line is working around the fact that wp (once) doesn't invoke
wp_pre. If that is changed then it could be removed.\<close>
| wp_pre0
| wpc
| wps)+
apply (elim conjE)
apply (match premises in "ntfn_bound_tcb _ = _" \<Rightarrow> \<open>fail\<close>
\<bar> _ \<Rightarrow> \<open>rule allI impI conjI\<close>)+
prefer 2
apply (intro conjI allI impI; fastforce?)
subgoal waiting_ntfn
apply clarsimp
apply (rule ccontr)
apply (frule (3) not_etcb_at_not_cdom_can_read[OF domains_distinct, rotated 2])
apply (rule tcb_at_ntfn_queue;assumption)
apply (frule (7) read_queued_thread_reads_ntfn)
using invisible
by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def)
apply (frule (1) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)", OF _ _ _ _ refl])
apply (fastforce simp: obj_at_def)
apply assumption
apply (intro allI conjI impI)
apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def
split: thread_state.splits
intro!: BlockedOnReceive_inj)
apply assumption
apply distinct_subgoals
apply (fold_subgoals (prefix))
apply (frule st_tcb_at_tcb_at)
subgoal bound_ntfn premises prems for st s ntfn x sta
prefer 2
apply (rule disjI2)
apply (rule disjI1)
subgoal bound_tcb_can_receive
using prems
apply (clarsimp simp: all_with_auth_to_def obj_at_def)
by (rule bound_tcb_at_implies_receive;assumption)
apply (rule disjI2)
apply (rule disjI2)
apply (rule disjI1)
subgoal bound_ep_can_receive
apply (rule bexI[OF _ bound_tcb_can_receive])
apply (simp add: all_with_auth_to_def all_to_which_has_auth_def)
using prems
apply (case_tac sta; (clarsimp simp: pred_tcb_at_def obj_at_def receive_blocked_def))
apply (rule get_tcb_recv_blocked_implies_receive, assumption)
apply (fastforce simp: get_tcb_def)
by (fastforce split: thread_state.splits)
apply (rule ccontr)
apply (insert prems)
apply (frule (4) not_etcb_at_not_cdom_can_read[OF domains_distinct])
using bound_tcb_can_receive
apply (fastforce simp: labels_are_invisible_def all_with_auth_to_def all_to_which_has_auth_def)
apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def)
apply (rule ccontr)
apply clarsimp
using invisible bound_tcb_can_receive reads_ep
by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def)
done
qed
done
end
lemma receive_signal_reads_respects:
assumes domains_distinct[wp]: "pas_domains_distinct aag"
shows
"reads_respects aag (l :: 'a subject_label)
(valid_objs and pas_refined aag and (\<lambda>s. is_subject aag (cur_thread s))
and K ((\<forall>ntfnptr \<in> obj_refs_ac cap.
(pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and>
is_subject aag thread)))
(receive_signal thread cap is_blocking)"
unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def
by (wp set_simple_ko_reads_respects set_thread_state_reads_respects
as_user_set_register_reads_respects' get_simple_ko_reads_respects hoare_vcg_all_lift
| wpc
| wp (once) hoare_drop_imps
| force dest: reads_ep)+
subsection "Sync IPC"
definition aag_can_read_or_affect_ipc_buffer :: "'a PAS \<Rightarrow> 'a \<Rightarrow> obj_ref option \<Rightarrow> bool" where
"aag_can_read_or_affect_ipc_buffer aag l \<equiv>
case_option True
(\<lambda>buf'. is_aligned buf' msg_align_bits \<and>
(\<forall>x \<in> ptr_range buf' msg_align_bits. aag_can_read aag x \<or> aag_can_affect aag l x))"
lemma for_each_byte_of_word_def2:
"for_each_byte_of_word P ptr \<equiv> (\<forall>x\<in>ptr_range ptr word_size_bits. P x)"
by (simp add: for_each_byte_of_word_def ptr_range_def word_size_size_bits_word add_diff_eq)
context Ipc_IF_1 begin
lemma lookup_ipc_buffer_aag_can_read_or_affect:
"\<lbrace>pas_refined aag and valid_objs and K (aag_can_read aag thread \<or> aag_can_affect aag l thread)\<rbrace>
lookup_ipc_buffer is_receiver thread
\<lbrace>\<lambda>rv s. aag_can_read_or_affect_ipc_buffer aag l rv\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_strengthen_post[OF lookup_ipc_buffer_has_read_auth])
apply (auto simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def
intro: reads_read_thread_read_pages
simp: aag_can_affect_label_def split: option.splits)
done
lemma aag_has_auth_to_read_cptrs:
"\<lbrakk> x \<in> set [buffer_cptr_index ..< buffer_cptr_index + unat (mi_extra_caps mi)];
ipc_buffer_has_read_auth aag (pasSubject aag) (Some a);
buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
\<Longrightarrow> for_each_byte_of_word (\<lambda> y. aag_can_read aag y) (a + of_nat x * of_nat word_size)"
apply (simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def)
apply (rule ballI)
apply (rule reads_read)
apply (clarify)
apply (erule bspec)
apply (rule subsetD[OF cptrs_in_ipc_buffer])
apply fastforce
apply assumption
apply assumption
apply assumption
done
lemma get_extra_cptrs_rev:
"reads_equiv_valid_inv A aag
(K (ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and>
(buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits))))
(get_extra_cptrs buffer mi)"
unfolding get_extra_cptrs_def
apply (rule gen_asm_ev)
apply clarsimp
apply (case_tac buffer, simp_all add: return_ev_pre)
apply (wp mapM_ev equiv_valid_guard_imp[OF load_word_offs_rev]
| erule (2) aag_has_auth_to_read_cptrs)+
done
lemma lookup_extra_caps_rev:
"reads_equiv_valid_inv A aag
(pas_refined aag and (K (is_subject aag thread)) and
(\<lambda>s. ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and>
buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)))
(lookup_extra_caps thread buffer mi)"
unfolding lookup_extra_caps_def fun_app_def
by (wpsimp wp: mapME_ev cap_fault_on_failure_rev lookup_cap_and_slot_rev get_extra_cptrs_rev)
lemmas lookup_extra_caps_reads_respects_g =
reads_respects_g_from_inv[OF lookup_extra_caps_rev lookup_extra_caps_inv]
lemma aag_has_auth_to_read_msg:
"\<lbrakk> n = msg_max_length \<or> n < msg_max_length;
ipc_buffer_has_read_auth aag (pasSubject aag) (Some p);
unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits) \<rbrakk>
\<Longrightarrow> for_each_byte_of_word (aag_can_read aag) (p + of_nat n * of_nat word_size)"
apply (simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def)
apply (rule ballI)
apply (rule reads_read)
apply (clarify)
apply (erule bspec)
apply (rule subsetD[OF msg_in_ipc_buffer[where n=n]])
apply assumption
apply assumption
apply assumption
apply assumption
done
(* only called within do_reply_transfer for which access assumes sender
and receiver in same domain *)
lemma get_mrs_rev:
"reads_equiv_valid_inv A aag
(K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf
\<and> unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)))
(get_mrs thread buf mi)"
unfolding get_mrs_def
apply (rule gen_asm_ev)
apply (wp mapM_ev'' load_word_offs_rev thread_get_rev
| wpc
| rule aag_has_auth_to_read_msg[where mi=mi]
| clarsimp split: if_split_asm)+
done
lemmas get_mrs_reads_respects_g = reads_respects_g_from_inv[OF get_mrs_rev get_mrs_inv]
end
lemma setup_caller_cap_reads_respects:
"reads_respects aag l (K (aag_can_read aag sender \<and> aag_can_read aag receiver))
(setup_caller_cap sender receiver grant)"
unfolding setup_caller_cap_def
by (wp cap_insert_reads_respects set_thread_state_owned_reads_respects | simp)+
lemma const_on_failure_ev:
"equiv_valid_inv I A P m
\<Longrightarrow> equiv_valid_inv I A P (const_on_failure c m)"
unfolding const_on_failure_def catch_def
by (wp | wpc | simp)+
lemma set_extra_badge_reads_respects:
"reads_respects aag l \<top> (set_extra_badge buffer badge n)"
unfolding set_extra_badge_def
by (rule store_word_offs_reads_respects)
lemma reads_equiv_cdt_has_children0:
"\<lbrakk> pas_refined aag s; pas_refined aag s'; aag_can_read aag (fst slot);
equiv_for (aag_can_read aag \<circ> fst) cdt s s' \<rbrakk>
\<Longrightarrow> (cdt s) c = Some slot \<longleftrightarrow> (cdt s') c = Some slot"
apply (rule iffI)
apply (drule equiv_forD)
apply (erule(1) all_children_subjectReads[THEN all_childrenD];fastforce)
apply fastforce
apply (drule equiv_forD)
apply (erule(1) all_children_subjectReads[THEN all_childrenD];fastforce)
apply fastforce
done
lemma reads_equiv_cdt_has_children:
"\<lbrakk> pas_refined aag s; pas_refined aag s'; is_subject aag (fst slot);
equiv_for (aag_can_read aag \<circ> fst) cdt s s' \<rbrakk>
\<Longrightarrow> (\<exists>c. (cdt s) c = Some slot) = (\<exists>c. (cdt s') c = Some slot)"
apply (rule iff_exI)
by (erule reads_equiv_cdt_has_children0; force)
lemma ensure_no_children_rev:
"reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag (fst slot)))
(ensure_no_children slot)"
unfolding ensure_no_children_def fun_app_def equiv_valid_def2
apply (rule equiv_valid_rv_guard_imp)
apply (rule_tac Q="\<lambda> rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s"
in equiv_valid_rv_liftE_bindE[OF equiv_valid_rv_guard_imp[OF gets_cdt_revrv']])
apply (rule TrueI)
apply (clarsimp simp: equiv_valid_2_def)
apply (drule reads_equiv_cdt_has_children)
apply assumption
apply assumption
apply (fastforce elim: reads_equivE)
apply (fastforce simp: in_whenE in_throwError)
apply (wp, simp)
done
(* FIXME MOVE *)
lemma ball_subsetE:
"\<lbrakk> \<forall>x \<in> S. P x; S' \<subseteq> S; \<And>x. P x \<Longrightarrow> Q x \<rbrakk>
\<Longrightarrow> \<forall>x \<in> S'. Q x"
by blast
context Ipc_IF_1 begin
lemma derive_cap_rev':
"reads_equiv_valid_inv A aag (\<lambda>s. (\<exists>x xa xb d. cap = cap.UntypedCap d x xa xb)
\<longrightarrow> pas_refined aag s \<and> is_subject aag (fst slot))
(derive_cap slot cap)"
unfolding derive_cap_def
apply (rule equiv_valid_guard_imp)
apply (wp ensure_no_children_rev arch_derive_cap_rev | wpc | simp)+
done
lemma derive_cap_rev:
"reads_equiv_valid_inv A aag (\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot))
(derive_cap slot cap)"
by (blast intro: equiv_valid_guard_imp[OF derive_cap_rev'])
lemma transfer_caps_loop_reads_respects':
"reads_respects aag l
(pas_refined aag and valid_mdb and valid_objs and
(\<lambda>s. (\<forall>cap\<in>set caps. valid_cap (fst cap) s
\<and> is_subject aag (fst (snd cap))
\<and> pas_cap_cur_auth aag (fst cap)
\<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap
\<longrightarrow> cp \<noteq> fst cap
\<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s)
\<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)
\<and> cte_wp_at ((=) NullCap) slot s
\<and> real_cte_at slot s)
\<and> distinct slots))
(transfer_caps_loop ep rcv_buffer n caps slots mi)"
apply (induct caps arbitrary: slots n mi)
apply simp
apply (rule return_ev_pre)
apply (case_tac a, rename_tac cap obj ind)
apply (simp split del: if_split)
apply (rule equiv_valid_guard_imp)
apply (wp const_on_failure_ev | simp | intro conjI impI)+
apply fast
apply (wp set_extra_badge_reads_respects hoare_vcg_ball_lift | simp)+
apply fast
apply (wp cap_insert_reads_respects cap_insert_pas_refined whenE_throwError_wp
derive_cap_rev derive_cap_cap_cur_auth derive_cap_is_derived
hoare_vcg_ball_lift cap_insert_cte_wp_at
| simp split del: if_split)+
apply (rule_tac Q'="\<lambda>capd s. (capd \<noteq> NullCap
\<longrightarrow> cte_wp_at (is_derived (cdt s) (obj,ind) capd) (obj, ind) s)
\<and> (capd \<noteq> NullCap \<longrightarrow> QM s capd)" for QM
in hoare_strengthen_postE_R)
prefer 2
apply (clarsimp simp: cte_wp_at_caps_of_state split del: if_split)
apply (strengthen is_derived_is_transferable[mk_strg I' O], assumption, solves\<open>simp\<close>)
apply (rule hoare_vcg_conj_liftE_R')
apply (rule derive_cap_is_derived)
apply (wp derive_cap_is_derived_foo')
apply wp
apply (clarsimp simp: remove_rights_cur_auth cte_wp_at_caps_of_state split del: if_split)
apply (rename_tac actual_cap)
apply (strengthen real_cte_tcb_valid)
apply (clarsimp)
apply (intro conjI)
subgoal
by (fastforce simp: masked_as_full_def is_cap_simps cap_master_cap_simps split: if_splits)
apply clarsimp
apply (intro conjI)
apply (fastforce dest: auth_derived_pas_cur_auth)
apply fastforce
subgoal
apply (erule ball_subsetE, fastforce)
by (fastforce simp: cte_wp_at_caps_of_state masked_as_full_def is_cap_simps split: if_splits)
subgoal by (fastforce simp: neq_Nil_conv cte_wp_at_caps_of_state)
by (rule distinct_tl)
lemma transfer_caps_loop_reads_respects:
"reads_respects aag l
(pas_refined aag and valid_mdb and valid_objs and
(\<lambda>s. (\<forall>cap\<in>set caps. valid_cap (fst cap) s
\<and> is_subject aag (fst (snd cap))
\<and> pas_cap_cur_auth aag (fst cap)
\<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp = fst cap) (snd cap) s)
\<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)
\<and> cte_wp_at ((=) NullCap) slot s
\<and> real_cte_at slot s)
\<and> distinct slots))
(transfer_caps_loop ep rcv_buffer n caps slots mi)"
apply (rule equiv_valid_guard_imp, rule transfer_caps_loop_reads_respects')
by (fastforce elim: cte_wp_at_weakenE)
end
lemma empty_on_failure_ev:
"equiv_valid_inv I A P m \<Longrightarrow>
equiv_valid_inv I A P (empty_on_failure m)"
unfolding empty_on_failure_def catch_def
by (wp | wpc | simp)+
lemma unify_failure_ev:
"equiv_valid_inv I A P m \<Longrightarrow>
equiv_valid_inv I A P (unify_failure m)"
unfolding unify_failure_def handleE'_def
by (wp | wpc | simp)+
lemma lookup_slot_for_cnode_op_rev:
"reads_equiv_valid_inv A aag
(\<lambda>s. (depth \<noteq> 0 \<and> depth \<le> word_bits)
\<longrightarrow> (pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))))
(lookup_slot_for_cnode_op is_source croot ptr depth)"
unfolding lookup_slot_for_cnode_op_def
apply (clarsimp split del: if_split)
apply (wp resolve_address_bits_rev lookup_error_on_failure_rev
whenE_throwError_wp
| wpc
| rule hoare_strengthen_postE_R[OF wp_post_tautE_R]
| simp add: split_def split del: if_split)+
done
lemma lookup_slot_for_cnode_op_reads_respects:
"reads_respects aag l (pas_refined aag and K (is_subject aag (obj_ref_of croot)))
(lookup_slot_for_cnode_op is_source croot ptr depth)"
apply (rule equiv_valid_guard_imp[OF lookup_slot_for_cnode_op_rev])
by simp
lemma lookup_cap_rev:
"reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread))
(lookup_cap thread ref)"
unfolding lookup_cap_def split_def fun_app_def
apply (wp lookup_slot_for_thread_rev get_cap_rev | simp | strengthen aag_can_read_self)+
apply (rule lookup_slot_for_thread_authorised)
apply simp
done
lemma word_plus_power_2_offset_le:
"\<lbrakk> is_aligned (p :: 'l :: len word) n; is_aligned q m; p < q; n \<le> m; n < len_of TYPE('l) \<rbrakk>
\<Longrightarrow> p + 2^n \<le> q"
apply (drule is_aligned_weaken, assumption)
apply (clarsimp simp: is_aligned_def)
apply (elim dvdE)
apply (rename_tac k ka)
apply (rule_tac ua=0 and n="int k" and n'="int ka" in udvd_incr')
apply assumption
apply (clarsimp simp: uint_nat)+
done
context Ipc_IF_1 begin