-
Notifications
You must be signed in to change notification settings - Fork 106
/
Tcb_DR.thy
1789 lines (1687 loc) · 90.5 KB
/
Tcb_DR.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 Tcb_DR
imports Ipc_DR Arch_DR
begin
context begin interpretation Arch . (*FIXME: arch-split*)
(*
* A "normal" TCB is a non-idle TCB. (Idle is special, because it
* doesn't get lifted up to capDL.
*)
abbreviation "normal_tcb_at x \<equiv> (tcb_at x) and (not_idle_thread x)"
(*
* Translate an abstract spec TCB invocation into a CDL TCB invocation.
*)
definition translate_tcb_invocation_thread_ctrl_buffer :: "(word32 \<times> (cap\<times> word32\<times> bool list) option) option \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) option"
where
"translate_tcb_invocation_thread_ctrl_buffer buffer \<equiv>
(case buffer of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None
| Some (a, Some (c,d)) \<Rightarrow> Some (transform_cap c, (transform_cslot_ptr d)))"
definition
translate_tcb_invocation :: "Invocations_A.tcb_invocation \<Rightarrow> cdl_tcb_invocation"
where
"translate_tcb_invocation x \<equiv>
case x of
Invocations_A.ReadRegisters oid' x' _ _ \<Rightarrow>
Invocations_D.ReadRegisters oid' x' 0 0
| Invocations_A.WriteRegisters oid' b' regs' _ \<Rightarrow>
Invocations_D.WriteRegisters oid' b' [0] 0
| Invocations_A.CopyRegisters dest_tcb src_tcb a b c d e \<Rightarrow>
Invocations_D.CopyRegisters dest_tcb src_tcb a b c d 0
| Invocations_A.ThreadControl target_tcb target_slot faultep _ _ croot vroot buffer \<Rightarrow>
Invocations_D.ThreadControl
target_tcb
(transform_cslot_ptr target_slot)
(option_map of_bl faultep)
(option_map (\<lambda>r. ((transform_cap \<circ> fst) r,(transform_cslot_ptr \<circ> snd) r)) croot)
(option_map (\<lambda>r. ((transform_cap \<circ> fst) r,(transform_cslot_ptr \<circ> snd) r)) vroot)
(translate_tcb_invocation_thread_ctrl_buffer buffer)
| Invocations_A.Suspend target_tcb \<Rightarrow>
Invocations_D.Suspend target_tcb
| Invocations_A.Resume target_tcb \<Rightarrow>
Invocations_D.Resume target_tcb
| Invocations_A.NotificationControl target_tcb opt \<Rightarrow>
Invocations_D.NotificationControl target_tcb opt
| Invocations_A.SetTLSBase target_tcb x \<Rightarrow>
Invocations_D.SetTLSBase target_tcb"
lemma decode_set_ipc_buffer_translate_tcb_invocation:
"\<lbrakk>x \<noteq> [];excaps ! 0 = (a,b,c)\<rbrakk> \<Longrightarrow>
(\<And>s. \<lbrace>(=) s\<rbrace> decode_set_ipc_buffer x (cap.ThreadCap t) slot' excaps
\<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and>
translate_tcb_invocation_thread_ctrl_buffer (tc_new_buffer rv) = (if (x ! 0) = 0 then None
else Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c)))
\<rbrace>,\<lbrace>\<lambda>ft. (=) s\<rbrace>)"
apply (clarsimp simp:decode_set_ipc_buffer_def whenE_def | rule conjI)+
apply (wp , simp_all add:translate_tcb_invocation_thread_ctrl_buffer_def)
apply (clarsimp | rule conjI)+
apply (wp , clarsimp simp:translate_tcb_invocation_thread_ctrl_buffer_def)
apply (wp | clarsimp | rule conjI)+
apply (simp add:check_valid_ipc_buffer_def)
apply (wpc|wp)+
apply (simp add:derive_cap_def split del:if_split)
apply (wpsimp simp: o_def arch_derive_cap_def split_del:if_split)
apply clarsimp
apply (clarsimp simp:transform_mapping_def)
done
lemma derive_cap_translate_tcb_invocation:
"\<lbrace>(=) s\<rbrace>derive_cap a b \<lbrace>\<lambda>rv. (=) s\<rbrace>,\<lbrace>\<lambda>rv. \<top>\<rbrace>"
apply (simp add:derive_cap_def)
apply (case_tac b)
apply (clarsimp simp:ensure_no_children_def whenE_def |wp)+
apply (clarsimp simp:arch_derive_cap_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:ensure_no_children_def whenE_def |wp)+
apply (clarsimp split:option.splits | rule conjI | wp)+
done
lemma derive_cnode_cap_as_vroot:
"\<lbrace>(=) s \<rbrace> derive_cap (ba, ca) aa
\<lbrace>\<lambda>vroot_cap'.
if is_valid_vtable_root vroot_cap' then \<lambda>sa. sa = s \<and> vroot_cap' = aa
else (=) s\<rbrace>, \<lbrace>\<lambda>r. (=) s\<rbrace>"
apply (simp add:derive_cap_def is_valid_vtable_root_def)
apply (case_tac aa)
apply (clarsimp|wp)+
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def | wp)+
done
lemma derive_cnode_cap_as_croot:
"\<lbrace>(=) s\<rbrace> derive_cap (b, c) a
\<lbrace>\<lambda>croot_cap'. if Structures_A.is_cnode_cap croot_cap' then \<lambda>sa. s = sa \<and> croot_cap' = a \<and> is_cnode_cap a else (=) s\<rbrace>,\<lbrace>\<lambda>r. (=) s\<rbrace>"
apply (clarsimp simp:derive_cap_def is_cap_simps)
apply (case_tac a)
apply (clarsimp|wp)+
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def | wp)+
done
lemma valid_vtable_root_update:
"\<lbrakk> is_valid_vtable_root (CSpace_A.update_cap_data False x aa)\<rbrakk>
\<Longrightarrow> CSpace_A.update_cap_data False x aa = aa"
apply (clarsimp simp: update_cap_data_def badge_update_def is_valid_vtable_root_def Let_def
the_cnode_cap_def is_arch_cap_def arch_update_cap_data_def the_arch_cap_def
split: if_split_asm cap.split_asm)
done
lemma decode_set_space_translate_tcb_invocation:
"\<And>s. \<lbrace>(=) s\<rbrace> decode_set_space x (cap.ThreadCap t) slot' (excaps')
\<lbrace>\<lambda>rv s'. s' = s \<and>
(rv = tcb_invocation.ThreadControl t slot' (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) None) \<and>
(tc_new_fault_ep rv = Some (to_bl (x!0)))
\<and> (option_map (\<lambda>c. snd c) (tc_new_croot rv) = Some (snd (excaps' ! 0)))
\<and> (option_map (\<lambda>c. snd c) (tc_new_vroot rv) = Some (snd (excaps' ! Suc 0)))
\<and> (option_map (\<lambda>c. fst c ) (tc_new_croot rv)
= (if (x!1 = 0) then Some (fst (excaps' ! 0)) else Some (update_cap_data False (x ! Suc 0) (fst (excaps' ! 0)))))
\<and> (option_map (\<lambda>c. fst c) (tc_new_vroot rv) = Some (fst (excaps' ! Suc 0)))
\<and> (option_map (\<lambda>c. is_cnode_cap (fst c)) (tc_new_croot rv) = Some True)
\<rbrace>,\<lbrace>\<lambda>rv. (=) s\<rbrace>"
supply if_cong[cong]
apply (case_tac "excaps' ! 0")
apply (case_tac "excaps' ! Suc 0")
apply (clarsimp simp:decode_set_space_def whenE_def | rule conjI)+
apply wp
apply (clarsimp simp: | rule conjI)+
apply (wp|clarsimp)+
apply (rule_tac P ="croot_cap' = a \<and> is_cnode_cap a" in hoare_gen_asmE)
apply clarsimp
apply (rule validE_validE_R)
apply (wp hoare_strengthen_postE[OF derive_cnode_cap_as_vroot],simp)
apply (wp|clarsimp)+
apply (wp hoare_strengthen_postE[OF derive_cnode_cap_as_croot],simp)
apply (wp|clarsimp)+
apply (clarsimp simp:whenE_def | rule conjI | wp)+
apply (rule_tac P ="croot_cap' = update_cap_data False (x! 1) a \<and> is_cnode_cap croot_cap'" in hoare_gen_asmE)
apply (rule validE_validE_R)
apply simp
apply (rule_tac s1 = s in hoare_strengthen_postE[OF derive_cnode_cap_as_vroot],simp)
apply (rule conjI|simp split:if_split_asm)+
apply (wp|clarsimp)+
apply (rule validE_validE_R)
apply (rule_tac s1 = s in hoare_strengthen_postE[OF derive_cnode_cap_as_croot])
apply (wp|clarsimp)+
apply (clarsimp simp:whenE_def | rule conjI | wp)+
apply (rule_tac P ="croot_cap' = a \<and> is_cnode_cap a" in hoare_gen_asmE)
apply clarsimp
apply (rule validE_validE_R)
apply (rule_tac s1 = s in hoare_strengthen_postE[OF derive_cnode_cap_as_vroot],simp)
apply (clarsimp split:if_splits simp:valid_vtable_root_update)
apply (wp|clarsimp)+
apply (wp hoare_strengthen_postE[OF derive_cnode_cap_as_croot],simp)
apply (wp|clarsimp)+
apply (clarsimp simp: | rule conjI | wp)+
apply (rule_tac P ="croot_cap' = update_cap_data False (x! 1) a \<and> is_cnode_cap croot_cap'" in hoare_gen_asmE)
apply (rule validE_validE_R)
apply simp
apply (rule_tac s1 = s in hoare_strengthen_postE[OF derive_cnode_cap_as_vroot],simp)
apply (rule conjI|simp split:if_split_asm)+
apply (rule valid_vtable_root_update)
apply clarsimp+
apply (wp|clarsimp)+
apply (rule validE_validE_R)
apply (rule hoare_strengthen_postE[OF derive_cnode_cap_as_croot])
apply fastforce+
apply (wp|clarsimp)+
done
lemma decode_tcb_cap_label_not_match:
"\<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = Structures_A.ThreadCap t\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_tcb_invocation label' args' cap' slot' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>"
apply (simp add:Decode_A.decode_tcb_invocation_def)
apply (case_tac "gen_invocation_type label'")
apply (simp_all add:transform_intent_def flip: gen_invocation_type_eq)
apply wp
apply (simp_all add: whenE_def transform_intent_tcb_defs
split: option.splits)
apply (simp_all split:List.list.split list.split_asm option.splits add: gen_invocation_type_eq)
apply (simp add: decode_read_registers_def decode_write_registers_def decode_set_ipc_buffer_def
decode_copy_registers_def decode_set_space_def decode_tcb_configure_def
decode_set_priority_def decode_set_mcpriority_def decode_set_sched_params_def
| wp)+
done
lemma is_cnode_cap_update_cap_data:
"Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a) \<Longrightarrow> is_cnode_cap a"
apply (case_tac a)
apply (clarsimp simp:update_cap_data_def arch_update_cap_data_def is_arch_cap_def badge_update_def
is_cap_simps split:if_split_asm)+
done
lemma update_cnode_cap_data:
"\<lbrakk>Some af = (if w = 0 then Some ab else Some (CSpace_A.update_cap_data False w ab)); Structures_A.is_cnode_cap af\<rbrakk>
\<Longrightarrow> transform_cap af = cdl_update_cnode_cap_data (transform_cap ab) w"
apply (clarsimp simp:is_cap_simps)
apply (clarsimp split:if_splits)
apply (simp add:cdl_update_cnode_cap_data_def CSpace_D.update_cap_data_def)
apply (clarsimp simp: update_cap_data_def arch_update_cap_data_def split:if_splits)
apply ((cases ab,simp_all add:badge_update_def)+)[2]
apply (clarsimp simp:is_cap_simps the_cnode_cap_def word_size split:if_split_asm simp:Let_def)
apply (clarsimp simp:cdl_update_cnode_cap_data_def word_bits_def of_drop_to_bl
word_size mask_twice dest!:leI)
done
lemma decode_tcb_corres:
"\<lbrakk> Some (TcbIntent ui) = transform_intent (invocation_type label') args';
cap = transform_cap cap';
cap' = Structures_A.ThreadCap t;
slot = transform_cslot_ptr slot';
excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> (\<lambda>x y. x = translate_tcb_invocation y)) \<top> \<top>
(Tcb_D.decode_tcb_invocation cap slot excaps ui)
(Decode_A.decode_tcb_invocation label' args' cap' slot' excaps')"
supply if_cong[cong]
apply (unfold Tcb_D.decode_tcb_invocation_def Decode_A.decode_tcb_invocation_def)
apply (drule sym, frule transform_tcb_intent_invocation)
apply (unfold transform_cap_def)
apply (unfold transform_cap_list_def)
apply (case_labels "invocation_type label'")
apply (simp_all add: gen_invocation_type_eq)
(* TCBReadRegisters *)
apply (clarsimp simp: decode_read_registers_def split: list.split)
apply (intro conjI impI allI)
apply (auto)[2]
apply (unfold bindE_def)[1]
apply (rule corres_symb_exec_r[where Q'="\<lambda> rv s. True"])
apply (case_tac rv)
apply (simp add: lift_def)
apply (rule corres_alternate2, simp)
apply (simp add: lift_def)
apply (simp add: liftE_def lift_def)
apply (rule corres_symb_exec_r[where Q'="\<lambda> rv s. True"])
apply (fold bindE_def)
apply (rule dcorres_whenE_throwError_abstract')
apply (rule corres_alternate2)
apply simp
apply (rule corres_alternate1)
apply (clarsimp simp: returnOk_def translate_tcb_invocation_def)
apply wp+
apply (simp add: range_check_def unlessE_def[abs_def])
(* TCBWriteRegisters *)
apply (clarsimp simp: decode_write_registers_def split: list.split)
apply (intro impI conjI allI)
(* IRQSetMode *)
apply (clarsimp simp: transform_intent_def)
apply fastforce
apply clarsimp
apply (rule dcorres_whenE_throwError_abstract')
apply (fastforce intro: corres_alternate2 simp: throwError_def)
apply (simp add: liftE_def bindE_def lift_def)
apply (rule corres_symb_exec_r[where Q'="\<lambda> rv s. True"])
apply (fold bindE_def, rule dcorres_whenE_throwError_abstract')
apply (fastforce intro: corres_alternate2 simp: throwError_def)
apply (fastforce intro: corres_alternate1
simp: returnOk_def
translate_tcb_invocation_def)
apply wp+
(* TCBCopyRegisters *)
apply (clarsimp simp: decode_copy_registers_def)
apply (case_tac args')
apply (clarsimp simp:whenE_def dcorres_alternative_throw split:option.splits)+
apply (case_tac "map fst excaps'")
apply (clarsimp simp: dcorres_alternative_throw split:option.splits)+
apply (case_tac ab)
apply (clarsimp simp:throw_on_none_def get_index_def dcorres_alternative_throw split:option.splits)+
apply (rule corres_alternate1)
apply (clarsimp simp:returnOk_def corres_underlying_def translate_tcb_invocation_def return_def)
apply ((clarsimp simp:throw_on_none_def get_index_def dcorres_alternative_throw split:option.splits)+)[5]
(* TCBConfigures *)
apply (clarsimp simp: decode_tcb_configure_def dcorres_alternative_throw whenE_def)
apply (case_tac "excaps' ! 2")
apply (case_tac "excaps' ! Suc 0")
apply (case_tac "excaps' ! 0")
apply (rule split_return_throw_thingy)
apply (rule_tac a = a and b = b and c = c in decode_set_ipc_buffer_translate_tcb_invocation)
apply simp+
apply (rule split_return_throw_thingy)
apply (rule decode_set_space_translate_tcb_invocation)
apply (clarsimp simp: get_index_def throw_on_none_def)
apply (rule conjI | clarsimp)+
apply (rule corres_alternate1,rule dcorres_returnOk)
apply (clarsimp simp: translate_tcb_invocation_def update_cnode_cap_data)
apply clarsimp
apply (clarsimp | rule conjI)+
apply (rule corres_alternate1,rule dcorres_returnOk)
apply (clarsimp simp: translate_tcb_invocation_def update_cnode_cap_data)
apply clarsimp+
(* TCBSetPriority *)
apply (clarsimp simp: decode_set_priority_def throw_on_none_def get_index_def dcorres_alternative_throw whenE_def)
apply (case_tac "fst (excaps' ! 0)"; simp add: dcorres_alternative_throw)
apply (rule corres_throw_skip_r)
apply (rule corres_alternate1)
apply (rule dcorres_returnOk)
apply (clarsimp simp: translate_tcb_invocation_def translate_tcb_invocation_thread_ctrl_buffer_def)
apply (rule check_prio_inv)
apply fastforce
(* TCBSetMCPriority *)
apply (clarsimp simp: decode_set_mcpriority_def throw_on_none_def get_index_def dcorres_alternative_throw whenE_def)
apply (case_tac "fst (excaps' ! 0)"; simp add: dcorres_alternative_throw)
apply (rule corres_throw_skip_r)
apply (rule corres_alternate1)
apply (rule dcorres_returnOk)
apply (clarsimp simp: translate_tcb_invocation_def translate_tcb_invocation_thread_ctrl_buffer_def)
apply (rule check_prio_inv)
apply fastforce
(* TCBSetSchedParams *)
apply (clarsimp simp: decode_set_sched_params_def throw_on_none_def get_index_def dcorres_alternative_throw whenE_def)
apply (case_tac "fst (excaps' ! 0)"; simp add: dcorres_alternative_throw)
apply (rule corres_throw_skip_r)+
apply (rule corres_alternate1)
apply (rule dcorres_returnOk)
apply (clarsimp simp: translate_tcb_invocation_def translate_tcb_invocation_thread_ctrl_buffer_def)
apply (rule check_prio_inv)
apply fastforce
apply (rule check_prio_inv)
apply fastforce
(* TCBSetIPCBuffer *)
apply (clarsimp simp:transform_intent_def transform_intent_tcb_set_ipc_buffer_def)
apply (case_tac args')
apply clarsimp+
apply (case_tac "excaps' ! 0")
apply (clarsimp simp:throw_on_none_def get_index_def dcorres_alternative_throw | rule conjI)+
apply (rule corres_return_throw_thingy)
apply (rule decode_set_ipc_buffer_translate_tcb_invocation)
apply fastforce+
apply (clarsimp|rule conjI)+
apply (clarsimp simp:translate_tcb_invocation_def translate_tcb_invocation_thread_ctrl_buffer_def
split:option.splits tcb_invocation.splits)
apply (clarsimp simp:decode_set_ipc_buffer_def dcorres_alternative_throw)+
apply (rule corres_alternate1[OF dcorres_returnOk])
apply (clarsimp simp:translate_tcb_invocation_def translate_tcb_invocation_thread_ctrl_buffer_def)
(* TCBSetSpace *)
apply (clarsimp simp:throw_on_none_def get_index_def dcorres_alternative_throw | rule conjI)+
apply (rule corres_return_throw_thingy)
apply (rule decode_set_space_translate_tcb_invocation)
apply (clarsimp split del: if_split)+
apply (clarsimp simp:translate_tcb_invocation_def translate_tcb_invocation_thread_ctrl_buffer_def)
apply (case_tac "excaps' ! 0",simp,case_tac "excaps' ! Suc 0",simp)
apply (simp add:update_cnode_cap_data)
apply (simp add:decode_set_space_def dcorres_alternative_throw | rule conjI)+
(* TCBSuspend *)
apply clarsimp
apply (rule corres_alternate1[OF dcorres_returnOk])
apply (simp add: translate_tcb_invocation_def)
(* TCBResume *)
apply clarsimp
apply (rule corres_alternate1[OF dcorres_returnOk])
apply (simp add: translate_tcb_invocation_def)
(* TCBBindNotification *)
apply (clarsimp simp: decode_bind_notification_def dcorres_alternative_throw whenE_def)
apply (rule dcorres_symb_exec_rE)
apply (case_tac rv, simp)
(* please continue scrolling *)
apply (case_tac "(fst (hd excaps'))", simp_all split del: if_split)[1]
prefer 4
apply (rename_tac rights)
apply (case_tac "AllowRead \<notin> rights", simp)
apply (rule corres_alternate2, rule dcorres_throw)
apply simp
apply (rule dcorres_symb_exec_rE)
apply (case_tac "ntfn_obj rva", simp_all split del: if_split)[1]
apply (case_tac "ntfn_bound_tcb rva", simp_all split del: if_split)[1]
apply (clarsimp simp: throw_on_none_def get_index_def dcorres_alternative_throw)
apply (case_tac "excaps' ! 0", clarsimp, rule corres_alternate1[OF dcorres_returnOk], simp add: translate_tcb_invocation_def hd_conv_nth)
apply (clarsimp simp: throw_on_none_def get_index_def dcorres_alternative_throw split del: if_split)+
apply (case_tac "ntfn_bound_tcb rva", simp split del: if_split)[1]
apply (rename_tac rva word)
apply ((case_tac "excaps' ! 0",clarsimp, rule corres_alternate1[OF dcorres_returnOk], simp add: translate_tcb_invocation_def hd_conv_nth)
| clarsimp simp: throw_on_none_def get_index_def dcorres_alternative_throw split del: if_split
| wp get_simple_ko_wp
| (case_tac "excaps' ! 0", rule dcorres_alternative_throw)
| (case_tac "AllowRead \<in> rights", simp))+
(* TCBUnbindNotification *)
apply (clarsimp simp: decode_unbind_notification_def dcorres_alternative_throw whenE_def)
apply (rule dcorres_symb_exec_rE)
apply (case_tac rv, simp, rule dcorres_alternative_throw)
apply (clarsimp, rule corres_alternate1[OF dcorres_returnOk], simp add: translate_tcb_invocation_def)
apply (wp gbn_wp | clarsimp)+
(* TCBSetTLSBase *)
apply (clarsimp simp: decode_set_tls_base_def whenE_def)
apply (rule conjI; clarsimp)
apply (rule dcorres_alternative_throw)
apply (rule corres_alternate1[OF dcorres_returnOk])
apply (simp add: translate_tcb_invocation_def)
(* ARMASIDPoolAssign *)
apply (clarsimp simp: transform_intent_def)
(* ARMIRQIssueIRQHandler *)
apply (clarsimp simp: transform_intent_def)
done
(* If the argument to "as_user" is idempotent, then so is the call. *)
lemma dcorres_idempotent_as_user:
"\<lbrakk> \<And>a. \<lbrace> \<lambda>s. s = a \<rbrace> x \<lbrace> \<lambda>_ s. s = a \<rbrace> \<rbrakk> \<Longrightarrow>
dcorres dc \<top> (tcb_at u) (return q) (as_user u x)"
apply (clarsimp simp: as_user_def)
apply (clarsimp simp: corres_underlying_def bind_def split_def set_object_def get_object_def
return_def get_def put_def get_tcb_def gets_the_def gets_def assert_opt_def
tcb_at_def select_f_def valid_def
split: option.split Structures_A.kernel_object.split)
done
lemma transform_full_intent_kheap_update_eq:
"q \<noteq> u' \<Longrightarrow>
transform_full_intent (machine_state (s\<lparr>kheap := (kheap s)(u' \<mapsto> x')\<rparr>)) q =
transform_full_intent (machine_state s) q"
by simp
(* Suspend functions correspond. *)
lemma suspend_corres:
"dcorres dc \<top> (tcb_at obj_id and not_idle_thread obj_id and invs and valid_etcbs)
(Tcb_D.suspend obj_id) (IpcCancel_A.suspend obj_id)"
apply (rule corres_guard_imp)
apply (clarsimp simp: IpcCancel_A.suspend_def Tcb_D.suspend_def)
apply (rule corres_split[OF finalise_cancel_ipc])
apply (rule dcorres_symb_exec_r[OF _ gts_inv gts_inv])
apply (rule dcorres_rhs_noop_above)
apply (case_tac "rv = Running"; simp)
apply (rule update_restart_pc_dcorres)
apply simp
apply (rule dcorres_rhs_noop_below_True[OF tcb_sched_action_dcorres])
apply (rule set_thread_state_corres)
apply wp
apply (case_tac "rv = Running"; simp)
apply wp+
apply (wpsimp simp: not_idle_thread_def conj_comms)+
done
lemma dcorres_setup_reply_master:
"dcorres dc \<top> (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs)
(KHeap_D.set_cap (obj_id, tcb_replycap_slot)
(cdl_cap.MasterReplyCap obj_id))
(setup_reply_master obj_id)"
apply (clarsimp simp:setup_reply_master_def)
apply (rule_tac Q'="\<lambda>rv. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and
cte_wp_at (\<lambda>c. c = rv) (obj_id,tcb_cnode_index 2)" in corres_symb_exec_r)
prefer 2
apply (wp get_cap_cte_wp_at)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:tcb_at_def)
apply (frule valid_tcb_objs)
apply (simp add:tcb_at_def)
apply (clarsimp simp:cte_wp_at_cases dest!:get_tcb_SomeD)
apply (clarsimp simp:valid_tcb_def)
apply (clarsimp simp:tcb_cap_cases_def)
apply (case_tac "cap.NullCap = tcb_reply tcb")
apply (clarsimp simp:when_def)
apply (rule corres_guard_imp)
apply (rule dcorres_symb_exec_r)
apply (rule set_cap_corres)
apply (clarsimp simp:transform_cap_def)
apply (clarsimp simp:transform_tcb_slot_simp)
apply (wp+)[2]
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (rule TrueI)
apply (clarsimp simp: not_idle_thread_def)
apply (clarsimp simp:when_def is_master_reply_cap_def split:cap.split_asm)
apply (rename_tac rc_rights)
apply (subgoal_tac "opt_cap (obj_id,tcb_replycap_slot) (transform s')
= Some (cdl_cap.MasterReplyCap obj_id)")
apply (clarsimp simp:corres_underlying_def set_cap_is_noop_opt_cap return_def)
apply (subgoal_tac "cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights))
(obj_id,tcb_cnode_index 2) s'")
apply (clarsimp dest!:iffD1[OF cte_wp_at_caps_of_state])
apply (drule caps_of_state_transform_opt_cap)
apply simp
apply (clarsimp simp:not_idle_thread_def)
apply (simp add:transform_cap_def transform_tcb_slot_simp)
apply (clarsimp simp:cte_wp_at_cases)
apply wp
apply simp
done
lemma set_cdl_cap_noop:
" dcorres dc \<top> (cte_wp_at (\<lambda>cap. cdlcap = transform_cap cap) slot and not_idle_thread (fst slot) and valid_etcbs)
(KHeap_D.set_cap (transform_cslot_ptr slot) cdlcap)
(return x)"
apply (rule dcorres_expand_pfx)
apply clarsimp
apply (drule iffD1[OF cte_wp_at_caps_of_state])
apply clarsimp
apply (drule caps_of_state_transform_opt_cap)
apply simp
apply (simp add:not_idle_thread_def)
apply (drule set_cap_is_noop_opt_cap)
apply (clarsimp simp:corres_underlying_def return_def not_idle_thread_def set_cap_is_noop_opt_cap)
done
lemma runnable_imply:
"runnable st
\<Longrightarrow> (infer_tcb_pending_op obj_id st = RunningCap \<or>
infer_tcb_pending_op obj_id st = RestartCap)"
apply (case_tac st)
apply (simp_all add:infer_tcb_pending_op_def)
done
lemma dcorres_set_thread_state_Restart2:
"dcorres dc (\<lambda>_. True)
(\<lambda>a. valid_mdb a \<and> not_idle_thread recver a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a)
(KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap)
(set_thread_state recver Structures_A.thread_state.Restart)"
apply (simp add:KHeap_D.set_cap_def set_thread_state_def)
apply (rule dcorres_gets_the)
apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp)
apply (frule opt_object_tcb, simp)
apply (clarsimp simp:not_idle_thread_def)
apply (clarsimp simp:transform_tcb_def has_slots_def update_slots_def object_slots_def tcb_slots)
apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres])
apply (rule dcorres_set_object_tcb)
apply (clarsimp simp:transform_tcb_def infer_tcb_pending_op_def tcb_slots)
apply (rule conjI, fastforce)
apply (clarsimp simp:get_etcb_SomeD)
apply (simp add:not_idle_thread_def)
apply (clarsimp simp:get_tcb_SomeD)
apply (clarsimp simp:get_etcb_SomeD)
apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb)
apply (fastforce simp:not_idle_thread_def dest!:opt_object_tcb)
done
(* Restart functions correspond. *)
lemma restart_corres:
"dcorres dc \<top>
(invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs)
(Tcb_D.restart obj_id) (Tcb_A.restart obj_id)"
apply (clarsimp simp: Tcb_D.restart_def Tcb_A.restart_def
when_def get_cap_def)
apply (clarsimp simp: thread_get_def get_thread_state_def )
apply (rule dcorres_gets_the)
apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp:opt_cap_tcb not_idle_thread_def tcb_vspace_slot_def
tcb_pending_op_slot_def tcb_caller_slot_def tcb_ipcbuffer_slot_def
tcb_cspace_slot_def tcb_replycap_slot_def)
apply (intro conjI impI)
apply (rule corres_guard_imp)
apply (rule corres_split[OF finalise_cancel_ipc])
apply (rule corres_split[OF dcorres_setup_reply_master[unfolded tcb_replycap_slot_def] ])
apply (rule dcorres_rhs_noop_below_True[OF dcorres_rhs_noop_below_True])
apply (rule possible_switch_to_dcorres)
apply (rule tcb_sched_action_dcorres)
apply (rule dcorres_set_thread_state_Restart2[unfolded tcb_pending_op_slot_def])
apply wp
apply (simp add:not_idle_thread_def)
apply ((wp|wps)+)[2]
apply (rule_tac P'="(=) s' and invs" in hoare_weaken_pre)
apply (rule hoare_strengthen_post
[where Q'="\<lambda>r. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs"])
apply (simp add:not_idle_thread_def)
apply (wp)
apply (clarsimp simp:invs_def valid_state_def valid_pspace_def
tcb_at_def not_idle_thread_def)+
apply (clarsimp simp:valid_idle_def pred_tcb_at_def obj_at_def)
apply assumption
apply (clarsimp simp:not_idle_thread_def)+
apply (clarsimp dest!:runnable_imply[where obj_id = obj_id])+
apply (clarsimp simp:invs_def valid_state_def)
apply (drule only_idleD[rotated])
apply (fastforce simp:st_tcb_at_def obj_at_def dest!:get_tcb_SomeD)
apply simp
apply (clarsimp simp: runnable_def infer_tcb_pending_op_def
split:Structures_A.thread_state.split_asm)+
apply (frule(1) valid_etcbs_get_tcb_get_etcb)
apply (fastforce simp:opt_cap_tcb not_idle_thread_def)
done
crunch get_thread, getRegister
for inv [wp]: P
(ignore_del: getRegister)
(* Read the registers of another thread. *)
lemma invoke_tcb_corres_read_regs:
"\<lbrakk> t' = tcb_invocation.ReadRegisters obj_id resume data flags;
t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> dc) \<top> (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs)
(Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def)
apply (case_tac "resume")
apply (rule corres_alternate1)
apply clarsimp
apply (subst bind_return [symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split[where r'=dc])
apply (rule suspend_corres, simp)
apply (rule corres_symb_exec_r)
apply (rule dcorres_idempotent_as_user)
apply (rule hoare_mapM_idempotent)
apply wpsimp+
apply (rule corres_alternate2)
apply (rule corres_symb_exec_r)
apply (rule dcorres_idempotent_as_user)
apply (rule hoare_mapM_idempotent)
apply (wp | simp)+
done
(* Write the registers of another thread. *)
lemma invoke_tcb_corres_write_regs:
"\<lbrakk> t' = tcb_invocation.WriteRegisters obj_id resume data flags;
t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def arch_get_sanitise_register_info_def
arch_post_modify_registers_def)
apply (rule corres_symb_exec_r)
apply (rule corres_guard_imp)
apply (rule corres_split[where r'=dc])
apply (rule corrupt_tcb_intent_as_user_corres)
apply (rule corres_dummy_return_l)
apply (rule corres_split[where r'=dc])
apply (clarsimp simp: when_def)
apply (clarsimp simp: dc_def, rule restart_corres [unfolded dc_def])
apply (rule corres_split_noop_rhs[OF corres_trivial])
apply (clarsimp simp: when_def)
apply (rule reschedule_required_dcorres[THEN corres_trivial])
apply simp
apply wp
apply (clarsimp simp: when_def)
apply (wpsimp wp: when_wp)+
apply (wp wp_post_taut | simp add:invs_def valid_state_def | fastforce)+
done
lemma corres_mapM_x_rhs_induct:
"\<lbrakk> corres_underlying sr nf nf' dc P P' g (return ());
\<And>a. corres_underlying sr nf nf' dc P P' g (g' a);
g = do g; g od;
\<lbrace> P \<rbrace> g \<lbrace> \<lambda>_. P \<rbrace>;
\<And>a. \<lbrace> P' \<rbrace> g' a \<lbrace> \<lambda>_. P'\<rbrace> \<rbrakk> \<Longrightarrow>
corres_underlying sr nf nf' dc P P' g (mapM_x g' l)"
apply (induct_tac l)
apply (clarsimp simp: mapM_x_def sequence_x_def dc_def)
apply (clarsimp simp: mapM_x_def sequence_x_def dc_def)
apply (erule ssubst)
apply (rule corres_guard_imp)
apply (rule corres_split)
apply assumption
apply assumption
apply assumption
apply assumption
apply simp
apply simp
done
(*
* Copy registers loop.
*
* What we show here is that any number of individual register
* copys from A to B merely results in a corruption of B's
* registers.
*)
lemma invoke_tcb_corres_copy_regs_loop:
"dcorres dc \<top>
(tcb_at target_id and tcb_at obj_id' and valid_idle and not_idle_thread target_id and not_idle_thread obj_id' and valid_etcbs)
(corrupt_tcb_intent target_id)
(mapM_x
(\<lambda>r. do v \<leftarrow> as_user obj_id' (getRegister r);
as_user target_id (setRegister r v)
od) x)"
apply (clarsimp simp: mapM_x_mapM)
apply (rule corres_guard_imp)
apply (rule corres_dummy_return_l)
apply (rule corres_split[OF Intent_DR.set_registers_corres corres_free_return[where P=\<top> and P'= \<top>]])
apply (wp|simp)+
done
crunch
"Tcb_A.restart", "IpcCancel_A.suspend"
for idle_thread_constant[wp]: "\<lambda>s::'z::state_ext state. P (idle_thread s)"
(wp: dxo_wp_weak)
lemma not_idle_after_restart [wp]:
"\<lbrace>invs and not_idle_thread obj_id' :: det_state \<Rightarrow> bool\<rbrace> Tcb_A.restart obj_id'
\<lbrace>\<lambda>rv. valid_idle \<rbrace>"
including no_pre
supply if_cong[cong]
apply (simp add:Tcb_A.restart_def)
apply wp
apply (simp add:cancel_ipc_def)
apply (wp not_idle_after_blocked_cancel_ipc not_idle_after_reply_cancel_ipc
not_idle_thread_cancel_signal | wpc)+
apply (rule hoare_strengthen_post[where Q'="\<lambda>r. st_tcb_at ((=) r) obj_id'
and not_idle_thread obj_id' and invs"])
apply (wp gts_sp)
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def not_idle_thread_def | rule conjI)+
apply (rule hoare_strengthen_post, rule gts_inv)
apply (clarsimp)
done
lemma not_idle_after_suspend [wp]:
"\<lbrace>invs and not_idle_thread obj_id' and tcb_at obj_id'\<rbrace> IpcCancel_A.suspend obj_id'
\<lbrace>\<lambda>rv. valid_idle \<rbrace>"
apply (rule hoare_strengthen_post)
apply (rule hoare_weaken_pre)
apply (rule suspend_invs)
apply (simp add:not_idle_thread_def invs_def valid_state_def)+
done
crunch "Tcb_A.restart"
for valid_etcbs[wp]: "valid_etcbs"
(* Copy registers from one thread to another. *)
lemma invoke_tcb_corres_copy_regs:
"\<lbrakk> t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e;
t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> dc) \<top>
(invs and tcb_at obj_id' and tcb_at target_id' and Tcb_AI.tcb_inv_wf t' and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs)
(Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def arch_post_modify_registers_def)
apply (rule corres_guard_imp)
apply (rule corres_split[where r'=dc])
apply (rule corres_cases [where R="a"])
apply (clarsimp simp: when_def)
apply (rule corres_alternate1)
apply (rule suspend_corres)
apply (clarsimp simp: when_def dc_def[symmetric])+
apply (rule corres_alternate2)
apply (rule corres_free_return [where P="\<top>" and P'="\<top>"])
apply (rule corres_split[where r'=dc])
apply (rule corres_cases [where R="b"])
apply (clarsimp simp: when_def)
apply (rule corres_alternate1)
apply (rule restart_corres, simp)
apply (rule corres_alternate2)
apply (rule corres_free_return [where P="\<top>" and P'="\<top>"])
apply (rule corres_corrupt_tcb_intent_dupl)
apply (rule corres_split[where r'=dc])
apply (rule corres_cases [where R="c"])
apply (clarsimp simp: when_def)
apply (rule corres_bind_ignore_ret_rhs)
apply (rule corres_corrupt_tcb_intent_dupl)
apply (rule corres_split[where r'=dc])
apply (rule invoke_tcb_corres_copy_regs_loop, simp)
apply (rule corres_symb_exec_r)
apply (simp add:setNextPC_def)
apply (rule Intent_DR.set_register_corres[unfolded dc_def], simp)
apply (wp | clarsimp simp:getRestartPC_def)+
apply (wp mapM_x_wp [where S=UNIV])
apply simp
apply simp
apply (rule dummy_corrupt_tcb_intent_corres)
apply (rule corres_dummy_return_l)
apply (rule corres_split[where r'=dc])
apply (rule corres_cases [where R="d"])
apply (clarsimp simp: when_def)
apply (rule invoke_tcb_corres_copy_regs_loop)
apply (clarsimp simp: when_def)
apply (rule dummy_corrupt_tcb_intent_corres)
apply (rule corres_symb_exec_r)
apply (rule corres_split_noop_rhs[OF corres_trivial])
apply simp
apply (clarsimp simp: when_def)
apply (rule reschedule_required_dcorres[THEN corres_trivial])
apply wpsimp+
apply (wp mapM_x_wp [where S=UNIV])[1]
apply simp
apply (wp wp_post_taut)
apply (clarsimp simp:conj_comms pred_conj_def cong: if_cong)
apply (wpsimp simp: not_idle_thread_def | rule conjI | strengthen invs_cur)+
done
lemma cnode_cap_unique_bits:
"is_cnode_cap cap \<Longrightarrow>
\<lbrace>\<lambda>s. (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s)
\<and> valid_cap cap s \<and> valid_objs s\<rbrace>
CSpaceAcc_A.get_cap (ba, c)
\<lbrace>\<lambda>rv s. (Structures_A.is_cnode_cap rv \<and> obj_refs rv = obj_refs cap) \<longrightarrow> (bits_of rv = bits_of cap)\<rbrace>"
apply (rule hoare_pre)
apply (rule_tac Q'="\<lambda>r s. (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and>
table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s)
\<and> valid_cap cap s \<and> valid_objs s
\<and> valid_objs s \<and> cte_wp_at (\<lambda>x. x = r) (ba,c) s"
in hoare_strengthen_post)
apply (wp get_cap_cte_wp_at)
apply (clarsimp simp:is_cap_simps)
apply (drule_tac x = ba in spec)
apply (drule_tac x = c in spec)
apply (drule(1) cte_wp_at_valid_objs_valid_cap)
apply (clarsimp simp:valid_cap_def obj_at_def is_ep_def is_ntfn_def is_cap_table_def,
clarsimp split:Structures_A.kernel_object.split_asm)+
apply (clarsimp simp:well_formed_cnode_n_def bits_of_def)
apply simp
done
lemma get_cap_ex_cte_cap_wp_to:
"(tcb_cnode_index x)\<in> dom tcb_cap_cases \<Longrightarrow> \<lbrace>\<top>\<rbrace> CSpaceAcc_A.get_cap a'
\<lbrace>\<lambda>rv s. is_thread_cap rv \<and> obj_ref_of rv = obj_id' \<longrightarrow> ex_cte_cap_wp_to (\<lambda>_. True) (obj_id', tcb_cnode_index x) s\<rbrace>"
apply (rule hoare_strengthen_post[OF get_cap_cte_wp_at])
apply (case_tac a')
apply (clarsimp simp:ex_cte_cap_wp_to_def)
apply (rule exI)+
apply (rule cte_wp_at_weakenE)
apply simp
apply (clarsimp simp:is_cap_simps)
done
crunch cap_delete
for idle[wp]: "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps dxo_wp_weak simp: crunch_simps ignore: wrap_ext_bool OR_choiceE)
lemma imp_strengthen:
"R \<and> (P x \<longrightarrow> Q x) \<Longrightarrow> P x \<longrightarrow> (Q x \<and> R) "
by simp
lemma dcorres_corrupt_tcb_intent_ipcbuffer_upd:
"dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs)
(corrupt_tcb_intent y)
(thread_set (tcb_ipc_buffer_update (\<lambda>_. a)) y)"
apply (clarsimp simp:corrupt_tcb_intent_def thread_set_def get_thread_def bind_assoc)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:update_thread_def tcb_at_def)
apply (rule select_pick_corres[where S = UNIV,simplified])
apply (frule(1) valid_etcbs_get_tcb_get_etcb)
apply (rule dcorres_gets_the)
apply (clarsimp simp:opt_object_tcb not_idle_thread_def)
apply (simp add:transform_tcb_def)
apply (rule corres_guard_imp)
apply (rule_tac s' = s'a in dcorres_set_object_tcb)
apply (clarsimp simp:transform_tcb_def)
apply (simp add: get_etcb_def)
apply (clarsimp dest!: get_tcb_SomeD get_etcb_SomeD split:option.splits)+
apply (clarsimp simp: opt_object_tcb not_idle_thread_def dest!:get_tcb_rev get_etcb_rev)
done
lemma arch_same_obj_as_lift:
"\<lbrakk>cap_aligned a;is_arch_cap a;ca = transform_cap a;cb=transform_cap b\<rbrakk>
\<Longrightarrow> cdl_same_arch_obj_as (ca) (cb) = same_object_as a b"
apply (clarsimp simp:is_arch_cap_def split:cap.split_asm)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:cdl_same_arch_obj_as_def)+
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply ((clarsimp simp:cdl_same_arch_obj_as_def)+)[5]
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+
done
lemma thread_set_valid_irq_node:
"(\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t)
\<Longrightarrow>
\<lbrace>valid_irq_node\<rbrace> thread_set f p
\<lbrace>\<lambda>rv s. valid_irq_node s\<rbrace>"
apply (simp add: valid_irq_node_def thread_set_def)
apply wp
apply (simp add: KHeap_A.set_object_def get_object_def)
apply wp+
apply (clarsimp simp: obj_at_def is_cap_table_def dest!: get_tcb_SomeD)
apply (drule_tac x = irq in spec)
apply clarsimp
done
lemma update_ipc_buffer_valid_objs:
"\<lbrace>valid_objs and K(is_aligned a msg_align_bits)\<rbrace>
thread_set (tcb_ipc_buffer_update (\<lambda>_. a)) ptr
\<lbrace>\<lambda>rv s. valid_objs s \<rbrace>"
apply (wp thread_set_valid_objs'')
apply (clarsimp simp:valid_tcb_def)
apply (intro conjI allI)
apply (clarsimp simp:tcb_cap_cases_def)
apply (auto simp: valid_ipc_buffer_cap_def split: cap.splits arch_cap.splits bool.splits)
done
lemma dcorres_tcb_empty_slot:
"(thread,idx) = (transform_cslot_ptr slot)
\<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True)
(cte_wp_at (\<lambda>_. True) slot and invs and emptyable slot and not_idle_thread (fst slot) and valid_pdpt_objs and valid_etcbs)
(tcb_empty_thread_slot thread idx) (cap_delete slot)"
apply (simp add:liftE_bindE tcb_empty_thread_slot_def)
apply (simp add:opt_cap_def gets_the_def assert_opt_def gets_def bind_assoc split_def)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp add:cte_at_into_opt_cap)
apply (erule impE)
apply (clarsimp simp: not_idle_thread_def dest!:invs_valid_idle)
apply (simp add:opt_cap_def whenE_def split_def)
apply (intro conjI impI)
apply (case_tac slot,clarsimp)
apply (rule corres_guard_imp)
apply (rule delete_cap_corres')
apply simp
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (simp add:cap_delete_def)
apply (subst rec_del_simps_ext)
apply (subst rec_del_simps_ext)
apply (clarsimp simp:bindE_assoc)
apply (subst liftE_bindE)
apply (rule corres_guard_imp[OF corres_symb_exec_r])
apply (rule_tac F = "x = cap.NullCap" in corres_gen_asm2)
apply (simp add:bindE_assoc when_def)
apply (simp add:IpcCancel_A.empty_slot_def returnOk_liftE)
apply (rule corres_symb_exec_r)
apply (rule_tac F = "cap = cap.NullCap" in corres_gen_asm2)
apply (rule corres_trivial)
apply simp
apply (simp | wp get_cap_wp)+
apply (clarsimp simp:cte_wp_at_caps_of_state)
done
lemma dcorres_idempotent_as_user_strong:
assumes prem: "\<And>tcb ms ref etcb P.
\<lbrace> \<lambda>cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch:=arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>
x
\<lbrace> \<lambda>_ cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch:=arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>"
shows "dcorres dc \<top> (tcb_at u) (return q) (as_user u x)"
supply option.case_cong[cong] if_cong[cong]
apply (clarsimp simp: as_user_def)
apply (clarsimp simp: corres_underlying_def bind_def split_def set_object_def get_object_def
return_def get_def put_def get_tcb_def gets_the_def gets_def assert_opt_def
tcb_at_def select_f_def valid_def
split: option.split Structures_A.kernel_object.split)
apply (clarsimp simp: transform_def transform_current_thread_def transform_objects_def restrict_map_def)
apply (rule ext)
apply (clarsimp simp: map_add_def split:option.splits)
apply (drule use_valid[OF _ prem])
prefer 2
apply force
apply simp
done
lemma TPIDRURW_notin_msg_registers[simp]:
"TPIDRURW \<notin> set msg_registers"
apply (auto simp: msgRegisters_def frameRegisters_def gpRegisters_def
syscallMessage_def exceptionMessage_def msg_registers_def)
apply (rule ccontr)
apply clarsimp
apply (simp_all add: upto_enum_red image_def)
apply (auto simp add: toEnum_eq_to_fromEnum_eq fromEnum_def enum_register maxBound_def
dest!: toEnum_eq_to_fromEnum_eq[THEN iffD1,rotated,OF sym])
done
lemma transform_full_intent_update_tpidrurw[simp]:
"transform_full_intent ms ref (tcb\<lparr>tcb_arch := arch_tcb_set_registers (s(TPIDRURW := a)) (tcb_arch tcb)\<rparr>)
= transform_full_intent ms ref (tcb\<lparr>tcb_arch := arch_tcb_set_registers s (tcb_arch tcb)\<rparr>)"
apply (clarsimp simp: transform_full_intent_def cap_register_def ARM.capRegister_def
arch_tcb_set_registers_def arch_tcb_context_get_def Let_def)
by (fastforce simp: get_tcb_message_info_def msg_info_register_def ARM.msgInfoRegister_def
get_tcb_mrs_def get_ipc_buffer_words_def Suc_le_eq Let_def
arch_tcb_context_get_def)
lemma as_user_valid_irq_node[wp]:
"\<lbrace>valid_irq_node\<rbrace>
as_user y (set_register a v)
\<lbrace>\<lambda>rv. valid_irq_node\<rbrace>"
apply (simp add: valid_irq_node_def cap_table_at_typ)
apply (rule hoare_pre)
apply (wp hoare_vcg_all_lift | wps )+
apply auto
done
lemma set_register_TPIDRURW_tcb_abstract_inv[wp]:
"\<lbrace>\<lambda>cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>
setRegister TPIDRURW a
\<lbrace>\<lambda>_ cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>"
supply transform_full_intent_update_tpidrurw[simplified arch_tcb_set_registers_def, simp]
apply (simp add: setRegister_def simpler_modify_def valid_def arch_tcb_context_set_def
transform_tcb_def)
done
lemma dcorres_tcb_update_ipc_buffer: