-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathIntent_DR.thy
2200 lines (2005 loc) · 96.8 KB
/
Intent_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 Intent_DR
imports Corres_D
begin
context begin interpretation Arch . (*FIXME: arch-split*)
definition not_idle_thread:: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"not_idle_thread x \<equiv> \<lambda>s. x \<noteq> idle_thread s"
(*Some trivial lemmas rule out irq_node and idle_thread*)
lemma ep_not_idle:
"\<lbrakk>valid_idle s;obj_at is_ep epptr s\<rbrakk> \<Longrightarrow> not_idle_thread epptr s"
by (clarsimp simp:valid_idle_def obj_at_def is_cap_table_def pred_tcb_at_def is_ep_def not_idle_thread_def)
lemma ntfn_not_idle:
"\<lbrakk>valid_idle s;obj_at is_ntfn epptr s\<rbrakk> \<Longrightarrow> not_idle_thread epptr s"
by (clarsimp simp:valid_idle_def obj_at_def is_cap_table_def pred_tcb_at_def is_ntfn_def not_idle_thread_def)
lemma cte_wp_at_zombie_not_idle:
"\<lbrakk>cte_wp_at ((=) (cap.Zombie ptr' zbits n)) ptr s; invs s\<rbrakk> \<Longrightarrow> not_idle_thread (fst ptr) s"
"\<lbrakk>cte_wp_at ((=) (cap.Zombie ptr' zbits n)) ptr s; invs s\<rbrakk> \<Longrightarrow> not_idle_thread ptr' s"
by (auto dest!: zombie_cap_two_nonidles simp: cte_wp_at_caps_of_state not_idle_thread_def)
lemmas tcb_slots = Types_D.tcb_caller_slot_def Types_D.tcb_cspace_slot_def Types_D.tcb_ipcbuffer_slot_def
Types_D.tcb_pending_op_slot_def Types_D.tcb_replycap_slot_def Types_D.tcb_vspace_slot_def Types_D.tcb_boundntfn_slot_def
(* FIXME: MOVE *)
lemma tcb_cap_casesE:
assumes cs: "tcb_cap_cases p = Some (gf, sf, restr)"
and rules: "\<lbrakk> p = tcb_cnode_index 0; gf = tcb_ctable; sf = tcb_ctable_update; restr = (\<lambda>_ _. \<top>) \<rbrakk> \<Longrightarrow> R"
"\<lbrakk> p = tcb_cnode_index 1; gf = tcb_vtable; sf = tcb_vtable_update;
restr = (\<lambda>_ _. is_valid_vtable_root or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
"\<lbrakk> p = tcb_cnode_index 2; gf = tcb_reply; sf = tcb_reply_update;
restr = (\<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))) \<rbrakk> \<Longrightarrow> R"
"\<lbrakk> p = tcb_cnode_index 3; gf = tcb_caller; sf = tcb_caller_update;
restr = (\<lambda>_ st. case st of
Structures_A.BlockedOnReceive e data \<Rightarrow>
((=) cap.NullCap)
| _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
"\<lbrakk> p = tcb_cnode_index 4; gf = tcb_ipcframe; sf = tcb_ipcframe_update; restr =
(\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
shows "R"
using cs
unfolding tcb_cap_cases_def
apply (simp split: if_split_asm del: One_nat_def)
apply (erule rules, fastforce+)+
done
lemma tcb_cnode_index_def2:
"n < 8 \<Longrightarrow> tcb_cnode_index n = bin_to_bl 3 (int n)"
unfolding tcb_cnode_index_def to_bl_def
by (simp add: uint_nat unat_of_nat)
lemma bl_to_bin_tcb_cnode_index:
"n < 8 \<Longrightarrow> nat (bl_to_bin (tcb_cnode_index n)) = n"
unfolding tcb_cnode_index_def
by (simp add: unat_of_nat)
(* LIFT LEMMAS:
Lift the property from abstract spec to capdl model
*)
lemma transform_objects_kheap:
"\<lbrakk> kheap s p = Some ko; p \<noteq> idle_thread s \<rbrakk>
\<Longrightarrow> transform_objects s p = Some (transform_object (machine_state s) p (ekheap s p) ko)"
unfolding transform_objects_def
by (simp)
lemma transform_objects_tcb:
"\<lbrakk> get_tcb ptr s = Some tcb; get_etcb ptr s = Some etcb; ptr \<noteq> idle_thread s\<rbrakk>
\<Longrightarrow> transform_objects s ptr = Some (transform_tcb (machine_state s) ptr tcb etcb)"
by (clarsimp dest!: get_tcb_SomeD simp: get_etcb_def transform_objects_def)
lemma opt_object_tcb:
"\<lbrakk> get_tcb ptr s = Some tcb; get_etcb ptr s = Some etcb; ptr \<noteq> idle_thread s \<rbrakk> \<Longrightarrow>
cdl_objects (transform s) ptr = Some (transform_tcb (machine_state s) ptr tcb etcb)"
by (clarsimp simp: transform_def transform_objects_tcb dest!: get_tcb_SomeD)
abbreviation
"tcb_abstract_slots \<equiv> {tcb_caller_slot, tcb_cspace_slot, tcb_ipcbuffer_slot, tcb_replycap_slot, tcb_vspace_slot}"
lemma tcb_cap_cases_slot_simps[simp]:
"tcb_cap_cases (tcb_cnode_index tcb_cspace_slot) = Some (tcb_ctable, tcb_ctable_update, (\<lambda>_ _. \<top>))"
"tcb_cap_cases (tcb_cnode_index tcb_vspace_slot) =
Some (tcb_vtable, tcb_vtable_update, (\<lambda>_ _. is_valid_vtable_root or ((=) cap.NullCap)))"
"tcb_cap_cases (tcb_cnode_index tcb_replycap_slot) =
Some (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))))"
"tcb_cap_cases (tcb_cnode_index tcb_caller_slot) =
Some (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)))"
"tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot) =
Some (tcb_ipcframe, tcb_ipcframe_update, (\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap)))"
by (simp add: tcb_slots)+
lemma opt_cap_tcb:
"\<lbrakk> get_tcb y s = Some tcb; (\<exists>etcb. get_etcb y s = Some etcb); y \<noteq> idle_thread s \<rbrakk> \<Longrightarrow>
opt_cap (y, sl) (transform s) =
(if sl \<in> tcb_abstract_slots then (option_map (\<lambda>(getF, _, _). transform_cap (getF tcb)) (tcb_cap_cases (tcb_cnode_index sl)))
else (if sl = tcb_pending_op_slot then (Some (infer_tcb_pending_op y (tcb_state tcb)))
else (if sl = tcb_boundntfn_slot then (Some (infer_tcb_bound_notification (tcb_bound_notification tcb))) else None)))"
by (fastforce simp add: opt_cap_def KHeap_D.slots_of_def opt_object_tcb object_slots_def transform_tcb_def tcb_slots)
lemma cdl_objects_cnode:
"\<lbrakk> kheap s' y = Some (CNode sz obj'); valid_idle s' ; sz \<noteq> 0\<rbrakk>
\<Longrightarrow> cdl_objects (transform s') y =
Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>)"
apply (subgoal_tac "y \<noteq> idle_thread s'")
apply (auto simp:obj_at_def is_cap_table_def valid_idle_def pred_tcb_at_def
transform_def transform_objects_def
split:nat.split)
done
lemma cdl_objects_irq_node:
"\<lbrakk> kheap s' y = Some (CNode 0 obj'); valid_idle s' \<rbrakk>
\<Longrightarrow> cdl_objects (transform s') y =
Some (cdl_object.IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>)"
apply (subgoal_tac "y \<noteq> idle_thread s'")
apply (auto simp:obj_at_def is_cap_table_def valid_idle_def pred_tcb_at_def
transform_def transform_objects_def)
done
lemma transform_objects_cnode:
"\<lbrakk> kheap s' y = Some (CNode sz obj'); valid_idle s'; sz \<noteq> 0\<rbrakk> \<Longrightarrow> transform_objects s' y =
Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>)"
apply (subgoal_tac "y \<noteq> idle_thread s'")
apply (simp add: transform_objects_def)
apply (clarsimp simp add: valid_idle_def obj_at_def pred_tcb_at_def split:nat.split)+
done
lemma transform_objects_irq_node:
"\<lbrakk> kheap s' y = Some (CNode 0 obj'); valid_idle s'\<rbrakk> \<Longrightarrow> transform_objects s' y =
Some (cdl_object.IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>)"
apply (subgoal_tac "y \<noteq> idle_thread s'")
apply (simp add: transform_objects_def)
apply (clarsimp simp add: valid_idle_def obj_at_def pred_tcb_at_def split:nat.split)+
done
lemmas lift_simp =
transform_objects_tcb transform_objects_cnode transform_objects_kheap cdl_objects_cnode
opt_cap_tcb opt_object_tcb
lemma transform_objects_update_other:
"\<lbrakk> kh ptr = Some ko; caps_of_object ko = caps_of_object ko'; a_type ko = a_type ko'; ref \<noteq> ptr \<rbrakk>
\<Longrightarrow> transform_objects (update_kheap (kh(ptr \<mapsto> ko')) s) ref = transform_objects (update_kheap kh s) ref"
unfolding transform_objects_def
by (cases ref, simp_all add: restrict_map_def caps_of_state_update_same_caps
cap_installed_at_irq_def map_add_def)
lemma caps_of_object_update_state [simp]:
"(\<lambda>n. map_option (\<lambda>(f, _). f (tcb_state_update stf tcb)) (tcb_cap_cases n)) =
(\<lambda>n. map_option (\<lambda>(f, _). f tcb) (tcb_cap_cases n))"
apply (rule ext)
apply (simp add: tcb_cap_cases_def split: if_split)
done
lemma caps_of_object_update_boundntfn [simp]:
"(\<lambda>n. map_option (\<lambda>(f, _). f (tcb_bound_notification_update stf tcb)) (tcb_cap_cases n)) =
(\<lambda>n. map_option (\<lambda>(f, _). f tcb) (tcb_cap_cases n))"
apply (rule ext)
apply (simp add: tcb_cap_cases_def split: if_split)
done
lemma caps_of_object_update_context [simp]:
"(\<lambda>n. map_option (\<lambda>(f, _). f (tcb_arch_update (tcb_context_update stf) tcb)) (tcb_cap_cases n)) =
(\<lambda>n. map_option (\<lambda>(f, _). f tcb) (tcb_cap_cases n))"
apply (rule ext)
apply (simp add: tcb_cap_cases_def split: if_split)
done
definition
generates_pending :: "Structures_A.thread_state \<Rightarrow> bool"
where
"generates_pending st \<equiv> case st of
Structures_A.BlockedOnReceive ptr payload \<Rightarrow> True
| Structures_A.BlockedOnSend ptr payload \<Rightarrow> True
| Structures_A.BlockedOnReply \<Rightarrow> True
| Structures_A.BlockedOnNotification ptr \<Rightarrow> True
| Structures_A.Restart \<Rightarrow> True
| Structures_A.Running \<Rightarrow> True
| _ \<Rightarrow> False"
lemmas generates_pending_simps [simp] = generates_pending_def [split_simps Structures_A.thread_state.split]
lemmas infer_tcb_pending_op_simps [simp] = infer_tcb_pending_op_def [split_simps Structures_A.thread_state.split]
(* Is actually iff *)
lemma not_generates_pending_is_null:
"\<not> generates_pending st \<Longrightarrow> (infer_tcb_pending_op ptr st = Types_D.NullCap)"
unfolding generates_pending_def infer_tcb_pending_op_def
by (simp split: Structures_A.thread_state.splits)
lemma transform_tcb_upd_state_no_pending:
"\<lbrakk> \<not> generates_pending (tcb_state tcb); \<not> generates_pending (f (tcb_state tcb)) \<rbrakk>
\<Longrightarrow> transform_tcb ms ptr (tcb_state_update f tcb) etcb = transform_tcb ms ptr tcb etcb"
unfolding transform_tcb_def
by (simp add: not_generates_pending_is_null cong: transform_full_intent_cong)
lemmas transform_objects_tcb_state =
transform_objects_update_kheap_same_caps transform_objects_update_same
transform_tcb_upd_state_no_pending
lemma transform_objects_dummy_set_original_cap [simp]:
"transform_objects (b\<lparr>is_original_cap := x\<rparr>) = transform_objects b"
by (clarsimp simp: cap_installed_at_irq_def transform_objects_def)
lemma transform_objects_dummy_update_cdt [simp]:
"transform_objects (b\<lparr>cdt := x\<rparr>) = transform_objects b"
by (clarsimp simp: cap_installed_at_irq_def transform_objects_def)
lemma update_tcb_cxt_eq_dupdate_tcb_intent:
"\<lbrakk>
cdl_objects (transform b) y = Some (Tcb t);
kheap b y = Some (TCB obj);
\<exists>etcb'. ekheap b y = Some etcb';
obj' = tcb_arch_update (arch_tcb_context_set cxt) obj;
not_idle_thread y b;
intent = transform_full_intent (machine_state (update_kheap ((kheap b)(y\<mapsto>(TCB obj'))) b)) y obj'
\<rbrakk>
\<Longrightarrow> dupdate_cdl_object y (Tcb (dupdate_tcb_intent intent t)) (transform b)
= transform (update_kheap ((kheap b)(y\<mapsto> (TCB obj'))) b)"
apply (clarsimp simp:transform_def transform_current_thread_def
not_idle_thread_def transform_objects_def)
apply (rule ext, clarsimp)
apply (rule conjI)
apply (clarsimp simp:restrict_map_Some_iff)
apply (clarsimp simp:transform_tcb_def restrict_map_def map_add_def)
apply (clarsimp simp:transform_tcb_def restrict_map_def map_add_def)
done
lemma duplicate_corrupt_tcb_intent:
"do corrupt_tcb_intent epptr; corrupt_tcb_intent epptr od = corrupt_tcb_intent epptr"
apply (clarsimp simp:bind_def)
apply (rule ext)
apply (clarsimp simp:split_def)
apply (rule prod_eqI)
apply (rule set_eqI)
apply clarsimp
apply (auto simp:corrupt_tcb_intent_def update_thread_def select_def gets_the_def
return_def fail_def gets_def get_def assert_opt_def bind_def
put_def modify_def KHeap_D.set_object_def split_def
split:option.splits cdl_object.splits)[1]
apply clarsimp
apply (rule iffI)
by (auto simp: corrupt_tcb_intent_def update_thread_def select_def gets_the_def
return_def fail_def gets_def get_def assert_opt_def bind_def
put_def modify_def KHeap_D.set_object_def split_def
split: option.splits cdl_object.splits)
(* Corrupting a register several times is the same as corrupting it once. *)
lemma corres_corrupt_tcb_intent_dupl:
"\<lbrakk> dcorres dc P P' (do corrupt_tcb_intent x; corrupt_tcb_intent x od) g \<rbrakk> \<Longrightarrow>
dcorres dc P P' (corrupt_tcb_intent x) g"
by (subst duplicate_corrupt_tcb_intent[symmetric], simp)
(*
* Doing nothing at the abstract level corresponds to corrupting a TCB intent.
* (In particular, it is the "null" corruption.)
*)
lemma corres_corrupt_tcb_intent_return:
"dcorres dc \<top> (tcb_at ptr and not_idle_thread ptr and valid_etcbs) (corrupt_tcb_intent ptr) (return x)"
supply option.case_cong[cong]
apply (clarsimp simp: corres_underlying_def return_def corrupt_tcb_intent_def update_thread_def
select_def gets_the_def fail_def gets_def get_def assert_opt_def bind_def
put_def modify_def KHeap_D.set_object_def)
apply (clarsimp split: option.splits
simp: transform_def tcb_at_def transform_objects_def not_idle_thread_def
dest!: get_tcb_SomeD)
apply (drule(1) valid_etcbs_tcb_etcb)
apply (clarsimp)
apply (force simp: transform_def transform_tcb_def transform_objects_def not_idle_thread_def
tcb_at_def obj_at_def
split: cdl_object.splits)
done
lemma dcorres_set_object_tcb:
"\<lbrakk> \<exists>etcb'. (transform_tcb (machine_state s') p' tcb' etcb' = Tcb tcb \<and> ekheap s' p' = Some etcb');
p' \<noteq> idle_thread s'; kheap s' p' \<noteq> None; ekheap s' p' \<noteq> None \<rbrakk> \<Longrightarrow>
dcorres dc ((=) (transform s')) ((=) s')
(KHeap_D.set_object p' (Tcb tcb ))
(KHeap_A.set_object p' (TCB tcb'))"
apply (clarsimp simp: corres_underlying_def set_object_def get_object_def in_monad)
apply (clarsimp simp: KHeap_D.set_object_def simpler_modify_def)
apply (clarsimp simp: transform_def transform_current_thread_def)
apply (clarsimp simp: transform_objects_def)
apply (rule ext)
apply clarsimp
apply (clarsimp simp: option_map_def restrict_map_def map_add_def)
done
lemma set_cxt_none_det_intent_corres':
"\<lbrakk>kheap s' y = Some (TCB obj'); ekheap s' y \<noteq> None; valid_idle s';not_idle_thread y s'\<rbrakk>
\<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s')
(corrupt_tcb_intent y)
(KHeap_A.set_object y (TCB (tcb_arch_update f obj')))"
apply (clarsimp simp:bind_assoc corrupt_tcb_intent_def get_thread_def gets_def gets_the_def)
apply (rule corres_guard_imp)
apply (rule_tac P="(=)(transform s')" and Q="(=) s'"
and x="transform_full_intent (machine_state (update_kheap ((kheap s')(y\<mapsto>(TCB (tcb_arch_update f obj')))) s'))
y (tcb_arch_update f obj')"
in select_pick_corres)
apply (clarsimp simp:update_thread_def get_object_def
gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (subgoal_tac "\<exists>t f. cdl_objects (transform s') y = Some (Tcb t)")
apply (clarsimp simp:assert_opt_def)
apply (rule dcorres_set_object_tcb)
apply (clarsimp simp:transform_tcb_def
transform_def transform_objects_def not_idle_thread_def)
apply (clarsimp simp:not_idle_thread_def)
apply simp
apply simp
apply (clarsimp simp:transform_def not_idle_thread_def
transform_objects_def transform_tcb_def)
apply clarsimp
apply clarsimp
done
lemma set_cxt_none_det_intent_corres:
"\<lbrakk>kheap s' y = Some (TCB obj'); ekheap s' y \<noteq> None; valid_idle s';not_idle_thread y s'\<rbrakk>
\<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s')
(corrupt_tcb_intent y)
(KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj')))"
by (rule set_cxt_none_det_intent_corres')
lemma set_message_info_corres:
"dcorres dc \<top> (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y)
(set_message_info y m)"
apply (clarsimp simp:set_message_info_def)
apply (clarsimp simp:as_user_def setRegister_def)
apply (rule dcorres_absorb_gets_the)
apply (clarsimp simp:get_tcb_def split:option.splits Structures_A.kernel_object.splits)
apply (subst modify_def[unfolded bind_def]|clarsimp simp:get_def put_def)+
apply (frule_tac ptr=y and tcb=obj' in valid_etcbs_tcb_etcb, clarsimp, clarsimp)
apply (clarsimp simp:select_f_def bind_def arch_tcb_update_aux3)
apply (rule corres_guard_imp)
apply (erule set_cxt_none_det_intent_corres)
apply (clarsimp simp: valid_def get_tcb_def lift_simp not_idle_thread_def transform_tcb_def
split: option.splits Structures_A.kernel_object.splits)+
done
lemma corrupt_tcb_intent_as_user_corres:
"dcorres dc \<top> (valid_idle and not_idle_thread y and valid_etcbs)
(corrupt_tcb_intent y) (as_user y t)"
apply (clarsimp simp:as_user_def)
apply (rule dcorres_absorb_gets_the)
apply (clarsimp simp:get_tcb_def arch_tcb_update_aux3
split:option.splits Structures_A.kernel_object.splits)
apply (rule corres_symb_exec_r)
apply clarsimp
apply (rule corres_dummy_return_l)
apply (rule corres_underlying_split)
apply (drule(1) valid_etcbs_tcb_etcb)
apply (rule set_cxt_none_det_intent_corres; simp)
apply (rule corres_return_trivial)
apply wpsimp+
done
lemmas set_register_corres = corrupt_tcb_intent_as_user_corres
lemma dummy_corrupt_tcb_intent_corres:
"dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs)
(corrupt_tcb_intent y) (return a)"
apply (simp add:corrupt_tcb_intent_def not_idle_thread_def)
apply (rule dcorres_expand_pfx, clarsimp)
apply (clarsimp simp:tcb_at_def)
apply (drule(1) valid_etcbs_get_tcb_get_etcb, clarsimp)
apply (rule corres_guard_imp)
apply (rule_tac P="(=)(transform s')" and Q="(=) s'" and
x="transform_full_intent (machine_state s') y tcb" in select_pick_corres)
apply (clarsimp simp:update_thread_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def)
apply (clarsimp simp:KHeap_D.set_object_def get_def put_def modify_def assert_def bind_def return_def)
apply (subst corres_singleton)
apply (clarsimp simp:dc_def)
apply (clarsimp simp:transform_def)
apply (rule ext)
apply (clarsimp simp: restrict_map_Some_iff transform_objects_def
split: option.splits dest!:get_tcb_SomeD get_etcb_SomeD)
apply (clarsimp simp: transform_tcb_def)
apply (clarsimp simp:transform_def)+
done
lemma neq_Nil_conv':
"(a \<noteq> []) = (\<exists>h x. a = h@[x])"
by (auto | drule append_butlast_last_id)+
lemma not_idle_thread_as_usr[wp]:
"\<lbrace>not_idle_thread y\<rbrace> as_user p q \<lbrace>\<lambda>rv. not_idle_thread y\<rbrace>"
by (simp add:not_idle_thread_def,wp)
lemma set_registers_corres:
"dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs)
(corrupt_tcb_intent y)
(mapM (%r. do v \<leftarrow> as_user thread (getRegister r);
as_user y (setRegister r v)
od) (x)
)"
apply (induct_tac "x")
apply (clarsimp simp:bind_assoc mapM_def sequence_def)
apply (rule corres_guard_imp)
apply (rule dummy_corrupt_tcb_intent_corres[unfolded dc_def])
apply simp+
apply (clarsimp simp:mapM_def)
apply (subst duplicate_corrupt_tcb_intent[symmetric])
apply (clarsimp simp:sequence_def)
apply (rule_tac Q'="%r. tcb_at y and valid_idle and not_idle_thread y and valid_etcbs"
in corres_split_forwards' [where Q="%r. \<top>"])
apply (rule corres_symb_exec_r)
apply (rule set_register_corres)
apply (wp|simp)+
apply (simp add:bind_assoc dc_def[symmetric])
apply (rule corres_dummy_return_l)
apply (rule corres_split_forwards' [where r'="dc" and Q="%x. \<top>" and Q'="%x. \<top>"])
apply (rule corres_guard_imp)
apply simp+
done
lemma set_mrs_corres_no_recv_buffer:
"dcorres dc \<top> (valid_idle and not_idle_thread y and valid_etcbs)
(corrupt_tcb_intent y) (set_mrs y None msg)"
unfolding set_mrs_def
apply (subst arch_tcb_update_aux3)
apply simp
apply (rule dcorres_absorb_gets_the, clarsimp)
apply (drule(1) valid_etcbs_get_tcb_get_etcb)
apply (rule corres_dummy_return_l)
apply (rule corres_split_forwards' [where Q'="%x. \<top>" and Q="%x. \<top>"])
apply (rule set_cxt_none_det_intent_corres')
apply (simp add:get_tcb_def get_etcb_def
split:option.splits Structures_A.kernel_object.splits
| wp)+
done
lemma corrupt_intents_dup: "corrupt_intents f bufp (corrupt_intents g bufp s) = corrupt_intents f bufp s"
apply (clarsimp simp:corrupt_intents_def)
apply (cases s)
apply clarsimp
apply (rule ext)
apply (case_tac "cdl_objects x")
apply (clarsimp simp:map_add_def)+
apply (clarsimp simp: tcb_ipcframe_id_def split:cdl_object.splits)
done
lemma corrupt_frame_duplicate: "(do _ \<leftarrow> corrupt_frame bufp; corrupt_frame bufp od) = (corrupt_frame bufp)"
apply (rule ext)
apply (clarsimp simp:corrupt_frame_def simpler_modify_def bind_assoc)
apply (clarsimp simp:bind_def select_def)
apply (force simp: corrupt_intents_dup)
done
lemma dcorres_dummy_corrupt_frame: "dcorres dc \<top> valid_etcbs
(corrupt_frame buf) (return a)"
apply (simp add:corrupt_frame_def)
apply (rule dcorres_expand_pfx)
apply (rule corres_guard_imp)
apply (rule_tac P="(=)(transform s')" and Q="(=) s'"
and x = "\<lambda>x. transform_full_intent (machine_state s') x (the (get_tcb x s'))" in select_pick_corres)
apply (clarsimp simp:get_def put_def modify_def assert_def bind_def return_def)
apply (subst corres_singleton)
apply (clarsimp simp:corrupt_intents_def Let_def transform_def transform_objects_def)
apply (rule ext)
apply (clarsimp split:option.splits simp:restrict_map_def map_add_def)
apply (clarsimp simp:map_add_def split:option.splits cdl_object.split_asm if_splits)
apply (clarsimp simp:transform_object_def split:Structures_A.kernel_object.splits arch_kernel_obj.splits nat.splits)
apply (drule(1) valid_etcbs_tcb_etcb)
apply (clarsimp simp:get_tcb_rev get_etcb_rev transform_tcb_def)
apply (clarsimp split:option.splits simp:map_add_def)+
done
definition empty_when_fail :: "('s,'a) nondet_monad \<Rightarrow> bool"
where "empty_when_fail m \<equiv> \<forall>s. snd (m s)\<longrightarrow> fst (m s) = {}"
lemma empty_when_fail_return:
"empty_when_fail (return x)"
by (clarsimp simp:return_def empty_when_fail_def)
lemma wp_no_fail_spec:
"\<lbrakk>empty_when_fail f ; no_fail ((=) s) f \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow>\<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>"
apply (case_tac "no_fail ((=) s) f")
apply simp
apply clarsimp
apply (simp add:no_fail_def valid_def empty_when_fail_def)
done
definition det_spec :: "('s \<Rightarrow> bool) \<Rightarrow> ('s\<Rightarrow>('b\<times>'s) set\<times> bool) \<Rightarrow> bool"
where "det_spec P f \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>r. f s = ({r},False))"
definition weak_det_spec :: "('s \<Rightarrow> bool) \<Rightarrow> ('s\<Rightarrow>('b\<times>'s) set\<times> bool) \<Rightarrow> bool"
where "weak_det_spec P f \<equiv> no_fail P f \<longrightarrow> det_spec P f"
lemma empty_when_fail_compose:
assumes Q:"\<And>r. empty_when_fail (b r)"
assumes P:"empty_when_fail a"
shows "(\<And>P. weak_det_spec P a) \<Longrightarrow> empty_when_fail (a>>=b)"
apply (clarsimp simp:empty_when_fail_def)
apply (case_tac "snd (a s)")
apply (clarsimp simp:bind_def)
using P
apply (clarsimp simp:empty_when_fail_def)
apply (clarsimp simp:bind_def)
apply (clarsimp simp:weak_det_spec_def no_fail_def)
apply (drule_tac x = "(=) s" in meta_spec)
apply (clarsimp simp:det_spec_def)
using Q
apply (simp add: empty_when_fail_def)
done
(*
The following lemma allows use to talking about the return value of a weak_det_spec function in wp
*)
lemma weak_det_spec_ret:
assumes no_fail_det: "weak_det_spec ((=) s) f"
assumes op_eq: "g s = f s"
shows "\<lbrakk> x = the (evalMonad g s); empty_when_fail f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r s. r = x\<rbrace>"
apply (rule wp_no_fail_spec)
apply clarsimp+
apply (clarsimp simp:op_eq evalMonad_def weak_det_spec_def empty_when_fail_def)+
apply (drule_tac x = s in spec)
apply (clarsimp simp:|rule conjI)+
apply (clarsimp simp:valid_def)
apply (clarsimp)
using no_fail_det[unfolded weak_det_spec_def]
apply (clarsimp simp:det_spec_def valid_def)
done
lemma wp_spec:
assumes "P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>"
shows "\<lbrace>(=) s and P\<rbrace> f \<lbrace>Q\<rbrace>"
using assms
by (clarsimp simp:valid_def)
lemma det_compose:
"\<lbrakk>det_spec P a;\<And>r. det_spec (Q r) (b r); \<lbrace>P\<rbrace>a\<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow> det_spec P (a>>=b)"
by (fastforce simp: det_spec_def bind_def valid_def)
lemma no_fail_compose_imp:
"\<lbrakk>no_fail P (a>>= b)\<rbrakk> \<Longrightarrow> no_fail P a \<and> (\<exists>Q. (\<lbrace>P\<rbrace>a\<lbrace>Q\<rbrace> \<and> (\<forall>r. no_fail (Q r) (b r))))"
apply (clarsimp simp: bind_def no_fail_def)
apply (rule_tac x = "\<lambda>rv s. \<exists>s'. P s'\<and> (rv,s) \<in> fst (a s')" in exI)
apply (auto simp:valid_def)
done
lemma mapM_load_word_offs_do_machine_op:
"mapM (load_word_offs ptr) list
= do_machine_op (mapM loadWord (map (\<lambda>offs. ptr + of_nat (offs * word_size)) list))"
apply (subst submonad_mapM[OF submonad_do_machine_op submonad_do_machine_op])
apply (simp add: loadWord_def empty_fail_cond)
apply (simp add: load_word_offs_def[abs_def] mapM_map_simp o_def)
done
lemma det_spec_return:
"det_spec P (return x)"
by (clarsimp simp:return_def det_spec_def)
lemma det_spec_get:
"det_spec P (get)"
by (clarsimp simp:get_def det_spec_def)
lemma det_spec_put:
"det_spec P (put t)"
by (clarsimp simp:put_def det_spec_def)
lemma det_spec_modify:
"det_spec P (modify f)"
by (clarsimp simp:simpler_modify_def det_spec_def)
lemma det_spec_gets:
"det_spec P (gets f)"
apply (clarsimp simp:gets_def)
apply (rule det_compose)
apply (rule det_spec_get)
apply (rule det_spec_return)
apply (fastforce simp:get_def valid_def)
done
lemma det_spec_select_f:
"\<lbrakk>P a; det_spec P f\<rbrakk> \<Longrightarrow> det_spec Q (select_f (f a))"
by (fastforce simp: select_f_def det_spec_def)
lemma det_imply_weak_det:
"det_spec P a \<Longrightarrow> weak_det_spec P a"
by (simp add:weak_det_spec_def)
lemma weak_det_specD:
"\<lbrakk>weak_det_spec P a;no_fail P a\<rbrakk> \<Longrightarrow> det_spec P a"
by (clarsimp simp:weak_det_spec_def)
lemma weak_det_spec_mapM:
assumes single:
"\<And>r P. weak_det_spec P (g r)"
shows
"weak_det_spec Q (mapM g ls)"
proof (induct ls arbitrary:Q)
case Nil
show ?case
apply (clarsimp simp:mapM_def sequence_def det_spec_return)
apply (rule det_imply_weak_det[OF det_spec_return])
done
next
case (Cons x xs)
show ?case
using Cons.hyps
apply (clarsimp simp:mapM_Cons weak_det_spec_def)
apply (drule no_fail_compose_imp)
apply clarsimp
apply (rule det_compose)
apply (rule weak_det_specD)
apply (simp add: assms)+
apply (drule_tac x = r in spec)
apply (drule meta_spec)
apply (drule no_fail_compose_imp)
apply clarsimp
apply (rule det_compose)
apply fastforce
apply (rule det_spec_return)
apply simp
apply simp
done
qed
lemma empty_when_fail_mapM:
"(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l))
\<Longrightarrow> empty_when_fail (mapM x ls)"
proof (induct ls)
case Nil
show ?case
by (clarsimp simp:mapM_def sequence_def empty_when_fail_return)
next
case (Cons x xs)
show ?case
apply (clarsimp simp:mapM_Cons)
apply (rule empty_when_fail_compose)+
apply (simp add: empty_when_fail_return)
apply (rule Cons)+
apply (rule weak_det_spec_mapM)
apply (simp add: Cons)+
done
qed
lemma weak_det_spec_compose:
assumes Q:"\<And>Q r. weak_det_spec (Q r) (b r)"
assumes P:"\<And>P. weak_det_spec P a"
shows "\<And>P. weak_det_spec P (a>>=b)"
apply (clarsimp simp:weak_det_spec_def)
apply (frule no_fail_compose_imp)
apply clarsimp
apply (rule det_compose)
apply (simp add: P[THEN weak_det_specD])
apply (drule_tac x = r in spec)
apply (erule Q[THEN weak_det_specD])
apply simp
done
lemma weak_det_spec_select_f:
"\<lbrakk>\<And>P. weak_det_spec P f\<rbrakk> \<Longrightarrow> weak_det_spec Q (select_f (f a))"
apply (case_tac "\<forall>s. \<not>Q s")
apply (simp add:weak_det_spec_def no_fail_def det_spec_def)
apply (clarsimp simp:weak_det_spec_def)
apply (rule det_spec_select_f[where P = "(=) a"])
apply simp
apply (drule_tac x = "(=) a" in meta_spec)
apply (clarsimp simp: no_fail_def select_f_def)
done
lemma weak_det_spec_fail:
"weak_det_spec P fail"
by (auto simp: weak_det_spec_def no_fail_def fail_def det_spec_def)
lemma weak_det_spec_assert:
"weak_det_spec P (assert x)"
by (auto simp:weak_det_spec_fail assert_def det_imply_weak_det[OF det_spec_return])
lemma weak_det_spec_assert_opt:
"weak_det_spec P (assert_opt x)"
by (auto simp: weak_det_spec_fail det_imply_weak_det[OF det_spec_return] assert_opt_def split:option.splits)
lemma weak_det_spec_gets_the:
"weak_det_spec P (gets_the f)"
apply (simp add:gets_the_def)
apply (rule weak_det_spec_compose[OF weak_det_spec_assert_opt det_imply_weak_det[OF det_spec_gets]])
done
lemma weak_det_spec_loadWord:
"weak_det_spec P (loadWord x)"
apply (clarsimp simp:loadWord_def)
apply (rule weak_det_spec_compose)+
apply (rule det_imply_weak_det[OF det_spec_return])
apply (rule weak_det_spec_assert)
apply (rule det_imply_weak_det[OF det_spec_gets])
done
lemmas weak_det_spec_simps = weak_det_spec_fail weak_det_spec_assert weak_det_spec_assert_opt weak_det_spec_gets_the
det_imply_weak_det[OF det_spec_return] det_imply_weak_det[OF det_spec_get]
det_imply_weak_det[OF det_spec_gets] det_imply_weak_det[OF det_spec_modify]
lemma weak_det_spec_storeWord:
"weak_det_spec P (storeWord a b)"
apply (simp add:storeWord_def)
apply (rule weak_det_spec_compose)+
apply (simp_all add:weak_det_spec_simps)
done
lemma weak_det_spec_thread_get:
"weak_det_spec P (thread_get f x)"
apply (simp add:thread_get_def)
apply (rule weak_det_spec_compose)
apply (clarsimp simp:weak_det_spec_simps)+
done
lemma weak_det_spec_load_word_offs:
"weak_det_spec P (load_word_offs buf r)"
apply (clarsimp simp:load_word_offs_def)
apply (clarsimp simp:do_machine_op_def)
apply (rule weak_det_spec_compose)+
apply clarsimp
apply (rule weak_det_spec_compose)+
apply (rule det_imply_weak_det[OF det_spec_return])
apply (rule det_imply_weak_det[OF det_spec_modify])
apply (rule weak_det_spec_select_f)
apply (rule weak_det_spec_loadWord)
apply (rule det_imply_weak_det[OF det_spec_gets])
done
lemma empty_when_fail_fail:
"empty_when_fail fail"
by (clarsimp simp:empty_when_fail_def fail_def)
lemma empty_when_fail_get:
"empty_when_fail get"
by (clarsimp simp:empty_when_fail_def get_def return_def)
lemma empty_when_fail_gets:
"empty_when_fail (gets x)"
by (clarsimp simp:empty_when_fail_def get_def return_def gets_def bind_def)
lemma empty_when_fail_assert:
"empty_when_fail (assert x)"
by(clarsimp simp:empty_when_fail_def assert_def fail_def return_def bind_def)
lemma empty_when_fail_assert_opt:
"empty_when_fail (assert_opt x)"
by (auto simp:assert_opt_def fail_def return_def empty_when_fail_def split:option.splits)
lemma empty_when_fail_gets_the:
"empty_when_fail (gets_the f)"
apply (clarsimp simp:gets_the_def)
apply (rule empty_when_fail_compose)+
apply (rule empty_when_fail_assert_opt)
apply (rule empty_when_fail_gets)+
apply (rule det_imply_weak_det[OF det_spec_gets])
done
lemma empty_when_fail_modify:
"empty_when_fail (modify x)"
by (clarsimp simp:empty_when_fail_def simpler_modify_def)
lemmas empty_when_fail_simps = empty_when_fail_fail empty_when_fail_return empty_when_fail_get empty_when_fail_gets
empty_when_fail_gets_the empty_when_fail_assert empty_when_fail_assert_opt empty_when_fail_modify
lemma empty_when_fail_loadWord:
"empty_when_fail (loadWord x)"
apply (simp add:loadWord_def)
apply (rule empty_when_fail_compose[OF _ empty_when_fail_gets])
apply (rule empty_when_fail_compose[OF empty_when_fail_return])
apply (simp_all add: weak_det_spec_simps empty_when_fail_simps)+
done
lemma empty_when_fail_storeWord:
"empty_when_fail (storeWord a b)"
apply (simp add:storeWord_def)
apply (rule empty_when_fail_compose)+
apply (simp_all add:empty_when_fail_simps weak_det_spec_simps)
done
lemma empty_when_fail_select_f:
"\<lbrakk>empty_when_fail f\<rbrakk> \<Longrightarrow> empty_when_fail (select_f (f a))"
by (clarsimp simp:empty_when_fail_def select_f_def)
lemma empty_when_fail_thread_get:
"empty_when_fail (thread_get f x)"
apply (clarsimp simp:thread_get_def)
apply (rule empty_when_fail_compose)
apply (clarsimp simp:empty_when_fail_simps weak_det_spec_simps)+
done
lemma empty_when_fail_load_word_offs:
"empty_when_fail (load_word_offs buf r)"
apply (clarsimp simp:load_word_offs_def)
apply (clarsimp simp:do_machine_op_def)
apply (rule empty_when_fail_compose[OF _ empty_when_fail_gets])
apply (rule empty_when_fail_compose[OF _ empty_when_fail_select_f])
apply clarsimp
apply (rule empty_when_fail_compose[OF empty_when_fail_return])
apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_loadWord)
apply (rule weak_det_spec_select_f[OF weak_det_spec_loadWord])
done
lemma empty_when_fail_get_object:
"empty_when_fail (get_object x)"
apply (simp add:get_object_def)
apply (rule empty_when_fail_compose)+
apply (simp add:empty_when_fail_simps weak_det_spec_simps)+
done
lemma weak_det_spec_get_object:
"weak_det_spec P (get_object x)"
apply (simp add:get_object_def)
apply (rule weak_det_spec_compose)+
apply (simp add:weak_det_spec_simps)+
done
lemma weak_det_spec_get_cap:
"weak_det_spec P (get_cap slot)"
apply (case_tac slot)
apply (simp add:get_cap_def)
apply (rule weak_det_spec_compose)+
apply (simp_all add:weak_det_spec_simps weak_det_spec_get_object)
apply (case_tac r)
apply (simp_all add:weak_det_spec_simps weak_det_spec_get_object)
apply (rule weak_det_spec_compose)
apply (simp_all add:weak_det_spec_simps weak_det_spec_get_object)
done
lemma empty_when_fail_get_cap:
"empty_when_fail (get_cap slot)"
apply (case_tac slot)
apply (clarsimp simp:get_cap_def)
apply (rule empty_when_fail_compose)+
apply (simp_all add:empty_when_fail_simps empty_when_fail_get_object weak_det_spec_get_object)
apply (case_tac r)
apply (simp_all add:empty_when_fail_simps empty_when_fail_get_object weak_det_spec_get_object)
apply (rule empty_when_fail_compose)
apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_get_object)
apply (case_tac r)
apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_get_object)
apply (rule weak_det_spec_compose)
apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_get_object)
done
lemma not_emptyI: "a\<noteq>{} \<Longrightarrow>\<exists>x. x\<in> a"
by auto
lemma evalMonad_do_machine_op:
assumes "weak_det_spec ((=) (machine_state sa)) f"
assumes "empty_when_fail f"
shows "evalMonad (f) (machine_state sa) =
evalMonad (do_machine_op (f)) sa"
apply (clarsimp simp:evalMonad_def do_machine_op_def gets_def get_def bind_def return_def simpler_modify_def)
apply (clarsimp simp:select_f_def | rule conjI)+
apply (drule not_emptyI)
apply clarsimp
apply (rule_tac x = "(a,b)" in bexI)
apply clarsimp+
apply (rule arg_cong[where f = "(\<lambda>A. (SOME x. x\<in> A))"])
apply (rule set_eqI)
apply (clarsimp simp:image_def)
apply (rule iffI)
apply clarsimp
using assms
apply (clarsimp simp:empty_when_fail_def weak_det_spec_def no_fail_def)
apply (drule_tac x = "machine_state sa" in spec)
apply (clarsimp simp:det_spec_def)
using assms
apply (clarsimp simp:empty_when_fail_def weak_det_spec_def no_fail_def)
apply force
done
lemma evalMonad_wp:
"\<lbrakk>empty_when_fail f; weak_det_spec ((=) pres) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) pres \<rbrace>f\<lbrace>\<lambda>rv s. evalMonad f pres = Some rv\<rbrace>"
apply (clarsimp simp:valid_def weak_det_spec_def no_fail_def empty_when_fail_def)
apply (drule_tac x = pres in spec)
apply (clarsimp simp:evalMonad_def notemptyI det_spec_def)
done
lemma evalMonad_compose:
"\<lbrakk>empty_when_fail a;weak_det_spec ((=) s) a;\<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk>
\<Longrightarrow> evalMonad (a>>=b) s = (case (evalMonad a s) of Some r \<Rightarrow> evalMonad (b r) s | _ \<Rightarrow> None)"
apply (clarsimp simp:evalMonad_def weak_det_spec_def)
apply (clarsimp simp:no_fail_def det_spec_def empty_when_fail_def)
apply (drule_tac x = s in spec)+
apply (case_tac "snd (a s)")
apply (simp_all)
apply (fastforce simp:bind_def valid_def)
apply (clarsimp simp:valid_def)
apply (drule_tac x = s in meta_spec)
apply (clarsimp simp:bind_def)
done
lemma evalMonad_thread_get:
"evalMonad (thread_get f thread) sa = Some x \<Longrightarrow> \<exists>tcb. get_tcb thread sa = Some tcb \<and> f tcb = x"
by (clarsimp simp:thread_get_def evalMonad_def gets_def gets_the_def
assert_opt_def bind_def get_def return_def get_tcb_def fail_def
split:option.splits Structures_A.kernel_object.splits)
lemma evalMonad_get_cap:
"evalMonad (get_cap slot) s = caps_of_state s slot"
using weak_det_spec_get_cap[where P ="(=) s" and slot = slot]
using empty_when_fail_get_cap[where slot = slot]
apply (clarsimp simp:evalMonad_def caps_of_state_def empty_when_fail_def
weak_det_spec_def no_fail_def det_spec_def)
apply (drule_tac x = s in spec)
apply clarsimp
apply (subgoal_tac "\<lbrace>(=) s\<rbrace>get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>")
apply (clarsimp simp:valid_def)
apply wp
done
lemma evalMonad_loadWord:
"evalMonad (loadWord x) ms =
(if x && mask 2 = 0 then
Some (word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x])
else None)"
by (clarsimp simp: loadWord_def gets_def get_def return_def bind_def assert_def fail_def evalMonad_def)
lemma weak_det_spec_lookup_ipc_buffer:
"weak_det_spec P (lookup_ipc_buffer a b)"
apply (simp add:lookup_ipc_buffer_def)
apply (rule weak_det_spec_compose)+
apply (simp_all add: empty_when_fail_simps empty_when_fail_get_cap empty_when_fail_thread_get
weak_det_spec_simps weak_det_spec_thread_get weak_det_spec_get_cap)
apply (case_tac ra; simp add:weak_det_spec_simps)
apply (rename_tac arch_cap)
apply (case_tac arch_cap; simp add:weak_det_spec_simps)
done
lemma empty_when_fail_lookup_ipc_buffer:
"empty_when_fail (lookup_ipc_buffer a b)"
apply (simp add:lookup_ipc_buffer_def)
apply (rule empty_when_fail_compose)+
apply (simp_all add: empty_when_fail_simps empty_when_fail_get_cap empty_when_fail_thread_get
weak_det_spec_simps weak_det_spec_thread_get weak_det_spec_get_cap)
apply (case_tac ra; simp add:empty_when_fail_simps)
apply (rename_tac arch_cap)
apply (case_tac arch_cap; simp add:empty_when_fail_simps)
done
abbreviation
"\<lambda>s. ipc_frame_cte_at thread buf rights sz s \<equiv>
\<lambda>s. (\<exists>mapdata dev. cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata))) (thread,tcb_cnode_index 4) s)"
lemma lookup_ipc_buffer_SomeB_evalMonad:
"evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf)
\<Longrightarrow> \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> in_receive \<or> (AllowWrite \<in> rs))
\<and> ipc_frame_cte_at thread b rs sz sa \<and> ko_at (TCB obj) thread sa
\<and> (buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))"
apply (simp add:lookup_ipc_buffer_def)
apply (subst (asm) evalMonad_compose)
apply (clarsimp simp:empty_when_fail_thread_get weak_det_spec_thread_get)+
apply wp
apply (clarsimp split:option.splits dest!:evalMonad_thread_get)
apply (subst (asm) evalMonad_compose)
apply (clarsimp simp:empty_when_fail_get_cap weak_det_spec_get_cap)+
apply wp
apply (clarsimp simp:evalMonad_get_cap split:option.splits)
apply (clarsimp dest!:caps_of_state_cteD get_tcb_SomeD simp:obj_at_def split:cap.splits arch_cap.splits if_splits)
apply (clarsimp simp:cte_wp_at_cases)
apply (fastforce simp: obj_at_def vm_read_only_def vm_read_write_def)
done
lemma lookup_ipc_buffer_None_evalMonad:
"evalMonad (lookup_ipc_buffer in_receive thread) sa = Some None
\<Longrightarrow> \<exists>obj. ko_at (TCB obj) thread sa \<and> (\<forall>b rs sz. ipc_frame_cte_at thread b rs sz sa
\<longrightarrow> ((AllowRead \<notin> rs \<and> \<not> in_receive) \<or> (in_receive \<and> (AllowWrite \<notin> rs \<or> AllowRead\<notin> rs)))) "
apply (simp add:lookup_ipc_buffer_def)
apply (subst (asm) evalMonad_compose)
apply (clarsimp simp:empty_when_fail_thread_get weak_det_spec_thread_get)+
apply wp
apply (clarsimp split:option.splits dest!:evalMonad_thread_get)
apply (subst (asm) evalMonad_compose)
apply (clarsimp simp:empty_when_fail_get_cap weak_det_spec_get_cap)+
apply wp
apply (clarsimp simp:evalMonad_get_cap split:option.splits)
apply (clarsimp dest!:caps_of_state_cteD get_tcb_SomeD)
apply (simp add:obj_at_def cte_wp_at_cases split:cap.splits arch_cap.splits if_splits)
apply (clarsimp simp:vm_read_only_def vm_read_write_def)
done
lemma cdl_get_ipc_buffer_None: