-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathSyscall_DR.thy
1680 lines (1579 loc) · 82.9 KB
/
Syscall_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 Syscall_DR
imports
Tcb_DR
Schedule_DR
Interrupt_DR
begin
context begin interpretation Arch . (*FIXME: arch-split*)
(*
* Translate an abstract invocation into a corresponding
* CDL invocation.
*)
definition
translate_invocation :: "Invocations_A.invocation \<Rightarrow> cdl_invocation"
where
"translate_invocation x \<equiv>
case x of
Invocations_A.InvokeUntyped iu \<Rightarrow>
Invocations_D.InvokeUntyped $
translate_untyped_invocation iu
| Invocations_A.InvokeEndpoint ep bdg grant grant_reply \<Rightarrow>
Invocations_D.InvokeEndpoint $
SyncMessage bdg grant grant_reply ep
| Invocations_A.InvokeNotification ntfn aebdg \<Rightarrow>
Invocations_D.InvokeNotification $
Signal aebdg ntfn
| Invocations_A.InvokeReply target_tcb reply_slot grant \<Rightarrow>
Invocations_D.InvokeReply $
ReplyMessage target_tcb (transform_cslot_ptr reply_slot) grant
| Invocations_A.InvokeCNode icn \<Rightarrow>
Invocations_D.InvokeCNode $
translate_cnode_invocation icn
| Invocations_A.InvokeTCB itcb \<Rightarrow>
Invocations_D.InvokeTcb $ translate_tcb_invocation itcb
| Invocations_A.InvokeDomain itcb d \<Rightarrow> Invocations_D.InvokeDomain $ SetDomain itcb d
| Invocations_A.InvokeIRQControl irqc \<Rightarrow>
Invocations_D.InvokeIrqControl $ translate_irq_control_invocation irqc
| Invocations_A.InvokeIRQHandler irrqh \<Rightarrow>
Invocations_D.InvokeIrqHandler $ translate_irq_handler_invocation irrqh
"
definition
cdl_invocation_relation :: "cdl_invocation \<Rightarrow> Invocations_A.invocation \<Rightarrow> bool"
where
"cdl_invocation_relation x y \<equiv>
case y of Invocations_A.InvokeArchObject invo \<Rightarrow> arch_invocation_relation x invo
| _ \<Rightarrow> x = translate_invocation y"
(* we store the simplified version of this lemma, since the 'liftME's in
* the goal are invariably simplified before this rule is applied *)
lemma dcorres_liftME_liftME [simplified]:
"\<lbrakk>dcorres (dc \<oplus> rvrel) G G' m m';
\<And> r r'. rvrel r r' \<Longrightarrow> rvrel' (f r) (f' r')\<rbrakk>
\<Longrightarrow>
dcorres (dc \<oplus> rvrel') G G' (liftME f m) (liftME f' m')"
apply(simp, rule_tac r'="(dc \<oplus> rvrel)" and r="dc \<oplus> ((\<lambda> x. rvrel' x \<circ> f') \<circ> f)" in corres_rel_imp)
apply(assumption)
apply(case_tac x, simp)
apply(case_tac y, simp_all)
done
(* Decoding NullCap invocations is equivalent. *)
lemma decode_invocation_nullcap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label) args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.NullCap \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (unfold Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply (clarsimp simp: transform_cap_def)
done
(* Decoding UntypedCap invocations is equivalent. *)
lemma decode_invocation_untypedcap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.UntypedCap dev a b idx \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top>
(invs and cte_wp_at ((=) invoked_cap') invoked_cap_ref'
and (\<lambda>s. \<forall>x \<in> set (map fst excaps'). s \<turnstile> x)
and (\<lambda>s. \<forall>x \<in> set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)
and valid_etcbs)
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply (case_tac "\<exists> ui. intent = UntypedIntent ui")
apply (clarsimp simp: throw_opt_def get_untyped_intent_def split: cdl_intent.splits option.splits)
apply (rule dcorres_liftME_liftME)
apply (rule corres_guard_imp, rule decode_untyped_corres, auto simp: transform_cap_def)[1]
apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def)
apply (clarsimp simp: throw_opt_def get_untyped_intent_def split: cdl_intent.split)
apply (rule absorb_imp,clarsimp)+
apply (rule dcorres_free_throw)
apply (subst decode_untyped_label_not_match)
apply simp+
done
(* Decoding Endpoint invocations is equivalent. *)
lemma decode_invocation_endpointcap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.EndpointCap a b c \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (clarsimp simp: Decode_A.decode_invocation_def
Decode_D.decode_invocation_def)
apply (rule corres_returnOk)
apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def)
done
(* Decoding Async Endpoint invocations is equivalent. *)
lemma decode_invocation_notificationcap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.NotificationCap a b c \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply (auto simp: cdl_invocation_relation_def translate_invocation_def
split:rights.splits intro!:corres_returnOk)
done
(* Decoding ReplyCap invocations is equivalent. *)
lemma decode_invocation_replycap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.ReplyCap a b c \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top> (cte_wp_at (Not\<circ> is_master_reply_cap) invoked_cap_ref' and
cte_wp_at ((=) invoked_cap') invoked_cap_ref')
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def )
apply (rule dcorres_expand_pfx)
apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def
split:rights.splits)
apply (clarsimp simp:cte_wp_at_def is_master_reply_cap_def)
apply (rule corres_guard_imp[OF dcorres_returnOk])
apply (simp add:cdl_invocation_relation_def translate_invocation_def)+
done
(* Decoding CNode invocations is equivalent. *)
lemma decode_invocation_cnodecap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.CNodeCap a b c \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top>
(invs and valid_cap invoked_cap' and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) and valid_etcbs)
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply (case_tac "\<exists> ui. intent = CNodeIntent ui")
apply (rotate_tac -1, erule exE)
apply (rotate_tac -1, drule sym)
apply (clarsimp simp: get_cnode_intent_def throw_opt_def split: cdl_intent.split)
apply (rule dcorres_liftME_liftME)
apply (rule decode_cnode_corres, auto simp: transform_cap_def)[1]
apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def)
apply (clarsimp simp: throw_opt_def get_cnode_intent_def split: cdl_intent.split)
apply (rule absorb_imp,clarsimp)+
apply (rule dcorres_free_throw)
apply (subst decode_cnode_label_not_match)
apply simp+
done
(* Decoding TCB invocations is equivalent. *)
lemma decode_invocation_tcbcap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.ThreadCap a \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply(case_tac "\<exists> ti. intent = (TcbIntent ti) ")
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply (clarsimp simp: throw_opt_def get_cnode_intent_def get_tcb_intent_def split: cdl_intent.split)
apply (rule corres_rel_imp[OF decode_tcb_corres],simp+)
apply (case_tac x)
apply (clarsimp simp:cdl_invocation_relation_def translate_invocation_def)+
apply (clarsimp simp:Decode_D.decode_invocation_def throw_opt_def get_tcb_intent_def Decode_A.decode_invocation_def
split:cdl_intent.splits)
apply (rule absorb_imp,clarsimp)+
apply (rule dcorres_free_throw)
apply (rule decode_tcb_cap_label_not_match)
apply (drule sym,clarsimp)
apply simp
done
lemma fst_hd_map_eq: "\<lbrakk> xs \<noteq> []; fst (hd xs) = x \<rbrakk> \<Longrightarrow> fst (hd (map (\<lambda>(x, y). (f x, g y)) xs)) = f x"
apply (case_tac xs)
apply (auto simp: fst_def hd_def split: list.splits)
done
lemma decode_domain_corres:
"\<lbrakk> Some (DomainIntent i) = transform_intent (invocation_type label') args';
excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) \<top> \<top>
(Tcb_D.decode_domain_invocation excaps i)
(Decode_A.decode_domain_invocation label' args' excaps')"
apply (unfold Tcb_D.decode_domain_invocation_def Decode_A.decode_domain_invocation_def)
apply (unfold transform_cap_list_def)
apply (case_labels "invocation_type label'"; simp add: gen_invocation_type_eq)
apply (clarsimp simp: transform_intent_def option_map_def
split: option.splits)+
defer
apply (clarsimp simp: transform_intent_def option_map_def split: option.splits)+
apply (clarsimp simp: transform_intent_domain_def)
apply (case_tac "args'")
apply simp
apply (clarsimp simp: bindE_def lift_def)
apply (rule_tac Q'="\<lambda>rv s. case rv of Inr b \<Rightarrow> ucast a = b | _ \<Rightarrow> True" in corres_symb_exec_r)
apply (case_tac "rv")
apply (simp add: lift_def)
apply (rule corres_alternate2, simp)
apply (simp add: lift_def)
apply (fold bindE_def)
apply (rule dcorres_whenE_throwError_abstract')
apply (rule corres_alternate2)
apply simp
apply (case_tac "fst (hd (excaps'))"; simp)
apply ((rule corres_alternate2, simp)+)[6]
apply (rule corres_alternate1)
apply (clarsimp simp: returnOk_def cdl_invocation_relation_def translate_invocation_def split: list.splits)
apply (simp add: fst_hd_map_eq)
apply (rule corres_alternate2, simp)+
apply (rule validE_cases_valid)
apply (wp whenE_inv| simp)+
done
lemma decode_domain_cap_label_not_match:
"\<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>"
apply (case_tac "invocation_type label' = GenInvocationLabel DomainSetSet")
apply (clarsimp simp: Decode_A.decode_domain_invocation_def transform_intent_def gen_invocation_type_eq)+
apply (clarsimp simp: transform_intent_domain_def split: option.splits list.splits)
apply wp
apply (simp add: Decode_A.decode_domain_invocation_def gen_invocation_type_eq)
apply wp
done
lemma decode_invocation_domaincap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label) args;
invoked_cap_ref = transform_cslot_ptr slot;
invoked_cap = transform_cap cap;
excaps = transform_cap_list excaps';
cap = cap.DomainCap\<rbrakk>
\<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label args cap_index slot cap excaps')"
apply (case_tac "\<exists>ti. intent = (DomainIntent ti)")
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply (clarsimp simp: throw_opt_def get_domain_intent_def split: cdl_intent.split)
apply (rule corres_rel_imp[OF decode_domain_corres],simp+)
apply (clarsimp simp:Decode_D.decode_invocation_def throw_opt_def get_domain_intent_def Decode_A.decode_invocation_def
split:cdl_intent.splits)
apply (rule absorb_imp,clarsimp)+
apply (rule dcorres_free_throw)
apply (rule decode_domain_cap_label_not_match)
apply (drule sym,clarsimp)
done
(* Decoding IRQ Control invocations is equivalent. *)
lemma decode_invocation_irqcontrolcap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.IRQControlCap \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation)
\<top>
(valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) and valid_global_refs and valid_idle and valid_etcbs)
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply(case_tac "\<exists> ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'")
apply(erule exE, rotate_tac -1, drule sym)
apply(clarsimp simp: throw_opt_def get_irq_control_intent_def)
apply (rule dcorres_liftME_liftME)
apply (rule decode_irq_control_corres, auto simp: transform_cap_def)[1]
apply (clarsimp simp: cdl_irq_control_invocation_relation_def)
apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def)
apply (rule corres_guard_imp)
apply (clarsimp simp: throw_opt_def split: cdl_intent.split option.splits)
apply (auto simp: get_irq_control_intent_def split: cdl_intent.split intro!: decode_irq_control_error_corres)
done
(* Decoding IRQ Handler invocations is equivalent. *)
lemma decode_invocation_irqhandlercap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.IRQHandlerCap x \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
apply (clarsimp simp: throw_opt_def get_irq_handler_intent_def split: option.splits)
apply (rule conjI)
apply (auto simp: decode_irq_handler_invocation_def transform_intent_def
simp flip: gen_invocation_type_eq
split del: if_split
split: invocation_label.splits gen_invocation_labels.splits cdl_intent.splits list.splits)[1]
apply clarsimp
apply (simp split: cdl_intent.splits)
apply (rule corres_rel_imp)
apply (erule decode_irq_handler_corres, simp+)[1]
apply clarsimp
apply (case_tac xa, simp)
apply (simp add: cdl_invocation_relation_def
cdl_irq_handler_invocation_relation_def
translate_invocation_def)
done
lemma transform_type_eq_None:
"(transform_type a = None) \<Longrightarrow> (data_to_obj_type a = throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0))"
apply (clarsimp simp:data_to_obj_type_def transform_type_def split:if_split_asm)
apply (simp add:unat_arith_simps)
apply (clarsimp simp:arch_data_to_obj_type_def)
apply (rule conjI,arith,clarsimp)+
done
lemma transform_intent_untyped_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>"
including no_pre
supply gen_invocation_type_eq[symmetric, simp]
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply wp
apply (case_labels "invocation_type label")
(* 46 subgoals *)
apply (clarsimp simp:Decode_A.decode_untyped_invocation_def unlessE_def, wp)+
apply (clarsimp simp:transform_intent_def Decode_A.decode_untyped_invocation_def unlessE_def split del:if_split)
apply (clarsimp simp:transform_intent_untyped_retype_def split del:if_split)
apply (case_tac "args")
apply (clarsimp,wp)[1]
apply (clarsimp split:list.split_asm split del:if_split)
apply (wp+)[5]
apply (clarsimp simp: transform_type_eq_None split del:if_split split:option.splits)
apply (wp|clarsimp simp:whenE_def|rule conjI)+
apply (clarsimp simp: Decode_A.decode_untyped_invocation_def unlessE_def split del:if_split,wp)+
done
lemma transform_intent_cnode_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>"
supply if_cong[cong]
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply (simp add: Decode_A.decode_cnode_invocation_def unlessE_def upto_enum_def
fromEnum_def toEnum_def enum_invocation_label enum_gen_invocation_labels
whenE_def)
apply (intro conjI impI;
clarsimp simp: transform_intent_def transform_cnode_index_and_depth_def
transform_intent_cnode_copy_def
transform_intent_cnode_mint_def transform_intent_cnode_move_def
transform_intent_cnode_mutate_def transform_intent_cnode_rotate_def
simp flip: gen_invocation_type_eq
split: list.split_asm;
(solves \<open>wpsimp\<close>)?)
done
lemma transform_intent_thread_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.ThreadCap w\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>"
including no_pre
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply wp+
apply (simp add:Decode_A.decode_tcb_invocation_def)
apply (cases "gen_invocation_type label"; simp; wp?)
apply (clarsimp simp: transform_intent_def decode_read_registers_def decode_write_registers_def
decode_copy_registers_def decode_tcb_configure_def decode_set_priority_def
decode_set_mcpriority_def decode_set_sched_params_def
decode_set_ipc_buffer_def transform_intent_tcb_defs
simp flip: gen_invocation_type_eq
split: list.split_asm
| wp+)+
apply (clarsimp simp: transform_intent_def decode_set_space_def decode_bind_notification_def
decode_unbind_notification_def transform_intent_tcb_set_space_def
split: list.split_asm
, wp+
| clarsimp simp: transform_intent_def simp flip: gen_invocation_type_eq)+
done
lemma transform_intent_irq_control_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.IRQControlCap\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>,
\<lbrace>\<lambda>x. (=) s\<rbrace>"
including no_pre
supply gen_invocation_type_eq[symmetric, simp] if_cong[cong]
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply wp
apply (clarsimp simp:decode_irq_control_invocation_def arch_decode_irq_control_invocation_def
split del:if_split)
apply (case_labels "invocation_type label"; (clarsimp, wp)?)
apply (clarsimp simp:transform_intent_issue_irq_handler_def transform_intent_def
split:list.split_asm split del:if_split,wp+)
apply (clarsimp simp:arch_transform_intent_issue_irq_handler_def transform_intent_def
split:list.split_asm split del:if_split,wp+)
done
lemma transform_intent_irq_handler_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.IRQHandlerCap w\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>"
supply gen_invocation_type_eq[symmetric, simp]
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply (wp)
apply (clarsimp simp:decode_irq_handler_invocation_def|rule conjI)+
apply (clarsimp simp:transform_intent_def split: list.splits)+
apply (clarsimp simp:transform_intent_def |rule conjI | wp)+
done
lemma transform_intent_zombie_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.Zombie w option n\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>"
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply (wp)
done
lemma transform_intent_domain_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>"
including no_pre
supply gen_invocation_type_eq[symmetric, simp]
apply (clarsimp simp: Decode_A.decode_invocation_def)
apply wp
apply (case_tac excaps, simp_all)
apply (clarsimp simp: decode_domain_invocation_def)
apply (case_tac args, simp_all)
apply (wp whenE_inv whenE_inv[THEN valid_validE] | simp)+
apply (clarsimp simp: decode_domain_invocation_def)
apply (case_tac args, simp_all)
apply ((wp whenE_inv whenE_inv[THEN valid_validE] | simp)+)[1]
apply (case_tac "invocation_type label \<noteq> GenInvocationLabel DomainSetSet", simp_all)
apply wp
apply (clarsimp simp: transform_intent_def transform_intent_domain_def)
done
lemma transform_intent_arch_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.ArchObjectCap arch_cap\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>"
including no_pre
supply gen_invocation_type_eq[symmetric, simp]
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply wp
apply (simp add: arch_decode_invocation_def split del: if_split)
apply (case_tac arch_cap)
apply (case_labels "invocation_type label"; simp split del: if_split, wp?)
apply (clarsimp split: if_splits | rule conjI)+
apply (case_tac "excaps ! 0")
apply (clarsimp split: cap.splits | rule conjI | wp)+
apply (clarsimp split: arch_cap.splits | rule conjI | wp)+
apply ((clarsimp simp: transform_intent_def | wp) +)[2]
apply (case_labels "invocation_type label"
; wpsimp simp: arch_decode_invocation_def split_del: if_split)
apply (case_tac "excaps ! 0")
apply (clarsimp simp: transform_intent_def transform_cnode_index_and_depth_def
split: list.split_asm)
apply wp+
apply (case_labels "invocation_type label"
; wpsimp simp: arch_decode_invocation_def isPageFlushLabel_def split_del: if_split)
apply (clarsimp simp: transform_intent_def transform_intent_page_map_def
split: list.split_asm )
apply wp+
apply (case_tac "excaps ! 0")
apply (clarsimp simp:transform_intent_def split:list.split_asm)
apply ((clarsimp simp:transform_intent_def | wp)+)
apply (case_labels "invocation_type label"; simp)
apply (intro conjI impI | wp)+
apply (clarsimp | rule conjI)+
apply (clarsimp simp: transform_intent_def transform_intent_page_table_map_def
split: list.split_asm)
apply (intro conjI impI | wp)+
apply ((clarsimp simp: transform_intent_def split: list.split_asm | wp)+)[1]
apply (case_labels "invocation_type label"; simp add: isPDFlushLabel_def)
apply (wp)+
done
lemma decode_invocation_error_branch:
"\<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap)\<rbrakk>
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>x. (=) s\<rbrace>"
apply (case_tac cap)
apply (simp_all add:ep_related_cap_def transform_cap_def split:if_split_asm)
apply (clarsimp simp:Decode_A.decode_invocation_def,wp)
apply (rule transform_intent_untyped_cap_None,fastforce+)
apply (clarsimp simp:Decode_A.decode_invocation_def,wp)
apply (rule transform_intent_cnode_cap_None,fastforce+)
apply (rule transform_intent_thread_cap_None,fastforce+)
apply (rule transform_intent_domain_cap_None,fastforce+)
apply (rule transform_intent_irq_control_None,fastforce+)
apply (rule transform_intent_irq_handler_None,fastforce+)
apply (rule transform_intent_zombie_cap_None,fastforce+)
apply (rule transform_intent_arch_cap_None,fastforce+)
done
lemma decode_invocation_ep_related_branch:
"\<lbrakk>ep_related_cap (transform_cap cap);\<not> is_master_reply_cap cap\<rbrakk>
\<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation (transform_cap cap) (transform_cslot_ptr ref) caps intent)
(Decode_A.decode_invocation label args index ref cap caps')"
apply (clarsimp simp:ep_related_cap_def transform_cap_def split:cdl_cap.split_asm cap.split_asm arch_cap.split_asm)
apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def | rule conjI)+
apply (rule corres_guard_imp[OF dcorres_returnOk],simp add:cdl_invocation_relation_def translate_invocation_def)
apply simp+
apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def split:if_split_asm | rule conjI)+
apply (rule corres_guard_imp[OF dcorres_returnOk])
apply (simp add:cdl_invocation_relation_def translate_invocation_def)+
apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def is_master_reply_cap_def | rule conjI)+
apply (rule corres_guard_imp[OF dcorres_returnOk])
apply (simp add:cdl_invocation_relation_def translate_invocation_def)+
done
(*
* Decoding zombies invocations is equivalent.
*
*)
lemma decode_invocation_zombiecap_corres:
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
excaps = transform_cap_list excaps';
invoked_cap' = cap.Zombie x y z \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
by (simp add:Decode_A.decode_invocation_def Decode_D.decode_invocation_def)
(*
* Show that decoding of invocations corresponds.
*)
lemma decode_invocation_corres:
"\<lbrakk> (Some intent) = transform_intent (invocation_type label) args;
invoked_cap_ref = transform_cslot_ptr slot;
invoked_cap = transform_cap cap;
excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> cdl_invocation_relation) \<top>
(invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s)
and (cte_wp_at (Not \<circ> is_master_reply_cap) slot
and cte_wp_at ((=) cap) slot)
and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)
and valid_etcbs)
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
(Decode_A.decode_invocation label args cap_index slot cap excaps')"
apply(case_tac cap)
apply (rule corres_guard_imp,rule decode_invocation_nullcap_corres, fastforce+)[1]
apply (rule corres_guard_imp,rule decode_invocation_untypedcap_corres,
(fastforce elim: cte_wp_at_weakenE)+)[1]
apply (rule corres_guard_imp,rule decode_invocation_endpointcap_corres, fastforce+)[1]
apply (rule corres_guard_imp,rule decode_invocation_notificationcap_corres, fastforce+)[1]
apply (rule corres_guard_imp,rule decode_invocation_replycap_corres, fastforce+)[1]
apply (rule corres_guard_imp,rule decode_invocation_cnodecap_corres, fastforce+)[1]
apply (rule corres_guard_imp, rule decode_invocation_tcbcap_corres, fastforce+)[1]
apply (rule corres_guard_imp, rule decode_invocation_domaincap_corres, fastforce+)[1]
apply (rule corres_guard_imp, rule decode_invocation_irqcontrolcap_corres, fastforce+)[1]
apply (rule corres_guard_imp,rule decode_invocation_irqhandlercap_corres, fastforce+)[1]
apply (rule corres_guard_imp,rule decode_invocation_zombiecap_corres, fastforce+)[1]
apply (rule corres_guard_imp)
apply (rule corres_rel_imp)
apply (rule decode_invocation_archcap_corres, fastforce+)[1]
apply clarsimp
apply (case_tac x, simp)
apply (clarsimp simp: cdl_invocation_relation_def)
apply simp
apply simp
done
lemma ct_running_not_idle_etc:
"\<lbrakk> invs s; ct_running s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s \<and> thread_is_running (cur_thread s) s"
apply (simp add: not_idle_thread_def ct_in_state_def)
apply (subgoal_tac "valid_idle s")
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
apply (clarsimp simp: invs_def valid_state_def)
done
lemma ct_active_not_idle_etc:
"\<lbrakk> invs s; ct_active s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s"
apply (simp add: not_idle_thread_def ct_in_state_def)
apply (subgoal_tac "valid_idle s")
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
apply (clarsimp simp: invs_def valid_state_def)
done
lemma dcorres_set_eobject_tcb:
"\<lbrakk> \<exists>tcb'. (transform_tcb (machine_state s') p' tcb' etcb = Tcb tcb \<and> kheap s' p' = Some (TCB tcb'));
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 ))
(set_eobject p' etcb)"
supply if_cong[cong]
apply (clarsimp simp: corres_underlying_def set_eobject_def in_monad)
apply (clarsimp simp: KHeap_D.set_object_def simpler_modify_def)
apply (clarsimp simp: transform_def transform_current_thread_def transform_cdt_def transform_asid_table_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 invoke_domain_corres:
"\<lbrakk> i = cdl_invocation.InvokeDomain (SetDomain word1 word2);
i' = Invocations_A.invocation.InvokeDomain word1 word2\<rbrakk>
\<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True)
(invs and ct_active and valid_pdpt_objs and valid_etcbs and
invocation_duplicates_valid (Invocations_A.invocation.InvokeDomain word1 word2) and
(tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)))
(Tcb_D.invoke_domain (SetDomain word1 word2)) (Tcb_A.invoke_domain word1 word2)"
supply if_cong[cong]
apply (clarsimp simp: Tcb_D.invoke_domain_def Tcb_A.invoke_domain_def)
apply (rule corres_bind_return_r)
apply (clarsimp simp: Tcb_D.set_domain_def Tcb_A.set_domain_def)
apply (rule corres_symb_exec_r)
apply (rule_tac Q=\<top> and Q'="tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)" in dcorres_rhs_noop_above)
apply (rule tcb_sched_action_dcorres)
apply (rule dcorres_rhs_noop_below_True)
apply (rule corres_noop)
apply (wp reschedule_required_transform tcb_sched_action_transform | simp)+
apply (simp add: update_thread_def ethread_set_def thread_set_domain_def)
apply (rule dcorres_gets_the)
apply clarsimp
apply (drule get_tcb_at)
apply (clarsimp simp: opt_object_tcb transform_tcb_def)
apply (rule dcorres_set_eobject_tcb[simplified dc_def])
apply (frule get_tcb_SomeD)
apply (clarsimp simp: transform_tcb_def)
apply simp
apply (frule get_tcb_SomeD)
apply simp
apply (clarsimp simp: get_etcb_def split:option.splits)
apply clarsimp
apply (drule get_tcb_at)
apply (clarsimp simp:opt_object_tcb)
apply wp+
apply simp
apply wp
apply simp
done
(*
* Show that invocation of a cap corresponds.
*)
lemma perform_invocation_corres:
"\<lbrakk>cdl_invocation_relation i i'\<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> dc)
\<top> (invs and ct_active and valid_pdpt_objs and valid_etcbs
and invocation_duplicates_valid i' and valid_invocation i')
(Syscall_D.perform_invocation call block i)
(Syscall_A.perform_invocation block call i')"
apply (clarsimp simp: cdl_invocation_relation_def)
apply (case_tac i')
apply (simp_all add: translate_invocation_def split: Invocations_A.invocation.splits)
subgoal (* untyped *)
apply (simp add: liftME_def[symmetric])
apply (rule corres_guard_imp, rule invoke_untyped_corres)
apply clarsimp
apply clarsimp
done
subgoal (* send_ipc *)
apply (clarsimp simp:invoke_endpoint_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF get_cur_thread_corres])
apply (rule corres_dummy_return_l)
apply (rule corres_split)
apply (rule send_sync_ipc_corres; simp)
apply (rule corres_trivial[OF corres_free_return])
apply (wp|clarsimp)+
apply (clarsimp simp: ct_in_state_def obj_at_def pred_tcb_at_def not_idle_thread_def
valid_state_def invs_def valid_idle_def)
done
subgoal (* send_signal *)
apply (clarsimp simp:invoke_notification_def liftE_bindE)
apply (clarsimp simp:liftE_def bind_assoc returnOk_def)
apply (rule corres_guard_imp)
apply (rule corres_split)
apply (rule send_signal_corres; simp)
apply (rule corres_trivial)
apply (simp add:dc_def corres_free_return)
apply (wp | clarsimp)+
done
apply clarsimp
subgoal for word a b c (* invoke_reply *)
apply (clarsimp simp:invoke_reply_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF get_cur_thread_corres])
apply clarsimp
apply (rule corres_dummy_return_l)
apply (rule corres_split)
apply (rule do_reply_transfer_corres, simp)
apply (rule corres_trivial[OF corres_free_return])
apply (wp|clarsimp)+
apply (simp add: ct_active_not_idle_etc)
apply (rule conjI, fastforce)+
apply (subgoal_tac "valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s")
apply clarsimp
apply (drule (1) valid_reply_capsD)
apply (clarsimp simp: valid_idle_def not_idle_thread_def pred_tcb_at_def obj_at_def)
apply (fastforce simp: has_reply_cap_def is_reply_cap_to_def)
done
subgoal (* invoke_tcb *)
apply (rule corres_guard_imp)
apply (rule invoke_tcb_corres,simp+)
done
subgoal (* invoke_domain *)
apply (rule corres_guard_imp)
apply (rule invoke_domain_corres,simp+)
done
subgoal (* invoke_cnode *)
apply (rule corres_guard_imp)
apply (clarsimp simp:bindE_def returnOk_def lift_def bind_assoc)
apply (rule corres_dummy_return_l)
apply (rule corres_split[OF invoke_cnode_corres])
apply (clarsimp simp:lift_def,case_tac rv',simp add: throwError_def)
apply (simp)
apply (rule hoare_triv[of \<top>], rule hoare_TrueI)+
apply clarsimp+
done
subgoal for irq_control_invocation (* invoke_irq_control *)
apply (simp add:liftE_def bindE_def)
apply (case_tac irq_control_invocation)
(* generic *)
apply (rule corres_guard_imp)
apply (rule corres_split[where r'=dc])
apply (rule dcorres_invoke_irq_control)
apply (rule_tac F = "\<exists>x. rv' = Inr x" in corres_gen_asm2)
apply (rule corres_trivial)
apply (clarsimp simp:lift_def returnOk_def)
apply (rule hoare_triv[of \<top>], rule hoare_TrueI)+
apply ((wp|simp add: liftE_def)+)
(* arch *)
apply (rename_tac arch_label)
apply (case_tac arch_label)
apply (rule corres_guard_imp)
apply (rule corres_split[where r'=dc])
apply (rule dcorres_arch_invoke_irq_control[simplified])
apply (rule_tac F = "\<exists>x. rv' = Inr x" in corres_gen_asm2)
apply (rule corres_trivial)
apply (clarsimp simp:lift_def returnOk_def)
apply (rule hoare_triv[of \<top>], rule hoare_TrueI)
apply ((wp|simp add: liftE_def)+)
done
subgoal (* invoke_irq_handler *)
apply (clarsimp simp:liftE_bindE,simp add:liftE_def returnOk_def)
apply (rule corres_guard_imp)
apply (rule corres_split)
apply (rule dcorres_invoke_irq_handler)
apply (rule corres_trivial)
apply clarsimp
apply (wp|clarsimp)+
done
subgoal (* invoke_arch *)
apply (rule corres_guard_imp[OF invoke_arch_corres],fastforce+)
done
done (* invoke_tcb_corres *)
lemma sfi_generate_pending:
"\<lbrace>st_tcb_at(\<lambda>st. \<not>(generates_pending st)) thread\<rbrace> Ipc_A.send_fault_ipc thread ft
\<lbrace>\<lambda>t. \<top>\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. \<not> (generates_pending st)) thread\<rbrace>"
apply (clarsimp simp:send_fault_ipc_def Let_def lookup_cap_def)
apply (wp hoare_drop_imps hoare_allI|wpc|clarsimp|rule hoare_conjI)+
done
lemma dcorres_handle_double_fault:
"dcorres dc \<top> (valid_mdb and not_idle_thread thread and valid_idle and valid_etcbs)
(KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap)
(handle_double_fault thread ft' ft'a)"
apply (simp add:handle_double_fault_def )
apply (rule corres_guard_imp)
apply (rule set_thread_state_corres )
apply simp+
done
lemma handle_fault_corres:
"dcorres dc \<top>
(\<lambda>s. cur_thread s = thread \<and> not_idle_thread thread s \<and>
st_tcb_at active thread s \<and> valid_fault ft' \<and>
invs s \<and> valid_irq_node s \<and> valid_etcbs s)
Endpoint_D.handle_fault
(Ipc_A.handle_fault thread ft')"
apply (simp add:Endpoint_D.handle_fault_def Ipc_A.handle_fault_def)
apply (rule dcorres_gets_the)
apply (clarsimp dest!:get_tcb_SomeD)
apply (frule(1) valid_etcbs_tcb_etcb, clarsimp)
apply (rule corres_guard_imp)
apply (rule corres_split_catch[where r=dc and f = dc])
apply (rule_tac tcb = obj' and etcb=etcb in send_fault_ipc_corres)
apply (clarsimp simp:transform_def transform_current_thread_def
not_idle_thread_def)
apply (rule_tac F = "obj = cur_thread s'" in corres_gen_asm2)
apply simp
apply (rule dcorres_handle_double_fault)
apply (wp)
apply (simp add:send_fault_ipc_def not_idle_thread_def Let_def)
apply (wp hoare_drop_imps hoare_vcg_ball_lift | wpc)+
apply (rule_tac Q'="\<lambda>r s. invs s \<and> valid_etcbs s \<and> obj\<noteq> idle_thread s \<and> obj = cur_thread s'"
in hoare_strengthen_postE_R)
apply wp
apply (clarsimp simp:invs_mdb invs_valid_idle)
apply wp
apply simp
apply (clarsimp simp:obj_at_def transform_def
invs_mdb invs_valid_idle
transform_current_thread_def not_idle_thread_def)
apply (clarsimp dest!:get_tcb_SomeD
simp: generates_pending_def not_idle_thread_def st_tcb_at_def obj_at_def)+
apply (auto simp:transform_def transform_current_thread_def
not_idle_thread_def split:Structures_A.thread_state.splits)
done
lemma get_tcb_mrs_wp:
"\<lbrace>ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some (op_buf)) and (=) sa\<rbrace>
get_mrs thread (op_buf) (data_to_message_info (arch_tcb_get_registers (tcb_arch obj) msg_info_register))
\<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace>"
apply (case_tac op_buf)
apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def arch_tcb_get_registers_def)
apply (wp|wpc)+
apply (clarsimp simp:get_tcb_mrs_def Let_def)
apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_split)
apply (clarsimp simp:get_tcb_message_info_def get_ipc_buffer_words_empty)
apply (clarsimp dest!:get_tcb_SomeD simp:obj_at_def arch_tcb_context_get_def)
apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def arch_tcb_get_registers_def)
apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_split)
apply (wp|wpc)+
apply (rule_tac P = "tcb = obj" in hoare_gen_asm)
apply (clarsimp simp: get_tcb_mrs_def Let_def get_tcb_message_info_def Suc_leI[OF msg_registers_lt_msg_max_length]
arch_tcb_context_get_def
split del:if_split)
apply (rule_tac Q'="\<lambda>buf_mrs s. buf_mrs =
(get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))"
in hoare_strengthen_post)
apply (rule get_ipc_buffer_words[where thread=thread ])
apply simp
apply wp
apply (clarsimp simp:get_tcb_SomeD obj_at_def)
apply simp
done
lemma get_ipc_buffer_noop:
"\<lbrace>P and (\<lambda>s. \<exists>s'. s = transform s' \<and> tcb_at t s' \<and> valid_etcbs s' \<and> not_idle_thread t s')\<rbrace>
get_ipc_buffer t True \<exists>\<lbrace>\<lambda>r. P\<rbrace>"
apply (simp add:gets_the_def gets_def bind_assoc get_def split_def get_ipc_buffer_def tcb_at_def
exs_valid_def fail_def return_def bind_def assert_opt_def split:cdl_cap.splits)
apply clarsimp
apply (rule_tac x = "(the (opt_cap (t, tcb_ipcbuffer_slot) s),s)" for s in bexI)
apply (rule conjI|fastforce simp:fail_def return_def split:option.splits)+
apply (clarsimp split:option.splits simp:fail_def return_def)
apply (frule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp: opt_cap_tcb not_idle_thread_def)
done
lemma dcorres_reply_from_kernel:
"dcorres dc \<top> (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (corrupt_ipc_buffer oid True) (reply_from_kernel oid msg_rv)"
apply (simp add:reply_from_kernel_def)
apply (case_tac msg_rv)
apply (clarsimp simp:corrupt_ipc_buffer_def)
apply (rule dcorres_expand_pfx)
apply (rule_tac Q' = "\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)"
in corres_symb_exec_r)
apply (rule dcorres_expand_pfx)
apply (clarsimp)
apply (case_tac rv)
apply (rule corres_symb_exec_l)
apply (rule_tac F="rva = None" in corres_gen_asm)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_corrupt_tcb_intent_dupl)
apply (rule corres_split[OF set_register_corres])
unfolding K_bind_def
apply (rule corres_corrupt_tcb_intent_dupl)
apply (rule corres_split[OF set_mrs_corres_no_recv_buffer])
unfolding K_bind_def
apply (rule set_message_info_corres)
apply (wp | clarsimp simp:not_idle_thread_def)+
apply (wp get_ipc_buffer_noop, clarsimp)
apply (fastforce simp: not_idle_thread_def)
apply (simp add: pred_conj_def)
apply (strengthen refl[where t=True])
apply (wp cdl_get_ipc_buffer_None | simp)+
apply clarsimp
apply (drule lookup_ipc_buffer_SomeB_evalMonad)
apply clarsimp
apply (rule corres_symb_exec_l)
apply (rule_tac F = "rv = Some ba" in corres_gen_asm)
apply clarsimp
apply (rule corrupt_frame_include_self[where y = oid])
apply (rule corres_guard_imp)
apply (rule corres_split[OF set_register_corres])
unfolding K_bind_def
apply (rule_tac y = oid in corrupt_frame_include_self')
apply (rule corres_guard_imp)
apply (rule corres_split[OF dcorres_set_mrs])
unfolding K_bind_def
apply (rule set_message_info_corres)
apply (wp| simp add:not_idle_thread_def)+
apply (clarsimp simp:not_idle_thread_def)
apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def valid_pspace_def
ipc_frame_wp_at_def ipc_buffer_wp_at_def obj_at_def)
apply (clarsimp simp:cte_wp_at_cases obj_at_def)
apply (drule_tac s="cap.ArchObjectCap c" for c in sym)
apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def)
apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def cte_wp_at_cases)
apply (drule_tac s="cap.ArchObjectCap c" for c in sym)
apply simp
apply (wp get_ipc_buffer_noop, clarsimp)
apply fastforce
apply simp
apply (rule cdl_get_ipc_buffer_Some)
apply fastforce
apply (simp add:tcb_at_def not_idle_thread_def get_tcb_rev)+
apply wp
apply (rule evalMonad_wp)
apply (simp add:empty_when_fail_lookup_ipc_buffer weak_det_spec_lookup_ipc_buffer)+
apply (wp|clarsimp)+
done
lemma dcorres_set_intent_error:
"dcorres dc \<top>
(invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er
\<and> ko_at (TCB tcb) oid s) and not_idle_thread oid) (mark_tcb_intent_error oid er) (return a)"
apply (clarsimp simp:mark_tcb_intent_error_def bind_assoc
gets_the_def update_thread_def gets_def )
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp: not_idle_thread_def)
apply (frule ko_at_tcb_at)
apply (frule(1) tcb_at_is_etcb_at)
apply (clarsimp simp:tcb_at_def is_etcb_at_def, fold get_etcb_def)
apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def KHeap_D.set_object_def
simpler_modify_def corres_underlying_def)
apply (simp add:transform_def return_def)
apply (rule ext)
apply (clarsimp simp:transform_objects_def transform_tcb_def
dest!:get_tcb_SomeD get_etcb_SomeD)
apply (simp add:transform_full_intent_def Let_def obj_at_def)
done
lemma dcorres_when_r:
"\<lbrakk>R \<Longrightarrow> dcorres dc \<top> P l r; \<not> R \<Longrightarrow> dcorres dc \<top> Q l (return ())\<rbrakk>
\<Longrightarrow> dcorres dc \<top> (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not> R \<longrightarrow> Q s)) l (when R r)"
by (clarsimp simp:when_def)
lemma evalMonad_from_wp:
"\<lbrakk>evalMonad f s = Some a;\<lbrace>P\<rbrace>f\<lbrace> \<lambda>rv s. R rv\<rbrace>;P s;empty_when_fail f;\<And>Q. weak_det_spec Q f \<rbrakk>\<Longrightarrow> R a"
apply (clarsimp simp:evalMonad_def valid_def)
apply (drule_tac x = "(=) s" in meta_spec)
apply (fastforce simp:weak_det_spec_def empty_when_fail_def no_fail_def det_spec_def)
done
lemma empty_when_fail_get_mrs:
notes option.case_cong_weak [cong]
shows "empty_when_fail (get_mrs a b c)"
apply (clarsimp simp:get_mrs_def)
apply (rule empty_when_fail_compose)+
apply (simp add:empty_when_fail_return split:option.splits)+
apply (rule conjI)
apply clarsimp
apply (rule empty_when_fail_mapM)
apply (simp add:empty_when_fail_load_word_offs weak_det_spec_load_word_offs)
apply clarsimp
apply (rule empty_when_fail_mapM)
apply (simp add:empty_when_fail_load_word_offs weak_det_spec_load_word_offs)
apply (clarsimp simp:empty_when_fail_return weak_det_spec_simps split:option.splits)
apply (rule conjI)
apply clarsimp
apply (rule weak_det_spec_mapM)
apply (simp add:weak_det_spec_load_word_offs)
apply clarsimp
apply (rule weak_det_spec_mapM)