-
Notifications
You must be signed in to change notification settings - Fork 105
/
TcbAcc_AI.thy
1839 lines (1537 loc) · 72.3 KB
/
TcbAcc_AI.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory TcbAcc_AI
imports ArchCSpace_AI
begin
arch_requalify_facts
valid_arch_arch_tcb_context_set
as_user_inv
getRegister_inv
user_getreg_inv
set_cap_valid_arch_caps_simple
set_cap_kernel_window_simple
declare user_getreg_inv[wp]
locale TcbAcc_AI_storeWord_invs =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes storeWord_invs[wp]:
"\<And> p w.
\<lbrace>in_user_frame p and invs :: 'state_ext state \<Rightarrow> bool\<rbrace>
do_machine_op (storeWord p w)
\<lbrace>\<lambda>rv. invs\<rbrace>"
lemmas gts_inv[wp] = get_thread_state_inv
lemmas gbn_inv[wp] = get_bound_notification_inv
lemma gts_sp:
"\<lbrace>P\<rbrace> get_thread_state t \<lbrace>\<lambda>st. st_tcb_at (\<lambda>x. st = x) t and P\<rbrace>"
apply (simp add: pred_conj_def)
apply (rule hoare_weaken_pre)
apply (rule hoare_vcg_conj_lift)
apply (rule gts_st_tcb)
apply (rule gts_inv)
apply simp
done
lemma gbn_sp:
"\<lbrace>P\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfn. bound_tcb_at (\<lambda>x. ntfn = x) t and P\<rbrace>"
apply (simp add: pred_conj_def)
apply (rule hoare_weaken_pre)
apply (rule hoare_vcg_conj_lift)
apply (rule gbn_bound_tcb)
apply (rule gbn_inv)
apply simp
done
lemma red_univ_get_wp[simp]:
"(\<forall>(rv, s') \<in> fst (f s). s = s' \<longrightarrow> (rv, s') \<in> fst (f s'))"
by clarsimp
lemma thread_get_inv [wp]: "\<lbrace>P\<rbrace> thread_get f t \<lbrace>\<lambda>rv. P\<rbrace>"
by (simp add: thread_get_def | wp)+
locale TcbAcc_AI_arch_tcb_context_set_eq =
assumes arch_tcb_context_set_eq[simp]:
"\<And> t. arch_tcb_context_set (arch_tcb_context_get t) t = t"
lemma (in TcbAcc_AI_arch_tcb_context_set_eq) thread_get_as_user:
"thread_get (arch_tcb_context_get o tcb_arch) t = as_user t get"
apply (simp add: thread_get_def as_user_def)
apply (rule bind_cong [OF refl])
apply (clarsimp simp: gets_the_member set_object_def get_object_def in_monad bind_assoc
gets_def put_def bind_def get_def return_def select_f_def
dest!: get_tcb_SomeD)
apply (subgoal_tac "(kheap s)(t \<mapsto> TCB v) = kheap s", simp)
apply fastforce
done
lemma thread_set_as_user:
"thread_set (\<lambda>tcb. tcb \<lparr> tcb_arch := arch_tcb_context_set (f $ arch_tcb_context_get (tcb_arch tcb)) (tcb_arch tcb) \<rparr>) t
= as_user t (modify f)"
proof -
have P: "\<And>f. det (modify f)"
by (simp add: modify_def)
thus ?thesis
apply (simp add: as_user_def P thread_set_def)
apply (clarsimp simp add: select_f_def simpler_modify_def bind_def image_def)
done
qed
lemma ball_tcb_cap_casesI:
"\<lbrakk> P (tcb_ctable, tcb_ctable_update, (\<lambda>_ _. \<top>));
P (tcb_vtable, tcb_vtable_update, (\<lambda>_ _. is_valid_vtable_root or ((=) cap.NullCap)));
P (tcb_reply, tcb_reply_update, (\<lambda>t st c. (is_master_reply_cap c
\<and> obj_ref_of c = t
\<and> AllowGrant \<in> cap_rights c)
\<or> (halted st \<and> (c = cap.NullCap))));
P (tcb_caller, tcb_caller_update, (\<lambda>_ st. case st of
Structures_A.BlockedOnReceive e data \<Rightarrow>
((=) cap.NullCap)
| _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)));
P (tcb_ipcframe, tcb_ipcframe_update, (\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap))) \<rbrakk>
\<Longrightarrow> \<forall>x \<in> ran tcb_cap_cases. P x"
by (simp add: tcb_cap_cases_def)
lemma thread_set_typ_at[wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> thread_set f p' \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
apply (simp add: thread_set_def set_object_def get_object_def)
apply wp
apply clarsimp
apply (drule get_tcb_SomeD)
apply (clarsimp simp: obj_at_def a_type_def)
done
lemma thread_set_tcb[wp]:
"\<lbrace>tcb_at t\<rbrace> thread_set t' f \<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
by (simp add: thread_set_typ_at [where P="\<lambda>s. s"] tcb_at_typ)
lemma thread_set_no_change_tcb_pred:
assumes x: "\<And>tcb. proj (tcb_to_itcb (f tcb)) = proj (tcb_to_itcb tcb)"
shows "\<lbrace>pred_tcb_at proj P t\<rbrace> thread_set f t' \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>"
apply (simp add: thread_set_def pred_tcb_at_def)
apply wp
apply (rule set_object_at_obj)
apply wp
apply (clarsimp simp: obj_at_def)
apply (drule get_tcb_SomeD)
apply (clarsimp simp: x)
done
lemmas thread_set_no_change_tcb_state=thread_set_no_change_tcb_pred[where proj="itcb_state",simplified]
lemmas thread_set_no_change_tcb_bound_notification = thread_set_no_change_tcb_pred[where proj="itcb_bound_notification", simplified]
lemma thread_set_no_change_tcb_pred_converse:
assumes x: "\<And>tcb. proj (tcb_to_itcb (f tcb)) = proj (tcb_to_itcb tcb)"
shows "\<lbrace>\<lambda>s. \<not> pred_tcb_at proj P t s\<rbrace> thread_set f t' \<lbrace>\<lambda>rv s. \<not> pred_tcb_at proj P t s\<rbrace>"
apply (wpsimp wp: set_object_wp
simp: thread_set_def pred_tcb_at_def obj_at_def)
by (simp add: get_tcb_SomeD x)
lemmas thread_set_no_change_tcb_state_converse=
thread_set_no_change_tcb_pred_converse[where proj="itcb_state", simplified]
lemmas thread_set_no_change_tcb_bound_notification_converse =
thread_set_no_change_tcb_pred_converse[where proj="itcb_bound_notification", simplified]
lemma pspace_valid_objsE:
assumes p: "kheap s p = Some ko"
assumes v: "valid_objs s"
assumes Q: "\<lbrakk>kheap s p = Some ko; valid_obj p ko s\<rbrakk> \<Longrightarrow> Q"
shows "Q"
proof -
from p have "ko_at ko p s" by (simp add: obj_at_def)
with v show Q by (auto elim: obj_at_valid_objsE simp: Q)
qed
schematic_goal tcb_ipcframe_in_cases:
"(tcb_ipcframe, ?x) \<in> ran tcb_cap_cases"
by (fastforce simp add: ran_tcb_cap_cases)
lemmas valid_ipc_buffer_cap_simps= valid_ipc_buffer_cap_def[split_simps cap.split]
locale TcbAcc_AI_valid_ipc_buffer_cap_0 =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes valid_ipc_buffer_cap_0[simp]:
"\<And>cap buf. valid_ipc_buffer_cap cap buf \<Longrightarrow> valid_ipc_buffer_cap cap 0"
assumes thread_set_hyp_refs_trivial:
"(\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow>
(\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb) \<Longrightarrow>
\<lbrace>\<lambda>(s::'state_ext state). P (state_hyp_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
context TcbAcc_AI_valid_ipc_buffer_cap_0 begin
lemma thread_set_valid_objs_triv:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
assumes z: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
assumes w: "\<And>tcb. tcb_ipc_buffer (f tcb) = tcb_ipc_buffer tcb
\<or> (tcb_ipc_buffer (f tcb) = 0)"
assumes y: "\<And>tcb. tcb_fault_handler (f tcb) \<noteq> tcb_fault_handler tcb
\<longrightarrow> length (tcb_fault_handler (f tcb)) = word_bits"
assumes a: "\<And>tcb. tcb_fault (f tcb) \<noteq> tcb_fault tcb
\<longrightarrow> (case tcb_fault (f tcb) of None \<Rightarrow> True
| Some f \<Rightarrow> valid_fault f)"
assumes b: "\<And>tcb. tcb_bound_notification (f tcb) \<noteq> tcb_bound_notification tcb
\<longrightarrow> tcb_bound_notification (f tcb) = None"
assumes c: "\<And>tcb s::'z::state_ext state.
valid_arch_tcb (tcb_arch (f tcb)) s = valid_arch_tcb (tcb_arch tcb) s"
shows "\<lbrace>valid_objs\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_objs :: 'z::state_ext state \<Rightarrow> bool\<rbrace>"
using bspec [OF x, OF tcb_ipcframe_in_cases]
apply (simp add: thread_set_def)
apply wp
apply clarsimp
apply (drule get_tcb_SomeD)
apply (erule (1) pspace_valid_objsE)
apply (clarsimp simp add: valid_obj_def valid_tcb_def valid_bound_ntfn_def z
split_paired_Ball obj_at_def c
a_type_def bspec_split[OF x])
apply (rule conjI)
apply (elim allEI)
apply auto[1]
apply (rule conjI)
apply (cut_tac tcb = y in w)
apply (auto simp: valid_ipc_buffer_cap_simps)[1]
apply (cut_tac tcb=y in y)
apply (cut_tac tcb=y in a)
apply (cut_tac tcb=y in b)
by auto[1]
end
lemma thread_set_aligned [wp]:
"\<lbrace>pspace_aligned\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_aligned)
apply (clarsimp simp: a_type_def)
done
lemma thread_set_distinct [wp]:
"\<lbrace>pspace_distinct\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_distinct)
apply clarsimp
done
lemma thread_set_cur_tcb:
shows "\<lbrace>\<lambda>s. cur_tcb s\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. cur_tcb s\<rbrace>"
apply (simp add: cur_tcb_def)
apply (clarsimp simp: thread_set_def pred_tcb_at_def set_object_def get_object_def
in_monad gets_the_def valid_def)
apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def is_tcb)
done
lemma thread_set_iflive_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
assumes z: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
assumes y: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
assumes a: "\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb"
shows "\<lbrace>if_live_then_nonz_cap\<rbrace> thread_set f t \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_iflive)
apply (clarsimp dest!: get_tcb_SomeD)
apply (clarsimp simp: obj_at_def get_tcb_def
split_paired_Ball
bspec_split [OF x])
apply (subgoal_tac "live (TCB y)")
apply (fastforce elim: if_live_then_nonz_capD2)
apply (clarsimp simp: live_def hyp_live_tcb_def z y a)
done
lemma thread_set_ifunsafe_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>if_unsafe_then_cap\<rbrace> thread_set f t \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_ifunsafe)
apply (clarsimp simp: x)
done
lemma thread_set_zombies_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>zombies_final\<rbrace> thread_set f t \<lbrace>\<lambda>rv. zombies_final\<rbrace>"
apply (simp add: thread_set_def)
apply wp
apply (clarsimp simp: x)
done
(* FIXME-NTFN: possible need for assumption on tcb_bound_notification *)
lemma thread_set_refs_trivial:
assumes x: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
assumes y: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
shows "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>"
apply (simp add: thread_set_def set_object_def get_object_def)
apply wp
apply (clarsimp dest!: get_tcb_SomeD)
apply (clarsimp simp: state_refs_of_def get_tcb_def x y
elim!: rsubst[where P=P]
intro!: ext)
done
lemma thread_set_valid_idle_trivial:
assumes "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
assumes "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
assumes "\<And>tcb. tcb_iarch (f tcb) = tcb_iarch tcb"
shows "\<lbrace>valid_idle\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_idle\<rbrace>"
apply (simp add: thread_set_def set_object_def get_object_def valid_idle_def)
apply wp
apply (clarsimp simp: assms get_tcb_def pred_tcb_at_def obj_at_def)
done
crunch thread_set
for it[wp]: "\<lambda>s. P (idle_thread s)"
lemma thread_set_caps_of_state_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
apply (simp add: thread_set_def set_object_def get_object_def)
apply wp
apply (clarsimp elim!: rsubst[where P=P]
intro!: ext
dest!: get_tcb_SomeD)
apply (subst caps_of_state_after_update)
apply (clarsimp simp: obj_at_def get_tcb_def bspec_split [OF x])
apply simp
done
crunch thread_set
for irq_node[wp]: "\<lambda>s. P (interrupt_irq_node s)"
lemma thread_set_global_refs_triv:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>valid_global_refs\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_global_refs\<rbrace>"
apply (rule valid_global_refs_cte_lift)
apply (wp thread_set_caps_of_state_trivial x)+
done
lemma thread_set_valid_reply_caps_trivial:
assumes x: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
assumes z: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>valid_reply_caps\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>"
by (wp valid_reply_caps_st_cte_lift thread_set_caps_of_state_trivial
thread_set_no_change_tcb_state x z)
lemma thread_set_valid_reply_masters_trivial:
assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>valid_reply_masters\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>"
by (wp valid_reply_masters_cte_lift thread_set_caps_of_state_trivial y)
crunch thread_set
for interrupt_states[wp]: "\<lambda>s. P (interrupt_states s)"
lemma thread_set_obj_at_impossible:
"\<lbrakk> \<And>tcb. \<not> (P (TCB tcb)) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. obj_at P p s\<rbrace> thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>"
apply (simp add: thread_set_def set_object_def get_object_def)
apply wp
apply (clarsimp dest!: get_tcb_SomeD)
apply (clarsimp simp: obj_at_def)
done
lemma tcb_not_empty_table:
"\<not> empty_table S (TCB tcb)"
by (simp add: empty_table_def)
(*
lemmas thread_set_arch_caps_trivial
= valid_arch_caps_lift_weak[OF thread_set_arch thread_set.aobj_at
thread_set_caps_of_state_trivial, simplified] *)
lemmas thread_set_arch_caps_trivial
= valid_arch_caps_lift_weak[OF thread_set.arch_state thread_set.vsobj_at
thread_set_caps_of_state_trivial, simplified]
lemma thread_set_only_idle:
"\<lbrace>only_idle and K (\<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> \<not>idle (tcb_state (f tcb)))\<rbrace>
thread_set f t \<lbrace>\<lambda>_. only_idle\<rbrace>"
apply (simp add: thread_set_def set_object_def get_object_def)
apply wp
apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def)
apply (drule get_tcb_SomeD)
apply force
done
lemma thread_set_pspace_in_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_pspace_in_kernel_window)
apply (clarsimp simp: obj_at_def dest!: get_tcb_SomeD)
done
crunch thread_set
for pspace_respects_device_region[wp]: "pspace_respects_device_region"
(wp: set_object_pspace_respects_device_region)
lemma thread_set_cap_refs_in_kernel_window:
assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows
"\<lbrace>cap_refs_in_kernel_window\<rbrace> thread_set f t \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_cap_refs_in_kernel_window)
apply (clarsimp simp: obj_at_def)
apply (clarsimp dest!: get_tcb_SomeD)
apply (drule bspec[OF y])
apply simp
apply (erule sym)
done
lemma thread_set_cap_refs_respects_device_region:
assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows
"\<lbrace>cap_refs_respects_device_region\<rbrace> thread_set f t \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_cap_refs_respects_device_region)
apply (clarsimp simp: obj_at_def)
apply (clarsimp dest!: get_tcb_SomeD)
apply (drule bspec[OF y])
apply simp
apply (erule sym)
done
lemma thread_set_ioports:
assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows
"\<lbrace>valid_ioports\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
by (wpsimp wp: valid_ioports_lift thread_set_caps_of_state_trivial y)
(* NOTE: The function "thread_set f p" updates a TCB at p using function f.
It should not be used to change capabilities, though. *)
lemma thread_set_valid_ioc_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>valid_ioc\<rbrace> thread_set f p \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
apply (simp add: thread_set_def, wp set_object_valid_ioc_caps)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (clarsimp simp: valid_ioc_def)
apply (drule spec, drule spec, erule impE, assumption)
apply (cut_tac tcb=y in x)
apply (clarsimp simp: cte_wp_at_cases get_tcb_def cap_of_def null_filter_def
split_def tcb_cnode_map_tcb_cap_cases
split: option.splits Structures_A.kernel_object.splits)
apply (drule_tac x="(get,set,restr)" in bspec)
apply (fastforce simp: ranI)+
done
context TcbAcc_AI_valid_ipc_buffer_cap_0 begin
lemma thread_set_invs_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
assumes z: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
assumes z': "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
assumes z'': "\<And>tcb. tcb_iarch (f tcb) = tcb_iarch tcb"
assumes w: "\<And>tcb. tcb_ipc_buffer (f tcb) = tcb_ipc_buffer tcb
\<or> (tcb_ipc_buffer (f tcb) = 0)"
assumes y: "\<And>tcb. tcb_fault_handler (f tcb) \<noteq> tcb_fault_handler tcb
\<longrightarrow> length (tcb_fault_handler (f tcb)) = word_bits"
assumes a: "\<And>tcb. tcb_fault (f tcb) \<noteq> tcb_fault tcb
\<longrightarrow> (case tcb_fault (f tcb) of None \<Rightarrow> True
| Some f \<Rightarrow> valid_fault f)"
assumes arch: "\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb"
shows "\<lbrace>invs::'state_ext state \<Rightarrow> bool\<rbrace> thread_set f t \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def)
apply (rule hoare_weaken_pre)
apply (wp thread_set_valid_objs_triv thread_set_ioports
thread_set_refs_trivial
thread_set_hyp_refs_trivial
thread_set_iflive_trivial
thread_set_mdb
thread_set_ifunsafe_trivial
thread_set_cur_tcb
thread_set_zombies_trivial
thread_set_valid_idle_trivial
thread_set_global_refs_triv
thread_set_valid_reply_caps_trivial
thread_set_valid_reply_masters_trivial
thread_set_valid_ioc_trivial
valid_irq_node_typ valid_irq_handlers_lift
thread_set_caps_of_state_trivial
thread_set_arch_caps_trivial thread_set_only_idle
thread_set_cap_refs_in_kernel_window
thread_set_cap_refs_respects_device_region
thread_set_aligned
| rule x z z' z'' w y a arch valid_tcb_arch_ref_lift [THEN fun_cong]
| erule bspec_split [OF x] | simp add: z')+
apply (simp add: z)
done
end
lemma thread_set_cte_wp_at_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
getF (f tcb) = getF tcb"
shows "\<lbrace>\<lambda>s. Q (cte_wp_at P p s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. Q (cte_wp_at P p s)\<rbrace>"
by (auto simp: cte_wp_at_caps_of_state
intro: thread_set_caps_of_state_trivial [OF x])
lemma det_query_twice:
assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
assumes y: "det f"
shows "do x \<leftarrow> f; y :: tcb \<leftarrow> f; g x y od
= do x \<leftarrow> f; g x x od"
apply (subgoal_tac "\<exists>fn. f = (\<lambda>s. ({(fn s, s)}, False))")
apply clarsimp
apply (rule bind_cong [OF refl])
apply (simp add: bind_def)
apply (rule_tac x="\<lambda>s. fst (THE x. x \<in> fst (f s))" in exI)
apply (rule ext)
apply (insert y, simp add: det_def)
apply (erule_tac x=s in allE)
apply clarsimp
apply (rule sym)
apply (rule state_unchanged [OF x])
apply simp
done
lemma as_user_wp_thread_set_helper:
assumes x: "
\<lbrace>P\<rbrace> do
tcb \<leftarrow> gets_the (get_tcb t);
p \<leftarrow> select_f (m (arch_tcb_context_get (tcb_arch tcb)));
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>) t
od \<lbrace>\<lambda>rv. Q\<rbrace>"
shows "\<lbrace>P\<rbrace> as_user t m \<lbrace>\<lambda>rv. Q\<rbrace>"
proof -
have P: "\<And>P Q a b c f.
\<lbrace>P\<rbrace> do x \<leftarrow> a; y \<leftarrow> b x; z \<leftarrow> c x y; return (f x y z) od \<lbrace>\<lambda>rv. Q\<rbrace>
= \<lbrace>P\<rbrace> do x \<leftarrow> a; y \<leftarrow> b x; c x y od \<lbrace>\<lambda>rv. Q\<rbrace>"
apply (simp add: valid_def bind_def return_def split_def)
done
have Q: "do
tcb \<leftarrow> gets_the (get_tcb t);
p \<leftarrow> select_f (m (arch_tcb_context_get (tcb_arch tcb)));
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>) t
od
= do
tcb \<leftarrow> gets_the (get_tcb t);
p \<leftarrow> select_f (m (arch_tcb_context_get (tcb_arch tcb)));
set_object t (TCB (tcb \<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))
od"
apply (simp add: thread_set_def)
apply (rule ext)
apply (rule bind_apply_cong [OF refl])+
apply (simp add: select_f_def in_monad gets_the_def gets_def)
apply (clarsimp simp add: get_def bind_def return_def assert_opt_def)
done
show ?thesis
apply (simp add: as_user_def split_def)
apply (simp add: P x [simplified Q])
done
qed
context TcbAcc_AI_valid_ipc_buffer_cap_0 begin
end
lemma as_user_psp_distinct[wp]:
"\<lbrace>pspace_distinct\<rbrace> as_user t m \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>"
by (wp as_user_wp_thread_set_helper) simp
lemma as_user_psp_aligned[wp]:
"\<lbrace>pspace_aligned\<rbrace> as_user t m \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>"
by (wp as_user_wp_thread_set_helper) simp
context TcbAcc_AI_valid_ipc_buffer_cap_0 begin
lemma as_user_objs [wp]:
"\<lbrace>valid_objs\<rbrace> as_user a f \<lbrace>\<lambda>rv. valid_objs\<rbrace>"
apply (wp as_user_wp_thread_set_helper
thread_set_valid_objs_triv)
apply (wpsimp simp: ran_tcb_cap_cases valid_arch_arch_tcb_context_set)+
done
end
lemma as_user_idle[wp]:
"\<lbrace>valid_idle\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_idle\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def split_def)
apply wp
apply (clarsimp cong: if_cong)
apply (clarsimp simp: obj_at_def get_tcb_def valid_idle_def pred_tcb_at_def
split: option.splits Structures_A.kernel_object.splits)
done
lemma as_user_reply[wp]:
"\<lbrace>valid_reply_caps\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>"
by (wp as_user_wp_thread_set_helper thread_set_valid_reply_caps_trivial
ball_tcb_cap_casesI | simp)+
lemma as_user_reply_masters[wp]:
"\<lbrace>valid_reply_masters\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>"
by (wp as_user_wp_thread_set_helper thread_set_valid_reply_masters_trivial
ball_tcb_cap_casesI | simp)+
lemma as_user_arch[wp]:
"\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
apply (simp add: as_user_def split_def)
apply wp
apply simp
done
lemma as_user_irq_handlers[wp]:
"\<lbrace>valid_irq_handlers\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_irq_handlers\<rbrace>"
apply (rule as_user_wp_thread_set_helper)
apply (wp valid_irq_handlers_lift thread_set_caps_of_state_trivial
ball_tcb_cap_casesI | simp)+
done
lemma as_user_iflive[wp]:
"\<lbrace>if_live_then_nonz_cap\<rbrace> as_user t f \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>"
by (wp as_user_wp_thread_set_helper thread_set_iflive_trivial
ball_tcb_cap_casesI | simp add:)+
lemma as_user_ifunsafe[wp]:
"\<lbrace>if_unsafe_then_cap\<rbrace> as_user t f \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace>"
by (wp as_user_wp_thread_set_helper thread_set_ifunsafe_trivial
ball_tcb_cap_casesI | simp)+
lemma as_user_zombies[wp]:
"\<lbrace>zombies_final\<rbrace> as_user t f \<lbrace>\<lambda>_. zombies_final\<rbrace>"
by (wp as_user_wp_thread_set_helper thread_set_zombies_trivial
ball_tcb_cap_casesI | simp)+
lemma as_user_refs_of[wp]:
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
as_user t m
\<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>"
apply (wp as_user_wp_thread_set_helper
thread_set_refs_trivial | simp)+
done
lemma as_user_caps [wp]:
"\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> as_user a f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
apply (simp add: as_user_def split_def set_object_def get_object_def)
apply wp
apply (clarsimp cong: if_cong)
apply (clarsimp simp: get_tcb_def split: option.splits Structures_A.kernel_object.splits)
apply (subst cte_wp_caps_of_lift)
prefer 2
apply simp
apply (clarsimp simp: cte_wp_at_cases tcb_cap_cases_def)
done
crunch as_user
for it[wp]: "\<lambda>s. P (idle_thread s)"
(simp: crunch_simps)
crunch as_user
for irq_node[wp]: "\<lambda>s. P (interrupt_irq_node s)"
(simp: crunch_simps)
lemma as_user_global_refs [wp]:
"\<lbrace>valid_global_refs\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_global_refs\<rbrace>"
by (rule valid_global_refs_cte_lift) wp+
declare thread_set_cur_tcb [wp]
lemma as_user_ct: "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> as_user t m \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
apply (simp add: as_user_def split_def set_object_def get_object_def)
apply wp
apply simp
done
lemma as_user_cur [wp]:
"\<lbrace>cur_tcb\<rbrace> as_user t f \<lbrace>\<lambda>_. cur_tcb\<rbrace>"
by (wp as_user_wp_thread_set_helper) simp
lemma as_user_cte_wp_at [wp]:
"\<lbrace>\<lambda>s. P (cte_wp_at P' c s)\<rbrace> as_user p' f \<lbrace>\<lambda>rv s. P (cte_wp_at P' c s)\<rbrace>"
by (wp as_user_wp_thread_set_helper
thread_set_cte_wp_at_trivial
ball_tcb_cap_casesI | simp)+
lemma as_user_ex_nonz_cap_to[wp]:
"\<lbrace>ex_nonz_cap_to p\<rbrace> as_user t m \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>"
by (wp ex_nonz_cap_to_pres)
lemma as_user_pred_tcb_at [wp]:
"\<lbrace>pred_tcb_at proj P t\<rbrace> as_user t' m \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>"
by (wp as_user_wp_thread_set_helper thread_set_no_change_tcb_pred
| simp add: tcb_to_itcb_def)+
lemma ct_in_state_thread_state_lift:
assumes ct: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
assumes st: "\<And>t. \<lbrace>st_tcb_at P t\<rbrace> f \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>"
shows "\<lbrace>ct_in_state P\<rbrace> f \<lbrace>\<lambda>_. ct_in_state P\<rbrace>"
apply (clarsimp simp: ct_in_state_def)
apply (clarsimp simp: valid_def)
apply (frule (1) use_valid [OF _ ct])
apply (drule (1) use_valid [OF _ st], assumption)
done
lemma as_user_ct_in_state:
"\<lbrace>ct_in_state x\<rbrace> as_user t f \<lbrace>\<lambda>_. ct_in_state x\<rbrace>"
by (rule ct_in_state_thread_state_lift) (wpsimp wp: as_user_ct)+
lemma set_object_ntfn_at:
"\<lbrace> ntfn_at p and tcb_at r \<rbrace> set_object r obj \<lbrace> \<lambda>rv. ntfn_at p \<rbrace>"
apply (rule set_object_at_obj2)
apply (clarsimp simp: is_obj_defs)
done
lemma gts_wf[wp]: "\<lbrace>tcb_at t and invs\<rbrace> get_thread_state t \<lbrace>valid_tcb_state\<rbrace>"
apply (simp add: get_thread_state_def thread_get_def)
apply wp
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
valid_objs_def get_tcb_def dom_def
split: option.splits Structures_A.kernel_object.splits)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def valid_tcb_def)
done
lemma idle_thread_idle[wp]:
"\<lbrace>\<lambda>s. valid_idle s \<and> t = idle_thread s\<rbrace> get_thread_state t \<lbrace>\<lambda>r s. idle r\<rbrace>"
apply (clarsimp simp: valid_def get_thread_state_def thread_get_def bind_def return_def
gets_the_def gets_def get_def assert_opt_def get_tcb_def
fail_def valid_idle_def obj_at_def pred_tcb_at_def
split: option.splits Structures_A.kernel_object.splits)
done
lemma set_thread_state_valid_objs[wp]:
"\<lbrace>valid_objs and valid_tcb_state st and
(\<lambda>s. (\<forall>a data. st = Structures_A.BlockedOnReceive a data \<longrightarrow>
cte_wp_at ((=) cap.NullCap) (thread, tcb_cnode_index 3) s) \<and>
(st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or>
cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread)
(thread, tcb_cnode_index 2) s))\<rbrace>
set_thread_state thread st
\<lbrace>\<lambda>r. valid_objs\<rbrace>"
apply (simp add: set_thread_state_def)
apply (wp, simp, (wp set_object_valid_objs)+)
apply (clarsimp simp: obj_at_def get_tcb_def is_tcb
split: Structures_A.kernel_object.splits option.splits)
apply (simp add: valid_objs_def dom_def)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def valid_tcb_def
a_type_def tcb_cap_cases_def)
(* very slow *)
by (erule cte_wp_atE disjE
| clarsimp simp: st_tcb_def2 tcb_cap_cases_def
dest!: get_tcb_SomeD
split: Structures_A.thread_state.splits)+
lemma set_bound_notification_valid_objs[wp]:
"\<lbrace>valid_objs and valid_bound_ntfn ntfn\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (wp set_object_valid_objs, simp)
apply (clarsimp simp: obj_at_def get_tcb_def is_tcb
split: option.splits kernel_object.splits)
apply (erule (1) valid_objsE)
apply (auto simp: valid_obj_def valid_tcb_def tcb_cap_cases_def)
done
lemma set_thread_state_aligned[wp]:
"\<lbrace>pspace_aligned\<rbrace>
set_thread_state thread st
\<lbrace>\<lambda>r. pspace_aligned\<rbrace>"
apply (simp add: set_thread_state_def)
apply (wp set_object_aligned|clarsimp)+
done
lemma set_bound_notification_aligned[wp]:
"\<lbrace>pspace_aligned\<rbrace>
set_bound_notification thread ntfn
\<lbrace>\<lambda>r. pspace_aligned\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (wp set_object_aligned)
apply clarsimp
done
lemma set_thread_state_typ_at [wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_thread_state st p' \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
apply (simp add: set_thread_state_def set_object_def get_object_def)
apply (wp|clarsimp)+
apply (clarsimp simp: obj_at_def a_type_def dest!: get_tcb_SomeD)
done
crunch set_bound_notification
for typ_at[wp]: "\<lambda>s. P (typ_at T p s)"
lemma set_thread_state_tcb[wp]:
"\<lbrace>tcb_at t\<rbrace> set_thread_state ts t' \<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
by (simp add: tcb_at_typ, wp)
lemma set_bound_notification_tcb[wp]:
"\<lbrace>tcb_at t\<rbrace> set_bound_notification t' ntfn \<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
by (simp add: tcb_at_typ, wp)
lemma set_thread_state_cte_wp_at [wp]:
"\<lbrace>cte_wp_at P c\<rbrace> set_thread_state st p' \<lbrace>\<lambda>rv. cte_wp_at P c\<rbrace>"
apply (simp add: set_thread_state_def set_object_def get_object_def)
apply (wp|simp)+
apply (clarsimp cong: if_cong)
apply (drule get_tcb_SomeD)
apply (auto simp: cte_wp_at_cases tcb_cap_cases_def)
done
lemma set_bound_notification_cte_wp_at [wp]:
"\<lbrace>cte_wp_at P c\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. cte_wp_at P c\<rbrace>"
apply (simp add: set_bound_notification_def set_object_def get_object_def)
apply (wp, simp)
apply (clarsimp cong: if_cong)
apply (drule get_tcb_SomeD)
apply (auto simp: cte_wp_at_cases tcb_cap_cases_def)
done
lemma set_object_tcb_at [wp]:
"\<lbrace> tcb_at t' \<rbrace> set_object t (TCB x) \<lbrace>\<lambda>_. tcb_at t'\<rbrace>"
by (rule set_object_at_obj1) (simp add: is_tcb)
lemma as_user_tcb [wp]: "\<lbrace>tcb_at t'\<rbrace> as_user t m \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>"
apply (simp add: as_user_def split_def)
apply wp
apply simp
done
lemma fold_fun_upd:
"distinct keys \<Longrightarrow>
foldl (\<lambda>s (k, v). s(k := v)) s (zip keys vals) key
= (if key \<in> set (take (length vals) keys)
then vals ! (the_index keys key)
else s key)"
apply (induct keys arbitrary: vals s)
apply simp
apply (case_tac vals, simp_all split del: if_split)
apply (case_tac "key = a", simp_all split del: if_split)
apply clarsimp
apply (drule in_set_takeD)
apply simp
apply clarsimp
done
lemma load_word_offs_P[wp]:
"\<lbrace>P\<rbrace> load_word_offs a x \<lbrace>\<lambda>_. P\<rbrace>"
unfolding load_word_offs_def
by (wp dmo_inv loadWord_inv)
lemma valid_tcb_objs:
assumes vs: "valid_objs s"
assumes somet: "get_tcb thread s = Some y"
shows "valid_tcb thread y s"
proof -
from somet have inran: "kheap s thread = Some (TCB y)"
by (clarsimp simp: get_tcb_def
split: option.splits Structures_A.kernel_object.splits)
with vs have "valid_obj thread (TCB y) s"
by (fastforce simp: valid_objs_def dom_def)
thus ?thesis by (simp add: valid_tcb_def valid_obj_def)
qed
locale TcbAcc_AI_get_cap_valid_ipc =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes get_cap_valid_ipc:
"\<And>v t.
\<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t\<rbrace>
get_cap (t, tcb_cnode_index 4)
\<lbrace>\<lambda>rv (s::'state_ext state). valid_ipc_buffer_cap rv v\<rbrace>"
lemma get_cap_aligned:
"\<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. cap_aligned rv\<rbrace>"
apply (rule hoare_strengthen_post, rule get_cap_valid)
apply (clarsimp simp: valid_cap_def)
done
lemma shiftr_eq_mask_eq:
"a && ~~ mask b = c && ~~ mask b \<Longrightarrow> a >> b = c >> b"
apply (rule word_eqI)
apply (drule_tac x="b + n" in word_eqD)
apply (case_tac "b + n < size a")
apply (simp add: nth_shiftr word_size word_ops_nth_size)
apply (auto dest!: test_bit_size simp: word_size)
done
lemma thread_get_wp:
"\<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (f tcb) s) ptr s\<rbrace>
thread_get f ptr
\<lbrace>P\<rbrace>"
apply (clarsimp simp: valid_def obj_at_def)
apply (frule in_inv_by_hoareD [OF thread_get_inv])
apply (clarsimp simp: thread_get_def bind_def gets_the_def
assert_opt_def split_def return_def fail_def
gets_def get_def
split: option.splits
dest!: get_tcb_SomeD)
done
lemma thread_get_sp:
"\<lbrace>P\<rbrace> thread_get f ptr
\<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> f tcb = rv) ptr and P\<rbrace>"
apply (clarsimp simp: valid_def obj_at_def)
apply (frule in_inv_by_hoareD [OF thread_get_inv])
apply (clarsimp simp: thread_get_def bind_def gets_the_def
assert_opt_def split_def return_def fail_def
gets_def get_def
split: option.splits
dest!: get_tcb_SomeD)
done
lemma gbn_wp:
"\<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (tcb_bound_notification tcb) s) ptr s \<rbrace>
get_bound_notification ptr
\<lbrace>P\<rbrace>"
apply (simp add: get_bound_notification_def)
apply (wp thread_get_wp | clarsimp)+
done
lemmas thread_get_obj_at_eq = thread_get_sp[where P=\<top>, simplified]
lemma wf_cs_0:
"well_formed_cnode_n sz cn \<Longrightarrow> \<exists>n. n \<in> dom cn \<and> bl_to_bin n = 0"
unfolding well_formed_cnode_n_def
apply clarsimp
apply (rule_tac x = "replicate sz False" in exI)
apply (simp add: bl_to_bin_rep_False)
done
lemma ct_active_st_tcb_at_weaken:
"\<lbrakk> st_tcb_at P (cur_thread s) s;
\<And>st. P st \<Longrightarrow> active st\<rbrakk>
\<Longrightarrow> ct_active s"
apply (unfold ct_in_state_def)
apply (erule pred_tcb_weakenE)
apply auto
done
lemma ct_in_state_decomp:
assumes x: "\<lbrace>\<lambda>s. t = (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. t = (cur_thread s)\<rbrace>"
assumes y: "\<lbrace>Pre\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at Prop t\<rbrace>"
shows "\<lbrace>\<lambda>s. Pre s \<and> t = (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv. ct_in_state Prop\<rbrace>"
apply (rule hoare_post_imp[where Q'="\<lambda>rv s. t = cur_thread s \<and> st_tcb_at Prop t s"])
apply (clarsimp simp add: ct_in_state_def)
apply (rule hoare_weaken_pre)
apply (wp x y)
apply simp
done
(**********************************************************
!@!@!@!@!@!@!@! UNINTERLEAVE SBA STUFF !@!@!@!@!@!@!@!@!
**********************************************************)
lemma sts_st_tcb_at:
"\<lbrace>\<top>\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>r. r = ts) t\<rbrace>"
by (simp add: set_thread_state_def pred_tcb_at_def | wp set_object_at_obj3)+
lemma sbn_bound_tcb_at:
"\<lbrace>\<top>\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at (\<lambda>r. r = ntfn) t\<rbrace>"
by (simp add: set_bound_notification_def pred_tcb_at_def | wp set_object_at_obj3)+
lemma sts_st_tcb_at':
"\<lbrace>K (P ts)\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>"
apply (rule hoare_assume_pre)
apply (rule hoare_chain)
apply (rule sts_st_tcb_at)
apply simp
apply (clarsimp elim!: pred_tcb_weakenE)
done
lemma sbn_bound_tcb_at':
"\<lbrace>K (P ntfn)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t\<rbrace>"
apply (rule hoare_assume_pre)
apply (rule hoare_chain)
apply (rule sbn_bound_tcb_at)
apply simp
apply (clarsimp elim!: pred_tcb_weakenE)
done