-
Notifications
You must be signed in to change notification settings - Fork 108
/
ADT_IF.thy
3472 lines (3058 loc) · 151 KB
/
ADT_IF.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
text \<open>
This file sets up a kernel automaton, ADT_A_if, which is
slightly different from ADT_A.
It then setups a big step framework to transfrom this automaton in the
big step automaton on which the infoflow theorem will be proved
\<close>
theory ADT_IF
imports
Noninterference_Base
Access.ArchSyscall_AC
Access.ArchADT_AC
ArchIRQMasks_IF
ArchScheduler_IF
ArchUserOp_IF
begin
section \<open>Generic big step automaton\<close>
inductive_set sub_big_steps ::
"('a,'b,'c) data_type \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'c list) set"
for A :: "('a,'b,'c) data_type" and R :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" and s :: "'a" where
nil: "\<lbrakk> evlist = []; t = s; \<not> R s s \<rbrakk>
\<Longrightarrow> (t,evlist) \<in> sub_big_steps A R s"
| step: "\<lbrakk> evlist = evlist' @ [e]; (s',evlist') \<in> sub_big_steps A R s; (s',t) \<in> Step A e; \<not> R s t \<rbrakk>
\<Longrightarrow> (t,evlist) \<in> sub_big_steps A R s"
text \<open>
Turn the (observable) multi-step executions of one automaton into the
steps of another. We call this second automaton a \emph{big step} automaton
of the first. We use a relation on observable states of the original
automaton to demarcate one big step from the next.
\<close>
inductive_set big_steps ::
"('a,'b,'c) data_type \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('c list \<Rightarrow> 'd) \<Rightarrow> ('d \<Rightarrow> ('a \<times> 'a) set)"
for A :: "('a,'b,'c) data_type" and R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and exmap :: "'c list \<Rightarrow> 'd" and ev :: "'d" where
cstep: "\<lbrakk> (s',as) \<in> sub_big_steps A R s; (s',t) \<in> Step A a; R s t; ev = exmap (as @ [a]) \<rbrakk>
\<Longrightarrow> (s,t) \<in> big_steps A R exmap ev"
definition big_step_adt ::
"('a,'b,'c) data_type \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('c list \<Rightarrow> 'd) \<Rightarrow> ('a,'b,'d) data_type" where
"big_step_adt A R exmap \<equiv> \<lparr>Init = Init A, Fin = Fin A, Step = big_steps A R exmap\<rparr>"
lemma system_Step_def_raw:
"system.Step = (\<lambda>A a. {(s,s'). s' \<in> execution A s [a]})"
apply (rule ext)
apply (rule ext)
apply (subst system.Step_def)
by (rule refl)
lemma big_stepsD:
"(s,t) \<in> big_steps A R exmap ev
\<Longrightarrow> \<exists>s' as a. (s',as) \<in> sub_big_steps A R s \<and> (s',t) \<in> Step A a \<and> R s t \<and> ev = exmap (as @ [a])"
apply (erule big_steps.induct)
apply blast
done
lemma big_stepsE:
assumes bs: "(s,t) \<in> big_steps A R exmap ev"
obtains s' as a where "(s',as) \<in> sub_big_steps A R s"
"(s',t) \<in> Step A a"
"R s t"
"ev = exmap (as @ [a])"
using bs[THEN big_stepsD] by blast
lemma Run_subset:
"(\<And>ev. Stepf ev \<subseteq> Stepf' ev) \<Longrightarrow> Run Stepf as \<subseteq> Run Stepf' as"
apply (induct as)
apply simp
apply auto
done
lemma rtranclp_def2:
"(R\<^sup>*\<^sup>* s0 s) = (R\<^sup>+\<^sup>+ s0 s \<or> s = s0)"
apply safe
apply (drule rtranclpD)
apply simp
apply (erule tranclp_into_rtranclp)
done
definition Fin_trancl where
"Fin_trancl A R s s' \<equiv> R\<^sup>+\<^sup>+ s s' \<or> Fin A s = Fin A s'"
text \<open>
A sufficient condition to show that the big steps of a big step ADT
terminate (i.e. that the relation R eventually becomes satisfied.)
\<close>
definition rel_terminate ::
"('a,'b,'c) data_type \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a set) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> nat) \<Rightarrow> bool" where
"rel_terminate A s0 R I measuref \<equiv>
(\<forall>s. s \<in> I \<and> (\<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s)
\<longrightarrow> (\<forall>as s'. (s',as) \<in> sub_big_steps A R s
\<longrightarrow> (\<forall>s'' a. (s',s'') \<in> Step A a
\<longrightarrow> (measuref s s'' < measuref s s') \<and>
(measuref s s' > 0 \<longrightarrow> measuref s s'' = 0 \<longrightarrow> R s s''))))"
lemma rel_terminateE:
assumes a: "rel_terminate A s0 R I measuref"
assumes b:
"\<lbrakk> (\<And>s s' as s'' a. \<lbrakk> s \<in> I; \<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s; (s',as) \<in> sub_big_steps A R s;
(s',s'') \<in> Step A a; measuref s s' > 0; measuref s s'' = 0 \<rbrakk>
\<Longrightarrow> R s s'');
(\<And>s s' as s'' a. \<lbrakk> s \<in> I; \<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s;
(s',as) \<in> sub_big_steps A R s; (s',s'') \<in> Step A a \<rbrakk>
\<Longrightarrow> measuref s s'' < measuref s s') \<rbrakk>
\<Longrightarrow> C"
shows "C"
using a b by (fastforce simp: rel_terminate_def)
lemma Run_big_steps_tranclp:
"(s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> R\<^sup>*\<^sup>* s0 s"
apply (induct js arbitrary: s rule: rev_induct)
apply simp
apply (fastforce dest: Run_mid elim: big_steps.cases)
done
lemma Step_system_reachable_trans:
"\<lbrakk> Step_system A s0; system.reachable A s0 s; system.reachable A s s' \<rbrakk>
\<Longrightarrow> system.reachable A s0 s'"
apply (clarsimp simp: system.reachable_def)
apply (rule Step_system.reachable_execution[simplified system.reachable_def])
apply blast+
done
lemma Step_system_reachable:
"\<lbrakk> Step_system A s0; system.reachable A s0 s \<rbrakk>
\<Longrightarrow> Step_system A s"
apply (subst Step_system_def)
apply (rule conjI)
apply (fastforce simp: system.reachable_def Step_system.execution_Run intro: exI[where x="[]"])
apply clarsimp
apply (frule Step_system_reachable_trans, assumption+)
apply (simp add: Step_system.execution_Run)
done
lemma Step_system_execution_Run_s0:
"Step_system A s0 \<Longrightarrow> execution A s0 as = {s'. (s0,s') \<in> Run (system.Step A) as}"
apply (rule Step_system.execution_Run, assumption)
apply (erule Step_system.reachable_s0)
done
text \<open>
Define a relation on states that is basically the inverse of the
Step relation for states @{term y} reachable from a given state @{term s}
before the next big step has finished.
\<close>
definition step_measuref_rel_from ::
"('a,'b,'c) data_type \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) set" where
"step_measuref_rel_from A R s \<equiv>
{(x,y). \<exists>a as. (y,x) \<in> Step A a \<and> (y,as) \<in> sub_big_steps A R s}"
lemma wf_step_measuref_rel_from:
"\<lbrakk> rel_terminate A s0 R I measuref; s \<in> I; \<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s \<rbrakk>
\<Longrightarrow> wf (step_measuref_rel_from A R s)"
apply (cut_tac wf_measure[where f="measuref s"])
apply (erule wf_subset)
apply (fastforce simp: measure_def inv_image_def step_measuref_rel_from_def rel_terminate_def)
done
lemma system_Step_one:
"(x, s') \<in> system.Step A a \<Longrightarrow> (x, s') \<in> Run (system.Step A) [a]"
by simp
definition inv_holds :: "('a,'b,'j) data_type \<Rightarrow> 'a set \<Rightarrow> bool" (infix "[>" 60) where
"D [> I \<equiv> (\<forall>j. Step D j `` I \<subseteq> I)"
lemma inv_holdsI:
"(\<forall>j. Step D j `` I \<subseteq> I) \<Longrightarrow> D [> I"
by (simp add: inv_holds_def)
lemma inv_holds_conjI:
"\<lbrakk> D [> P; D [> Q \<rbrakk> \<Longrightarrow> D [> P \<inter> Q"
by (simp add: inv_holds_def) blast
lemma inv_holds_steps:
assumes I: "A [> I"
assumes start_I: "B \<subseteq> I"
shows "steps (Simulation.Step A) B as \<subseteq> I"
apply clarsimp
apply (induct as rule: rev_induct)
apply (simp add: steps_def)
apply (rule set_mp)
apply (rule start_I)
apply simp
apply (simp add: steps_def)
apply (erule ImageE)
apply (drule_tac x=xb in meta_spec)
apply simp
apply (rule set_mp)
apply (rule I[simplified inv_holds_def,rule_format])
apply (rule ImageI)
apply assumption
apply simp
done
locale serial_system_weak = system +
fixes I
assumes I: "A [> I"
assumes serial: "\<And>s' a. s' \<in> I \<Longrightarrow> (\<exists>t. (s', t) \<in> data_type.Step A a)"
begin
lemma step_serial:
assumes nonempty_start: "B \<noteq> {}"
assumes invariant_start: "B \<subseteq> I"
shows "steps (Simulation.Step A) B as \<noteq> {}"
apply (induct as rule: rev_induct)
apply (simp add: steps_def nonempty_start)
apply (erule nonemptyE)
apply (frule set_mp[OF inv_holds_steps[OF I invariant_start]])
apply (frule_tac a=x in serial)
apply (elim exE)
apply (rule_tac x=t in notemptyI)
apply (fastforce simp: steps_def)
done
end
lemma sub_big_steps_I_holds:
"\<lbrakk> A [> I; s \<in> I; (x, xs) \<in> sub_big_steps A R s \<rbrakk>
\<Longrightarrow> x \<in> I"
apply (erule sub_big_steps.induct)
apply simp
apply (simp add: inv_holds_def)
apply blast
done
lemma rel_terminate_terminates:
assumes ss: "serial_system_weak A I"
assumes rt: "rel_terminate A s0 R I measuref"
assumes si: "s \<in> I"
assumes sR: "\<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s"
shows "\<forall>js. (x,js) \<in> sub_big_steps A R s
\<longrightarrow> (\<exists>as s' a s''. (s',(js@as)) \<in> sub_big_steps A R s \<and>
(s',s'') \<in> Step A a \<and> R s s'')"
proof -
show ?thesis
apply (induct x rule: wf_induct)
apply (rule wf_step_measuref_rel_from[OF rt si sR])
apply clarsimp
apply (frule sub_big_steps_I_holds[OF ss[THEN serial_system_weak.I] si])
apply (frule_tac serial_system_weak.serial[OF ss])
apply (erule exE, rename_tac s')
apply (drule_tac x=s' in spec)
apply (erule impE)
apply (fastforce simp: step_measuref_rel_from_def)
apply (case_tac "R s s'")
apply (rule_tac x="[]" in exI)
apply (rule_tac x=x in exI)
apply fastforce
apply (fastforce intro: sub_big_steps.step)
done
qed
lemma sub_big_steps_nrefl:
"(\<And>s. \<not> R s s) \<Longrightarrow> (s,[]) \<in> sub_big_steps A R s"
by (blast intro: nil)
lemma big_steps_enabled:
assumes ss: "serial_system_weak A I"
assumes rt: "rel_terminate A s0 R I measuref"
assumes s_I: "s \<in> I"
assumes nrefl: "\<And>s. \<not> R s s"
shows "\<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s \<Longrightarrow> \<exists>x s'. (s, s') \<in> big_steps A R exmap x"
apply (frule rel_terminate_terminates[OF ss rt s_I])
apply (drule_tac x="[]" in spec)
apply (erule impE[OF _ sub_big_steps_nrefl])
apply (rule nrefl)
apply (fastforce intro: cstep)
done
text \<open>
We assume here that there is only one event that can ever occur. This
is overly restrictive in general, but should be fine for the seL4
automata (which shouldn't need multiple event labels since it should only
ever be able to perform one event in each state).
\<close>
lemma Step_system_to_enabled_system:
assumes single_event: "(\<forall>(x::'b) (y::'b). x = y)"
assumes st: "Step_system A s0"
assumes en: "\<And>s. system.reachable A s0 s \<Longrightarrow> \<exists>(x::'b) s'. (s,s') \<in> system.Step A x"
shows "enabled_system A s0"
apply (clarsimp simp: enabled_system_def)
proof -
fix s js jsa
assume a: "s \<in> execution A s0 js"
show "\<exists>s'. s' \<in> execution A s jsa"
proof -
have er: "\<And>as. execution A s as = {s'. (s,s') \<in> Run (system.Step A) as}"
apply (rule Step_system.execution_Run[OF st])
using a apply (fastforce simp: system.reachable_def)
done
show ?thesis
apply (induct jsa rule: rev_induct)
apply (simp add: er)
apply (clarsimp simp: er)
apply (cut_tac s=s' in en)
apply (rule Step_system.reachable_execution[OF st])
using a apply (fastforce simp: system.reachable_def)
apply (simp add: er)
apply clarify
apply (rename_tac b s'a)
apply (rule_tac x=s'a in exI)
apply (rule Run_trans, assumption)
apply (rule system_Step_one)
apply (cut_tac x=b and xa=x in single_event[rule_format], simp)
done
qed
qed
lemma steps_subset:
"A \<subseteq> B \<Longrightarrow> steps steps1 A as \<subseteq> steps steps1 B as"
apply (simp add: steps_def Image_def)
apply (induct as rule: rev_induct)
apply simp
apply force
done
locale Init_Fin_serial_weak = serial_system_weak +
assumes Init_Fin: "\<And>s'. s' \<in> I \<Longrightarrow> s' \<in> Init A (Fin A s')"
assumes s0_I: "Init A s0 \<subseteq> I"
begin
lemma enabled:
"enabled_system A s0"
supply image_cong_simp[cong del]
supply ex_image_cong_iff [simp del]
apply (clarsimp simp: enabled_system_def)
apply (rename_tac jsa, induct_tac jsa rule: rev_induct)
apply (clarsimp simp: execution_def steps_def)
apply (fold steps_def)
apply (rule_tac x="Fin A x" in exI)
apply (rule imageI)
apply (rule Init_Fin)
apply (rule set_mp)
apply (rule inv_holds_steps[OF I])
apply (rule s0_I)
apply simp
apply (clarsimp simp: execution_def steps_def)
apply (fold steps_def)
apply (subgoal_tac "steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {}")
apply (erule nonemptyE)
apply clarsimp
apply (drule_tac a=x in serial)
apply clarsimp
apply (rule_tac x="Fin A t" in exI)
apply (rule imageI)
apply (rule ImageI)
apply assumption
apply assumption
apply (cut_tac inv_holds_steps[OF I s0_I])
apply (drule (1) subsetD)
apply (cut_tac B="{xa}" and as=xs in inv_holds_steps[OF I])
apply simp
apply (cut_tac B="{xa}" and as=xs in step_serial)
apply simp+
apply (cut_tac A="{xa}" and B="Init A (Fin A xa)" in steps_subset)
apply (simp add: Init_Fin)
apply force
done
end
lemma invariant_holds_steps:
assumes I: "A \<Turnstile> I"
assumes start_I: "B \<subseteq> I"
shows "steps (Simulation.Step A) B as \<subseteq> I"
apply clarsimp
apply (induct as rule: rev_induct)
apply (simp add: steps_def)
apply (rule set_mp)
apply (rule start_I)
apply simp
apply (simp add: steps_def)
apply (erule ImageE)
apply (drule_tac x=xb in meta_spec)
apply simp
apply (rule set_mp)
apply (rule I[simplified invariant_holds_def, THEN conjunct2,rule_format])
apply (rule ImageI)
apply assumption
apply simp
done
locale serial_system = system +
fixes I
assumes I: "A \<Turnstile> I"
assumes serial: "\<And>s' a. s' \<in> I \<Longrightarrow> (\<exists>t. (s', t) \<in> data_type.Step A a)"
begin
lemma step_serial:
assumes nonempty_start: "B \<noteq> {}"
assumes invariant_start: "B \<subseteq> I"
shows "steps (Simulation.Step A) B as \<noteq> {}"
apply (induct as rule: rev_induct)
apply (simp add: steps_def nonempty_start)
apply (erule nonemptyE)
apply (frule set_mp[OF invariant_holds_steps[OF I invariant_start]])
apply (frule_tac a=x in serial)
apply (elim exE)
apply (rule_tac x=t in notemptyI)
apply (fastforce simp: steps_def)
done
lemma fw_sim_serial:
assumes refines: "LI B A R (I_b \<times> I_a)"
assumes B_I_b: "B \<Turnstile> I_b'"
assumes A_I_as: "I \<subseteq> I_a"
assumes B_I_bs': "I_b' \<subseteq> I_b"
assumes constrained_B: "\<And>s. s \<in> I_b' \<Longrightarrow> \<exists>s'. s' \<in> I \<and> (s,s') \<in> R"
shows "serial_system B I_b'"
apply unfold_locales
apply (rule B_I_b)
apply (insert refines)
apply (clarsimp simp: LI_def)
apply (drule_tac x=a in spec)
apply (frule_tac s=s' in constrained_B)
apply clarsimp
apply (frule_tac a=a in serial)
apply (clarsimp simp: rel_semi_def)
apply (cut_tac B_I_bs' A_I_as)
apply blast
done
end
locale Init_Fin_serial = serial_system +
assumes Init_Fin: "\<And>s'. s' \<in> I \<Longrightarrow> s' \<in> Init A (Fin A s')"
assumes s0_I: "Init A s0 \<subseteq> I"
begin
lemma enabled:
"enabled_system A s0"
supply image_cong_simp [cong del]
supply ex_image_cong_iff [simp del]
apply (clarsimp simp: enabled_system_def)
apply (induct_tac jsa rule: rev_induct)
apply (clarsimp simp: execution_def steps_def)
apply (fold steps_def)
apply (rule_tac x="Fin A x" in exI)
apply (rule imageI)
apply (rule Init_Fin)
apply (rule set_mp)
apply (rule invariant_holds_steps[OF I])
apply (rule s0_I)
apply simp
apply (clarsimp simp: execution_def steps_def)
apply (fold steps_def)
apply (subgoal_tac "xb \<in> I")
apply (drule_tac a=x in serial)
apply clarsimp
apply (rule_tac x="Fin A t" in exI)
apply (rule imageI)
apply (rule ImageI)
apply assumption
apply assumption
apply (rule set_mp)
apply (rule invariant_holds_steps[OF I])
prefer 2
apply assumption
apply (rule I[simplified invariant_holds_def, THEN conjunct1,rule_format])
done
end
sublocale Init_Fin_serial \<subseteq> enabled_system by (rule enabled)
sublocale Init_Fin_serial \<subseteq> Init_Fin_serial_weak
using I by unfold_locales (auto simp add: inv_holds_def invariant_holds_def elim: serial Init_Fin)
lemma (in Init_Fin_serial) serial_to_weak:
"Init_Fin_serial_weak A s0 I"
by intro_locales
definition inv_from_rel :: "('a, 'b, 'j) data_type \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set" where
"inv_from_rel A s0 R \<equiv> {s. \<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s}"
lemma big_step_adt_R_tranclp_inv:
"big_step_adt C R exmap [> inv_from_rel C s0 R"
apply (rule inv_holdsI)
apply (clarsimp simp: big_step_adt_def inv_from_rel_def Fin_trancl_def)
apply (rule_tac x="s0'" in bexI)
apply (force elim: big_steps.cases)
apply simp
done
lemma big_steps_I_holds:
"\<lbrakk> (xa, x) \<in> big_steps A R exmap j; xa \<in> I; A [> I \<rbrakk>
\<Longrightarrow> x \<in> I"
apply (erule big_stepsE)
apply (frule sub_big_steps_I_holds, assumption+)
apply (simp add: inv_holds_def)
apply blast
done
lemma big_step_adt_inv_holds:
"A [> I \<Longrightarrow> big_step_adt A R exmap [> I"
apply (simp add: big_step_adt_def inv_holds_def)
apply clarsimp
apply (rule big_steps_I_holds, assumption+)
apply (simp add: inv_holds_def)
done
lemma big_step_adt_Init_Fin_serial_weak:
assumes single_event: "\<forall>(x::'b) (y::'b). x = y"
assumes nrefl: "\<And>s. \<not> R s s"
assumes ifsw: "Init_Fin_serial_weak A s0 I"
assumes rt: "rel_terminate A s0 R I measuref"
assumes J_def: "J = inv_from_rel A s0 R \<inter> I"
shows "Init_Fin_serial_weak (big_step_adt A R (exmap::('a list \<Rightarrow> 'b))) s0 J"
using ifsw
apply (unfold_locales)
apply (simp add: J_def)
apply (rule inv_holds_conjI)
apply (rule big_step_adt_R_tranclp_inv)
apply (rule big_step_adt_inv_holds)
apply (simp add: Init_Fin_serial_weak_def serial_system_weak.I)
apply (simp add: big_step_adt_def J_def inv_from_rel_def)
apply (elim conjE exE)
apply (cut_tac s=s' and I=I and exmap=exmap in big_steps_enabled)
apply (force simp: Init_Fin_serial_weak_def)
apply (rule rt)
apply assumption
apply (simp add: nrefl)
apply simp
apply clarsimp
apply (cut_tac x=x and xa=a in single_event[rule_format])
apply blast
apply (simp add: J_def big_step_adt_def Init_Fin_serial_weak.Init_Fin)
apply (simp add: big_step_adt_def Init_Fin_serial_weak.s0_I J_def inv_from_rel_def, force)
done
lemma big_step_adt_enabled_system:
assumes single_event: "\<forall>(x::'b) (y::'b). x = y"
assumes nrefl: "\<And>s. \<not> R s s"
assumes ifsw: "Init_Fin_serial_weak A s0 I"
assumes rt: "rel_terminate A s0 R I measuref"
shows "enabled_system (big_step_adt A R (exmap::('a list \<Rightarrow> 'b))) s0"
apply (cut_tac big_step_adt_Init_Fin_serial_weak[OF single_event nrefl ifsw rt])
apply (erule Init_Fin_serial_weak.enabled)
apply simp
done
(* For reachability in big_step_adt we need to consider internal reachability. *)
definition reachable_i where
"reachable_i A s0 s \<equiv> \<exists>js. (s0, s) \<in> Run (Step A) js"
lemma sub_big_steps_Run:
"(t,evlist) \<in> sub_big_steps A R s \<Longrightarrow> (s, t) \<in> Run (Step A) evlist \<and> \<not> R s t"
apply (induct t evlist rule: sub_big_steps.induct)
apply simp
apply clarsimp
apply (rule Run_trans)
apply assumption
apply simp
done
lemma big_step_adt_reachable_i_states:
"(s0, s) \<in> Run (Step (big_step_adt C R exmap)) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js"
apply (induct js arbitrary: s0)
apply (rule_tac x="[]" in exI, simp)
apply (clarsimp simp: big_step_adt_def)
apply (rename_tac s0 sa)
apply (erule big_stepsE)
apply (drule sub_big_steps_Run)
apply (subgoal_tac "(s0,sa) \<in> Run (data_type.Step C) (as@[aa])")
apply (blast intro: Run_trans)
apply (fastforce intro: Run_trans)
done
lemma reachable_i_big_step_adt:
"reachable_i (big_step_adt C R exmap) s0 s \<Longrightarrow> reachable_i C s0 s"
apply (clarsimp simp: reachable_i_def)
apply (blast intro: big_step_adt_reachable_i_states)
done
lemma steps_eq_Run:
"(s' \<in> steps (Step A) (Init A s0) js) =
(\<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js)"
apply (rule iffI)
apply (clarsimp simp: steps_def image_def Image_def)
apply (induct js arbitrary: s' rule: rev_induct)
apply simp
apply (force intro: Run_trans)
apply (clarsimp simp: steps_def image_def Image_def)
apply (induct js arbitrary: s' rule: rev_induct)
apply simp
apply clarsimp
apply (drule Run_mid, force)
done
lemma reachable_reachable_i:
"system.reachable A s0 s \<Longrightarrow> \<exists>s0' s'. s0' \<in> Init A s0 \<and> Fin A s' = s \<and> reachable_i A s0' s'"
by (force simp: system.reachable_def reachable_i_def execution_def steps_eq_Run)
lemma reachable_i_reachable:
"\<lbrakk> reachable_i A s0' s'; s0' \<in> Init A s0; Fin A s' = s \<rbrakk>
\<Longrightarrow> system.reachable A s0 s"
by (force simp: system.reachable_def reachable_i_def execution_def steps_eq_Run)
lemma reachable_big_step_adt:
"system.reachable (big_step_adt C R exmap) s0 s
\<Longrightarrow> system.reachable C s0 s"
by (force dest: reachable_reachable_i
intro: reachable_i_reachable reachable_i_big_step_adt
simp: big_step_adt_def)
lemma big_step_adt_Init_inv_Fin_system:
"Init_inv_Fin_system A s0 \<Longrightarrow> Init_inv_Fin_system (big_step_adt A R exmap) s0"
apply (clarsimp simp: Init_inv_Fin_system_def big_step_adt_def)
apply (erule_tac x=s in allE)
apply (force intro: reachable_big_step_adt simp: big_step_adt_def)
done
lemma big_step_adt_Step_system:
"Init_inv_Fin_system C s0 \<Longrightarrow> Step_system (big_step_adt C R exmap) s0"
apply (rule Init_Fin_system_Step_system)
apply (rule Init_inv_Fin_system_Init_Fin_system)
apply (rule big_step_adt_Init_inv_Fin_system)
apply simp
done
lemma big_step_adt_enabled_Step_system:
assumes single_event: "\<forall>(x::'b) (y::'b). x = y"
assumes nrefl: "\<And>s. \<not> R s s"
assumes ifsw: "Init_Fin_serial_weak A s0 I"
assumes iifs: "Init_inv_Fin_system A s0"
assumes rt: "rel_terminate A s0 R I measuref"
shows "enabled_Step_system (big_step_adt A R (examp::('a list \<Rightarrow> 'b))) s0"
using assms
by (simp add: enabled_Step_system_def big_step_adt_Step_system big_step_adt_enabled_system)
section \<open>ADT_A_if definition and enabledness\<close>
subsection \<open>global_automaton_if definition\<close>
text \<open>
We define a bunch of states that the system can be in. The first two
are when the processor is in user mode, the final four are for when in
kernel mode.
- in user mode (a user-level thread is running)
- in idle mode (the idle thread is running)
- kernel entry for some event e (kernel entry is occurring)
- in kernel mode where kernel execution has been pre-empted by interrupt
arrival
- in kernel mode where the scheduler is about to execute -- the boolean here
is ghost state to capture when the schedule event follows interrupt-handling
(i.e. is True when the previous mode was KernelEntry Interrupt or KernelPreempted)
- in kernel mode, about to exit to userspace
\<close>
datatype sys_mode = InUserMode | InIdleMode |
KernelEntry event | KernelPreempted |
KernelSchedule bool | KernelExit
type_synonym 'k global_sys_state = "(user_context \<times> 'k) \<times> sys_mode"
text \<open>
We take the @{term global_automaton} and split the kernel transitions
into multiple steps. This is done because, while the entire execution
from kernel entry to exit is atomic, different parts of it need to be
considered as being done on behalf of different domains. For instance,
the part that does kernel entry and then handles the event should happen
on behalf of the domain of the currently running thread, but the
part that handles pre-emptions will probably need to purport to happen on
behalf of the scheduler domain.
- a transition for kernel entry on event e (kernel entry happens,
and we handle the event, possibly gettting pre-empted along the way)
- a transition for handling those pre-emptions
- a transition for running the scheduler at the end of every kernel event
- a transition for kernel exit
TODO: schedule and kernel exit may be able to be put into the same
transition. It depends on what domain each transition needs to
purport to run on behalf of
We also have the user operations possibly give an event, which gives us
a handle on modelling when user programs request system calls or cause
other exceptions to occur.
\<close>
definition global_automaton_if ::
"((user_context \<times> 'k) \<times> irq option \<times> (user_context \<times> 'k)) set
\<Rightarrow> ((user_context \<times> 'k) \<times> event option \<times> (user_context \<times> 'k)) set
\<Rightarrow> (event \<Rightarrow> ((user_context \<times> 'k) \<times> bool \<times> (user_context \<times> 'k)) set)
\<Rightarrow> (((user_context \<times> 'k) \<times> unit \<times> (user_context \<times> 'k)) set)
\<Rightarrow> (((user_context \<times> 'k) \<times> unit \<times> (user_context \<times> 'k)) set)
\<Rightarrow> (((user_context \<times> 'k) \<times> sys_mode \<times> (user_context \<times> 'k)) set)
\<Rightarrow> ('k global_sys_state \<times> 'k global_sys_state) set" where
"global_automaton_if get_active_irqf do_user_opf kernel_callf preemptionf schedulef kernel_exitf \<equiv>
\<comment> \<open>Kernel entry with preemption during event handling
NOTE: kernel cannot be preempted while servicing an interrupt\<close>
{((s, KernelEntry e),
(s', KernelPreempted)) | s s' e. (s, True, s') \<in> kernel_callf e \<and> e \<noteq> Interrupt} \<union>
\<comment> \<open>kernel entry without preemption during event handling\<close>
{((s, KernelEntry e),
(s', KernelSchedule (e = Interrupt))) | s s' e. (s, False, s') \<in> kernel_callf e } \<union>
\<comment> \<open>handle in-kernel preemption\<close>
{((s, KernelPreempted), (s', KernelSchedule True)) | s s'. (s, (), s') \<in> preemptionf } \<union>
\<comment> \<open>schedule\<close>
{((s, KernelSchedule b), (s', KernelExit)) | s s' b. (s, (), s') \<in> schedulef } \<union>
\<comment> \<open>kernel exit\<close>
{((s, KernelExit), (s', m)) | s s' m. (s, m, s') \<in> kernel_exitf } \<union>
\<comment> \<open>User runs, causes exception\<close>
{((s, InUserMode), (s', KernelEntry e)) | s s_aux s' e. (s, None, s_aux) \<in> get_active_irqf \<and>
(s_aux, Some e, s') \<in> do_user_opf \<and>
e \<noteq> Interrupt} \<union>
\<comment> \<open>User runs, no exception happens\<close>
{((s, InUserMode), (s', InUserMode) ) | s s_aux s'. (s, None, s_aux) \<in> get_active_irqf \<and>
(s_aux, None, s') \<in> do_user_opf} \<union>
\<comment> \<open>Interrupt while in user mode\<close>
{((s, InUserMode), (s', KernelEntry Interrupt)) | s s' i. (s, Some i, s') \<in> get_active_irqf} \<union>
\<comment> \<open>Interrupt while in idle mode\<close>
{((s, InIdleMode), (s', KernelEntry Interrupt)) | s s' i. (s, Some i, s') \<in> get_active_irqf} \<union>
\<comment> \<open>No interrupt while in idle mode\<close>
{((s, InIdleMode), (s', InIdleMode)) | s s'. (s, None, s') \<in> get_active_irqf}"
subsection \<open>do_user_op_if\<close>
definition do_user_op_A_if ::
"user_transition_if
\<Rightarrow> ((user_context \<times> det_state) \<times> event option \<times> (user_context \<times> det_state)) set" where
"do_user_op_A_if uop \<equiv>
{(s,e,(tc,s'))| s e tc s'. ((e,tc),s') \<in> fst (split (do_user_op_if uop) s)}"
lemma no_irq_user_memory_update[simp]:
"no_irq (user_memory_update a)"
by (wpsimp simp: no_irq_def user_memory_update_def)
lemma no_irq_device_memory_update[simp]:
"no_irq (device_memory_update a)"
by (wpsimp simp: no_irq_def device_memory_update_def)
subsection \<open>kernel_entry_if\<close>
text \<open>
Enter the kernel, and handle the event. Leave the user context
unchanged; although it shouldn't matter really what its value is
while we are still in kernel mode.
\<close>
definition kernel_entry_if ::
"event \<Rightarrow> user_context \<Rightarrow> (((unit + unit) \<times> user_context),det_ext) s_monad" where
"kernel_entry_if e tc \<equiv>
do t \<leftarrow> gets cur_thread;
thread_set (\<lambda>tcb. tcb \<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r \<leftarrow> handle_event e;
return (r,tc)
od"
crunch kernel_entry_if
for cur_domain[wp]: "\<lambda>s. P (cur_domain s)"
crunch kernel_entry_if
for idle_thread[wp]: "\<lambda>s::det_state. P (idle_thread s)"
crunch kernel_entry_if
for cur_thread[wp]: "\<lambda>s::det_state. P (cur_thread s)"
lemma thread_set_tcb_context_update_ct_active[wp]:
"thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>ct_active\<rbrace>"
apply (simp add: thread_set_def ct_in_state_def | wp set_object_wp)+
apply (clarsimp simp: st_tcb_at_def obj_at_def get_tcb_def)
done
lemma thread_set_tcb_context_update_not_ct_active[wp]:
"thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>s. \<not> ct_active s\<rbrace>"
apply (simp add: thread_set_def ct_in_state_def | wp set_object_wp)+
apply (clarsimp simp: st_tcb_at_def obj_at_def get_tcb_def
split: kernel_object.splits option.splits)
done
lemma kernel_entry_if_invs:
"\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. invs\<rbrace>"
unfolding kernel_entry_if_def
by (wpsimp wp: thread_set_invs_trivial hoare_weak_lift_imp
simp: arch_tcb_update_aux2 ran_tcb_cap_cases)+
lemma kernel_entry_if_globals_equiv:
"\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st
and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (simp add: kernel_entry_if_def)
apply (wp hoare_weak_lift_imp handle_event_globals_equiv
thread_set_invs_trivial thread_set_context_globals_equiv
| simp add: ran_tcb_cap_cases arch_tcb_update_aux2)+
apply (clarsimp simp: cur_thread_idle)
done
lemma thread_set_tcb_context_update_neg_cte_wp_at[wp]:
"thread_set (tcb_arch_update f) t \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_wp get_object_wp | simp)+
apply (case_tac "t = fst slot")
apply (clarsimp split: kernel_object.splits)
apply (erule notE)
apply (erule cte_wp_atE)
apply (fastforce simp: obj_at_def)
apply (drule get_tcb_SomeD)
apply (rule cte_wp_at_tcbI)
apply (simp)
apply assumption
apply (fastforce simp: tcb_cap_cases_def split: if_splits)
apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
lemma thread_set_tcb_context_update_domain_sep_inv[wp]:
"thread_set (tcb_arch_update f) t \<lbrace>domain_sep_inv irqs st\<rbrace>"
by (wp domain_sep_inv_triv)
lemma kernel_entry_silc_inv[wp]:
"\<lbrace>silc_inv aag st and einvs and simple_sched_action and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)
and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))
and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
kernel_entry_if ev tc
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding kernel_entry_if_def
by (wpsimp simp: ran_tcb_cap_cases arch_tcb_update_aux2
wp: hoare_weak_lift_imp handle_event_silc_inv thread_set_silc_inv thread_set_invs_trivial
thread_set_not_state_valid_sched thread_set_pas_refined
| wp (once) hoare_vcg_imp_lift | force)+
subsection \<open>handle_preemption_if\<close>
text \<open>
Since this executes entirely in kernel mode, leave the
user context unchanged
\<close>
definition handle_preemption_if :: "user_context \<Rightarrow> (user_context,det_ext) s_monad" where
"handle_preemption_if tc \<equiv>
do irq \<leftarrow> do_machine_op (getActiveIRQ True);
when (irq \<noteq> None) $ handle_interrupt (the irq);
return tc
od"
subsection \<open>schedule_if\<close>
text \<open>
Since this executes entirely in kernel mode, leave the
user context unchanged
\<close>
definition schedule_if :: "user_context \<Rightarrow> (user_context,det_ext) s_monad" where
"schedule_if tc \<equiv>
do schedule;
activate_thread;
return tc
od"
crunch schedule_if
for silc_inv[wp]: "silc_inv aag st"
crunch schedule_if
for domain_sep_inv[wp]: "\<lambda>s :: det_state. domain_sep_inv irqs st s"
crunch activate_thread
for idle_thread[wp]: "\<lambda>s :: det_state. P (idle_thread s)"
crunch activate_thread
for cur_domain[wp]: "\<lambda>s. P (cur_domain s)"
function (domintros) next_irq_state :: "nat \<Rightarrow> (irq \<Rightarrow> bool) \<Rightarrow> nat" where
"next_irq_state cur masks =
(if irq_at cur masks = None then next_irq_state (Suc cur) masks else cur)"
by (pat_completeness, auto)
definition irq_measure_if where
"irq_measure_if s \<equiv> let cur = Suc (irq_state (machine_state s))
in (next_irq_state cur (irq_masks (machine_state s))) - cur"
definition irq_measure_if_inv where
"irq_measure_if_inv st s \<equiv> irq_measure_if (s::det_state) \<le> irq_measure_if (st::det_state)"
definition irq_state_inv where
"irq_state_inv (st :: det_state) (s :: det_state) \<equiv>
irq_state (machine_state s) \<ge> irq_state (machine_state st) \<and>
irq_masks (machine_state s) = irq_masks (machine_state st) \<and>
next_irq_state (Suc (irq_state (machine_state s))) (irq_masks (machine_state s)) =
next_irq_state (Suc (irq_state (machine_state st))) (irq_masks (machine_state s))"
definition irq_state_next where
"irq_state_next (st :: det_state) (s :: det_state) \<equiv>
irq_state (machine_state s) \<ge> irq_state (machine_state st) \<and>
irq_masks (machine_state s) = irq_masks (machine_state st) \<and>
irq_state (machine_state s) = next_irq_state (Suc (irq_state (machine_state st)))
(irq_masks (machine_state s))"
locale ADT_IF_1 =
fixes initial_aag :: "'a subject_label PAS"
assumes do_user_op_if_invs[wp]:
"do_user_op_if uop tc \<lbrace>invs and ct_running :: det_state \<Rightarrow> bool\<rbrace>"
and do_user_op_if_domain_sep_inv[wp]:
"do_user_op_if uop tc \<lbrace>\<lambda>s. domain_sep_inv irqs (st :: det_state) (s :: det_state)\<rbrace>"
and do_user_op_if_valid_sched[wp]:
"do_user_op_if uop tc \<lbrace>valid_sched\<rbrace>"
and do_user_op_if_irq_masks[wp]:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>"
and do_user_op_if_valid_list[wp]:
"do_user_op_if uop tc \<lbrace>valid_list\<rbrace>"
and do_user_op_if_scheduler_action[wp]:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>"
and do_user_op_silc_inv[wp]:
"do_user_op_if uop tc \<lbrace>silc_inv (aag :: 'a subject_label PAS) st\<rbrace>"
and do_user_op_pas_refined[wp]:
"do_user_op_if uop tc \<lbrace>pas_refined aag\<rbrace>"
and do_user_op_cur_thread[wp]:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s :: det_state. P (cur_thread s)\<rbrace>"
and do_user_op_cur_domain[wp]:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>"
and do_user_op_idle_thread[wp]:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s :: det_state. P (idle_thread s)\<rbrace>"
and do_user_op_domain_fields[wp]:
"\<And>P. do_user_op_if uop tc \<lbrace>domain_fields P\<rbrace>"
and do_use_op_guarded_pas_domain[wp]:
"do_user_op_if uop tc \<lbrace>guarded_pas_domain aag\<rbrace>"
and tcb_arch_ref_tcb_context_set[simp]:
"tcb_arch_ref (tcb_arch_update (arch_tcb_context_set uc) tcb) = tcb_arch_ref tcb"
and arch_switch_to_idle_thread_pspace_aligned[wp]:
"arch_switch_to_idle_thread \<lbrace>\<lambda>s :: det_ext state. pspace_aligned s\<rbrace>"
and arch_switch_to_idle_thread_valid_vspace_objs[wp]:
"arch_switch_to_idle_thread \<lbrace>\<lambda>s :: det_ext state. valid_vspace_objs s\<rbrace>"
and arch_switch_to_idle_thread_valid_arch_state[wp]:
"arch_switch_to_idle_thread \<lbrace>\<lambda>s :: det_ext state. valid_arch_state s\<rbrace>"
and arch_switch_to_thread_pspace_aligned[wp]:
"arch_switch_to_thread t \<lbrace>\<lambda>s :: det_ext state. pspace_aligned s\<rbrace>"
and arch_switch_to_thread_valid_vspace_objs[wp]:
"arch_switch_to_thread t \<lbrace>\<lambda>s :: det_ext state. valid_vspace_objs s\<rbrace>"
and arch_switch_to_thread_valid_arch_state[wp]:
"arch_switch_to_thread t \<lbrace>\<lambda>s :: det_ext state. valid_arch_state s\<rbrace>"
and arch_switch_to_thread_cur_thread[wp]:
"\<And>P. arch_switch_to_thread t \<lbrace>\<lambda>s :: det_state. P (cur_thread s)\<rbrace>"
and arch_activate_idle_thread_cur_thread[wp]:
"\<And>P. arch_activate_idle_thread t \<lbrace>\<lambda>s :: det_state. P (cur_thread s)\<rbrace>"
and arch_activate_idle_thread_scheduler_action[wp]:
"\<And>P. arch_activate_idle_thread t \<lbrace>\<lambda>s :: det_state. P (scheduler_action s)\<rbrace>"
and handle_vm_fault_domain_fields[wp]:
"\<And>P. handle_vm_fault t vmft \<lbrace>domain_fields P\<rbrace>"
and handle_hypervisor_fault_domain_fields[wp]:
"\<And>P. handle_hypervisor_fault t hft \<lbrace>domain_fields P\<rbrace>"
and arch_perform_invocation_noErr[wp]:
"\<And>Q. \<lbrace>\<top>\<rbrace> arch_perform_invocation i -, \<lbrace>\<lambda>rv s :: det_state. Q rv s\<rbrace>"
and arch_invoke_irq_control_noErr[wp]:
"\<And>Q. \<lbrace>\<top>\<rbrace> arch_invoke_irq_control ici -, \<lbrace>\<lambda>rv s :: det_state. Q rv s\<rbrace>"
and init_arch_objects_irq_state_of_state[wp]:
"\<And>P. init_arch_objects new_type dev ptr num_objects obj_sz refs \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>"
and getActiveIRQ_None:
"(None, s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) (s :: det_state))
\<Longrightarrow> irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = None"
and getActiveIRQ_Some:
"(Some irq, s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s)
\<Longrightarrow> irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = Some irq"
and kernel_entry_if_idle_equiv:
"\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st
and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. idle_equiv st\<rbrace>"
and handle_preemption_idle_equiv[wp]:
"\<lbrace>idle_equiv st and invs\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. idle_equiv st\<rbrace>"
and schedule_if_idle_equiv[wp]:
"\<lbrace>idle_equiv st and invs\<rbrace> schedule_if tc \<lbrace>\<lambda>_. idle_equiv st\<rbrace>"
and do_user_op_if_idle_equiv[wp]:
"\<lbrace>idle_equiv st and invs\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>_. idle_equiv st\<rbrace>"
and kernel_entry_if_valid_vspace_objs_if[wp]:
"\<lbrace>valid_vspace_objs_if and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. valid_vspace_objs_if\<rbrace>"
and handle_preemption_if_valid_pdpt_objs[wp]:
"handle_preemption_if tc \<lbrace>\<lambda>s. valid_vspace_objs_if s\<rbrace>"
and schedule_if_valid_pdpt_objs[wp]:
"schedule_if tc \<lbrace>\<lambda>s. valid_vspace_objs_if s\<rbrace>"
and do_user_op_if_valid_pdpt_objs[wp]:
"do_user_op_if uop tc \<lbrace>\<lambda>s :: det_state. valid_vspace_objs_if s\<rbrace>"
and valid_vspace_objs_if_ms_update[simp]:
"\<And>f. valid_vspace_objs_if (machine_state_update f s) = valid_vspace_objs_if s"
and do_user_op_if_irq_state_of_state:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>"
and do_user_op_if_irq_masks_of_state:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>"
and do_user_op_if_irq_measure_if:
"\<And>P. do_user_op_if uop tc \<lbrace>\<lambda>s :: det_state. P (irq_measure_if s)\<rbrace>"
and invoke_tcb_irq_state_inv:
"\<lbrace>(\<lambda>s. irq_state_inv st s) and domain_sep_inv False (sta :: det_state)
and tcb_inv_wf tinv and K (irq_is_recurring irq st)\<rbrace>