1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(NICTA_GPL)
9 *)
10
11theory ADT_IF_Refine
12imports "InfoFlow.ADT_IF" "Refine.EmptyFail_H"
13begin
14
15context begin interpretation Arch . (*FIXME: arch_split*)
16
17definition
18  kernelEntry_if
19where
20  "kernelEntry_if e tc \<equiv> do
21    t \<leftarrow> getCurThread;
22    threadSet (tcbArch_update (atcbContextSet tc)) t;
23    r \<leftarrow> handleEvent e;
24    return (r,tc)
25  od"
26
27crunch (empty_fail) empty_fail: kernelEntry_if
28
29definition prod_lift where "prod_lift R r r' \<equiv> R (fst r) (fst r') \<and> (snd r) = (snd r')"
30
31lemma kernel_entry_if_corres:
32  "corres (prod_lift (intr \<oplus> dc)) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
33                       (\<lambda>s. scheduler_action s = resume_cur_thread))
34                      (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and
35                       (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
36                       (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
37                      (kernel_entry_if event tc) (kernelEntry_if event tc)"
38  apply (simp add: kernel_entry_if_def kernelEntry_if_def)
39  apply (rule corres_guard_imp)
40    apply (rule corres_split [OF _ gct_corres])
41      apply (rule corres_split)
42         prefer 2
43         apply simp
44         apply (rule threadset_corresT)
45            apply (simp add: tcb_relation_def
46                             arch_tcb_relation_def
47                             arch_tcb_context_set_def
48                             atcbContextSet_def)
49           apply (clarsimp simp: tcb_cap_cases_def)
50          apply (clarsimp simp: tcb_cte_cases_def)
51         apply (simp add: exst_same_def)
52        apply (rule corres_split [OF _ he_corres])
53          apply (clarsimp simp: prod_lift_def)
54         apply (wp  hoare_TrueI threadSet_invs_trivial thread_set_invs_trivial
55                   thread_set_not_state_valid_sched thread_set_ct_running threadSet_ct_running' static_imp_wp
56               | simp add: tcb_cap_cases_def)+
57   apply (force simp: invs_def cur_tcb_def)
58  apply force
59  done
60
61lemma kernelEntry_invs'[wp]:
62  "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and
63           (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
64           (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
65    kernelEntry_if e tc \<lbrace>\<lambda>_. invs'\<rbrace>"
66  apply (simp add: kernelEntry_if_def)
67  apply (wp threadSet_invs_trivial threadSet_ct_running' static_imp_wp
68         | clarsimp)+
69  done
70
71lemma kernelEntry_valid_duplicates[wp]:
72  "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and
73           (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
74           (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
75    kernelEntry_if e tc \<lbrace>\<lambda>_. (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>"
76  apply (simp add: kernelEntry_if_def)
77  apply (wp handleEvent_valid_duplicates'
78            threadSet_invs_trivial threadSet_ct_running' static_imp_wp
79         | clarsimp)+
80  done
81
82
83lemma kernel_entry_if_domain_time_inv:
84  "\<lbrace> K (e \<noteq> Interrupt) and (\<lambda>s. P (domain_time s)) \<rbrace>
85   kernel_entry_if e tc
86   \<lbrace>\<lambda>_ s. P (domain_time s) \<rbrace>"
87   unfolding kernel_entry_if_def
88   by (wp handle_event_domain_time_inv) simp
89
90lemma kernel_entry_if_valid_domain_time:
91  "\<lbrace>\<lambda>s. 0 < domain_time s \<rbrace>
92   kernel_entry_if Interrupt tc
93   \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread  \<rbrace>"
94   unfolding kernel_entry_if_def
95   apply (rule hoare_pre)
96    apply (wp handle_interrupt_valid_domain_time
97           | clarsimp | wpc)+
98   \<comment> \<open>strengthen post of do_machine_op; we know interrupt occurred\<close>
99   apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)
100   apply (wp+, simp)
101   done
102
103lemma kernel_entry_if_no_preempt:
104  "\<lbrace> \<top> \<rbrace> kernel_entry_if Interrupt ctx \<lbrace>\<lambda>(interrupt,_) _. interrupt = Inr () \<rbrace>"
105  unfolding kernel_entry_if_def
106  by (wp | clarsimp intro!: validE_cases_valid)+
107
108lemma corres_ex_abs_lift:
109  "\<lbrakk>corres r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow>
110   \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>"
111  apply (clarsimp simp: corres_underlying_def valid_def ex_abs_def)
112  apply fastforce
113  done
114
115lemmas schedaction_related = sched_act_rct_related
116
117lemma kernelEntry_ex_abs[wp]:
118  "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle')
119      and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
120      and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs (einvs)\<rbrace>
121   kernelEntry_if e tc
122   \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>"
123  apply (rule hoare_pre)
124   apply (rule corres_ex_abs_lift[OF kernel_entry_if_corres])
125   apply (wp_trace kernel_entry_if_invs kernel_entry_if_valid_sched)
126  apply (clarsimp simp: ex_abs_def)
127  apply (rule_tac x=sa in exI)
128  apply (fastforce simp: ct_running_related ct_idle_related schedaction_related
129                         active_from_running' active_from_running)
130  done
131
132definition
133  kernelCall_H_if
134  where
135  "kernelCall_H_if e \<equiv>
136      {(s, b, (tc,s'))|s b tc s' r. ((r,tc),s') \<in> fst (split (kernelEntry_if e) s) \<and>
137                   b = (case r of Inl _ \<Rightarrow> True | Inr _ \<Rightarrow> False)}"
138
139definition
140  "ptable_rights_s' s \<equiv> ptable_rights (ksCurThread s) (absKState s)"
141
142definition
143  "ptable_lift_s' s \<equiv> ptable_lift (ksCurThread s) (absKState s)"
144
145definition
146  "ptable_attrs_s' s \<equiv> ptable_attrs (ksCurThread s) (absKState s)"
147
148definition
149  "ptable_xn_s' s \<equiv>  \<lambda>addr. XNever \<in> ptable_attrs_s' s addr"
150
151definition doUserOp_if :: "user_transition_if \<Rightarrow> user_context \<Rightarrow> (kernel_state, (event option \<times> user_context)) nondet_monad" where
152  "doUserOp_if uop tc \<equiv>
153  do pr \<leftarrow> gets ptable_rights_s';
154     pxn \<leftarrow> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
155     pl \<leftarrow> gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
156     allow_read \<leftarrow> return {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x};
157     allow_write \<leftarrow> return {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x};
158     t \<leftarrow> getCurThread;
159     um \<leftarrow> gets (\<lambda>s. (user_mem' s \<circ> ptrFromPAddr));
160     dm \<leftarrow> gets (\<lambda>s. (device_mem' s \<circ> ptrFromPAddr));
161     ds \<leftarrow> gets (device_state \<circ> ksMachineState);
162     assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
163     assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
164     es \<leftarrow> doMachineOp getExMonitor;
165     u \<leftarrow>
166       return
167        (uop t pl pr pxn
168          (tc, um |` allow_read,
169           (ds \<circ> ptrFromPAddr) |` allow_read, es));
170     assert (u \<noteq> {});
171     (e, tc', um',ds', es') \<leftarrow> select u;
172     doMachineOp
173      (user_memory_update
174        ((um' |` allow_write \<circ> addrFromPPtr) |` (- (dom ds))));
175     doMachineOp
176      (device_memory_update
177          ((ds' |` allow_write \<circ> addrFromPPtr) |` dom ds));
178     doMachineOp (setExMonitor es');
179     return (e, tc')
180  od"
181
182lemma empty_fail_select_bind: "empty_fail (assert (S \<noteq> {}) >>= (\<lambda>_. select S))"
183  apply (clarsimp simp: empty_fail_def select_def assert_def)
184  done
185
186crunch (empty_fail) empty_fail[wp]: user_memory_update
187crunch (empty_fail) empty_fail[wp]: device_memory_update
188
189lemma getExMonitor_empty_fail[wp]:
190  "empty_fail getExMonitor"
191  by (simp add: getExMonitor_def)
192
193lemma setExMonitor_empty_fail[wp]:
194  "empty_fail (setExMonitor es)"
195  by (simp add: setExMonitor_def)
196
197lemma getExMonitor_no_fail[wp]:
198  "no_fail \<top> getExMonitor"
199  by (simp add: getExMonitor_def)
200
201lemma setExMonitor_no_fail'[wp]:
202  "no_fail \<top> (setExMonitor (x, y))"
203  by (simp add: setExMonitor_def)
204
205lemma setExMonitor_no_fail[wp]:
206  "no_fail \<top> (setExMonitor es)"
207  by (simp add: setExMonitor_def)
208
209lemma doUserOp_if_empty_fail: "empty_fail (doUserOp_if uop tc)"
210  apply (simp add: doUserOp_if_def)
211  apply wp_once
212   apply wp_once
213  apply wp_once
214   apply wp_once
215  apply wp_once
216   apply wp_once
217  apply wp_once
218   apply wp_once
219  apply wp_once
220   apply wp_once
221  apply wp_once
222   apply wp[1]
223  apply wp_once
224   apply wp[1]
225  apply wp_once
226   apply wp[1]
227  apply wp_once
228   apply wp[1]
229  apply wp_once
230   apply wp[1]
231  apply (subst bind_assoc[symmetric])
232  apply (rule empty_fail_bind)
233   apply (rule empty_fail_select_bind)
234  apply (wp | wpc)+
235  done
236
237
238lemma ptable_attrs_abs_state[simp]:
239  "ptable_attrs thread (abs_state s) = ptable_attrs thread s"
240  by (simp add: ptable_attrs_def abs_state_def)
241
242lemma corres_gets_same:
243  assumes equiv: "\<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk>\<Longrightarrow> f s = g s'"
244     and rimp : "\<And>s. P s \<Longrightarrow> R (f s) s"
245     and corres: "\<And>r.  corres_underlying sr b c rr (P and (R r) and (\<lambda>s. r = f s)) Q (n r) (m r)"
246  shows "corres_underlying sr b c rr P Q
247  (do r \<leftarrow> gets f; n r od)
248  (do r \<leftarrow> gets g; m r od)"
249  apply (rule corres_guard_imp)
250  apply (rule corres_split[where r' = "(=)"])
251   apply simp
252   apply (rule corres)
253   apply clarsimp
254   apply (rule equiv)
255   apply (wp|simp)+
256   apply (simp add: rimp)
257  apply simp
258  done
259
260lemma corres_assert_imp_r:
261  "\<lbrakk>\<And>s. P s\<Longrightarrow> Q' ; corres_underlying state_relation a b rr P Q f (g ())\<rbrakk>
262  \<Longrightarrow> corres_underlying state_relation a b rr P Q f (assert Q' >>= g)"
263  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
264
265lemma corres_return_same_trivial:
266  "corres_underlying sr b c (=) \<top> \<top> (return a) (return a)"
267  by simp
268
269crunch (no_fail) no_fail[wp]: device_memory_update
270
271lemma do_user_op_if_corres:
272   "corres (=) (einvs and ct_running and (\<lambda>_. \<forall>t pl pr pxn tcu. f t pl pr pxn tcu \<noteq> {}))
273   (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
274    ct_running')
275   (do_user_op_if f tc) (doUserOp_if f tc)"
276  apply (rule corres_gen_asm)
277  apply (simp add: do_user_op_if_def doUserOp_if_def)
278  apply (rule corres_gets_same)
279    apply (clarsimp simp: ptable_rights_s_def ptable_rights_s'_def)
280    apply (subst absKState_correct, fastforce, assumption+)
281    apply (clarsimp elim!: state_relationE)
282   apply simp
283  apply (rule corres_gets_same)
284    apply (clarsimp simp: ptable_attrs_s'_def ptable_attrs_s_def ptable_xn_s'_def ptable_xn_s_def)
285    apply (subst absKState_correct, fastforce, assumption+)
286    apply (clarsimp elim!: state_relationE)
287   apply simp
288  apply (rule corres_gets_same)
289    apply (clarsimp simp: absArchState_correct curthread_relation ptable_lift_s'_def
290                         ptable_lift_s_def)
291    apply (subst absKState_correct, fastforce, assumption+)
292    apply (clarsimp elim!: state_relationE)
293   apply simp
294  apply (simp add: getCurThread_def)
295  apply (rule corres_gets_same)
296    apply (simp add: curthread_relation)
297   apply simp
298  apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> - device_region s"])
299   apply (clarsimp simp add: user_mem_relation dest!: invs_valid_stateI invs_valid_stateI')
300   apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def)
301   apply fastforce
302  apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> device_region s"])
303   apply (clarsimp simp add: device_mem_relation dest!: invs_valid_stateI invs_valid_stateI')
304   apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def)
305   apply fastforce
306  apply (rule corres_gets_same[where R ="\<lambda>r s. dom r = device_region s"])
307    apply (clarsimp simp: state_relation_def)
308   apply simp
309  apply (rule corres_assert_imp_r)
310   apply fastforce
311  apply (rule corres_assert_imp_r)
312   apply fastforce
313  apply (rule corres_guard_imp)
314       apply (rule corres_split[OF _ corres_machine_op,where r'="(=)"])
315         apply clarsimp
316         apply (rule corres_split[where r'="(=)"])
317            apply clarsimp
318            apply (rule corres_split[OF _ corres_machine_op,where r'="(=)"])
319               apply clarsimp
320               apply (rule corres_split[OF _ corres_machine_op,where r'="(=)"])
321                  apply clarsimp
322                  apply (rule corres_split[OF _ corres_machine_op, where r'="(=)"])
323                     apply (rule corres_return_same_trivial)
324                    apply (wp hoare_TrueI[where P = \<top>] | simp | rule corres_underlying_trivial)+
325            apply (clarsimp simp: user_memory_update_def)
326            apply (rule non_fail_modify)
327           apply clarsimp
328           apply (wp hoare_TrueI)
329          apply clarsimp
330          apply (wp hoare_TrueI)
331         apply (clarsimp simp: select_def corres_underlying_def)
332         apply (simp only: comp_def | wp hoare_TrueI)+
333      apply (rule corres_underlying_trivial)
334     apply (wp hoare_TrueI)+
335   apply clarsimp
336   apply force
337  apply force
338  done
339
340lemma dmo_getExMonitor_wp'[wp]:
341  "\<lbrace>\<lambda>s. P (exclusive_state (ksMachineState s)) s\<rbrace>
342   doMachineOp getExMonitor \<lbrace>P\<rbrace>"
343  apply(simp add: doMachineOp_def)
344  apply(wp modify_wp | wpc)+
345  apply clarsimp
346  apply(erule use_valid)
347   apply wp
348  apply simp
349  done
350
351lemma dmo_setExMonitor_wp'[wp]:
352  "\<lbrace>\<lambda>s. P (s\<lparr>ksMachineState := ksMachineState s
353             \<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace>
354   doMachineOp (setExMonitor es) \<lbrace>\<lambda>_. P\<rbrace>"
355  apply(simp add: doMachineOp_def)
356  apply(wp modify_wp | wpc)+
357  apply clarsimp
358  apply(erule use_valid)
359   apply wp
360  apply simp
361  done
362
363lemma valid_state'_exclusive_state_update[iff]:
364  "valid_state' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = valid_state' s"
365  by (simp add: valid_state'_def valid_machine_state'_def)
366
367lemma invs'_exclusive_state_update[iff]:
368  "invs' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = invs' s"
369  by (simp add: invs'_def)
370
371lemma doUserOp_if_invs'[wp]:
372   "\<lbrace>invs'  and
373    (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
374    ct_running' and ex_abs (einvs)\<rbrace>
375   doUserOp_if f tc
376  \<lbrace>\<lambda>_. invs'\<rbrace>"
377  apply (simp add: doUserOp_if_def split_def ex_abs_def)
378  apply (wp device_update_invs' dmo_setExMonitor_wp' dmo_invs' | simp)+
379         apply (clarsimp simp add: no_irq_modify user_memory_update_def)
380         apply wpsimp
381        apply (wp doMachineOp_ct_running' select_wp)+
382  apply (clarsimp simp: user_memory_update_def simpler_modify_def
383                        restrict_map_def
384                  split: option.splits)
385  apply (drule ptable_rights_imp_UserData[rotated 2], auto simp: ptable_rights_s'_def ptable_lift_s'_def)
386  done
387
388lemma doUserOp_valid_duplicates[wp]:
389  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> doUserOp_if f tc
390  \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
391  apply (simp add: doUserOp_if_def split_def)
392  apply (wp dmo_setExMonitor_wp' dmo_invs' select_wp | simp)+
393  done
394
395lemma doUserOp_if_schedact[wp]:
396   "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
397      doUserOp_if f tc
398     \<lbrace>\<lambda>r s. P (ksSchedulerAction s)\<rbrace>"
399  apply (simp add: doUserOp_if_def)
400  apply (wp select_wp | wpc | simp)+
401  done
402
403lemma doUserOp_if_st_tcb_at[wp]:
404   "\<lbrace>st_tcb_at' st t\<rbrace>
405      doUserOp_if f tc
406     \<lbrace>\<lambda>_. st_tcb_at' st t\<rbrace>"
407  apply (simp add: doUserOp_if_def)
408  apply (wp select_wp | wpc | simp)+
409  done
410
411lemma doUserOp_if_cur_thread[wp]:
412  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> doUserOp_if f tc
413   \<lbrace>\<lambda>r s. P (ksCurThread s)\<rbrace>"
414  apply (simp add: doUserOp_if_def)
415  apply (wp select_wp | wpc | simp)+
416  done
417
418
419lemma doUserOp_if_ct_in_state[wp]:
420  "\<lbrace>ct_in_state' st\<rbrace>
421    doUserOp_if f tc
422   \<lbrace>\<lambda>_. ct_in_state' st\<rbrace>"
423  apply (rule hoare_pre)
424   apply (rule ct_in_state_thread_state_lift')
425    apply (wp | simp)+
426  done
427
428
429lemma corres_ex_abs_lift':
430  "\<lbrakk>corres_underlying state_relation False False r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow>
431   \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>"
432  apply (clarsimp simp: corres_underlying_def valid_def ex_abs_def)
433  apply fastforce
434  done
435
436lemma gct_corres': "corres_underlying state_relation nf nf' (=) \<top> \<top> (gets cur_thread) getCurThread"
437  by (simp add: getCurThread_def curthread_relation)
438
439lemma user_mem_corres':
440  "corres_underlying state_relation nf nf' (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))"
441  by (clarsimp simp add: gets_def get_def return_def bind_def
442                         invs_def invs'_def
443                         corres_underlying_def user_mem_relation)
444
445lemma corres_machine_op':
446  assumes P: "corres_underlying Id nf nf' r P Q x x'"
447  shows      "corres_underlying state_relation nf nf' r (P \<circ> machine_state) (Q \<circ> ksMachineState)
448                       (do_machine_op x) (doMachineOp x')"
449  apply (rule corres_submonad3
450              [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P])
451   apply (simp_all add: state_relation_def swp_def)
452  done
453
454lemma corres_assert':
455  "corres_underlying sr nf False dc \<top> \<top> (assert P) (assert P)"
456  by (clarsimp simp: corres_underlying_def assert_def return_def fail_def)
457
458lemma do_user_op_if_corres':
459   "corres_underlying state_relation nf False (=) (einvs and ct_running)
460   (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
461    ct_running')
462   (do_user_op_if f tc) (doUserOp_if f tc)"
463  apply (simp add: do_user_op_if_def doUserOp_if_def)
464  apply (rule corres_gets_same)
465    apply (clarsimp simp: ptable_rights_s_def ptable_rights_s'_def)
466    apply (subst absKState_correct, fastforce, assumption+)
467    apply (clarsimp elim!: state_relationE)
468   apply simp
469  apply (rule corres_gets_same)
470    apply (clarsimp simp: ptable_attrs_s'_def ptable_attrs_s_def ptable_xn_s'_def ptable_xn_s_def)
471    apply (subst absKState_correct, fastforce, assumption+)
472    apply (clarsimp elim!: state_relationE)
473   apply simp
474  apply (rule corres_gets_same)
475    apply (clarsimp simp: absArchState_correct curthread_relation ptable_lift_s'_def
476                         ptable_lift_s_def)
477    apply (subst absKState_correct, fastforce, assumption+)
478    apply (clarsimp elim!: state_relationE)
479   apply simp
480  apply (simp add: getCurThread_def)
481  apply (rule corres_gets_same)
482    apply (simp add: curthread_relation)
483   apply simp
484  apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> - device_region s"])
485   apply (clarsimp simp add: user_mem_relation dest!: invs_valid_stateI invs_valid_stateI')
486   apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def)
487   apply fastforce
488  apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> device_region s"])
489   apply (clarsimp simp add: device_mem_relation dest!: invs_valid_stateI invs_valid_stateI')
490   apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def dom_def)
491  apply (rule corres_gets_same[where R ="\<lambda>r s. dom r = device_region s"])
492    apply (clarsimp simp: state_relation_def)
493   apply simp
494  apply (rule corres_assert_imp_r)
495   apply fastforce
496  apply (rule corres_assert_imp_r)
497   apply fastforce
498  apply (rule corres_guard_imp)
499       apply (rule corres_split[OF _ corres_machine_op',where r'="(=)"])
500         apply simp
501         apply (rule corres_split[where r'="dc"])
502            apply simp
503            apply (rule corres_split[where r'="(=)"])
504               apply clarsimp
505               apply (rule corres_split[OF _ corres_machine_op',where r'="(=)"])
506                  apply simp
507                  apply (rule corres_split[OF _ corres_machine_op', where r'="(=)"])
508                     apply simp
509                     apply (rule corres_split[OF _ corres_machine_op', where r'="(=)"])
510                     apply (rule corres_return_same_trivial)
511                    apply (wp hoare_TrueI[where P = \<top>] | simp | rule corres_underlying_trivial)+
512           apply (clarsimp simp: select_def corres_underlying_def)
513           apply (simp only: comp_def | wp hoare_TrueI)+
514       apply (rule corres_assert')
515       apply (wp hoare_TrueI[where P = \<top>] | simp | rule corres_underlying_trivial)+
516   apply clarsimp
517   apply force
518  apply force
519  done
520
521lemma doUserOp_if_ex_abs[wp]:
522   "\<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs (einvs)\<rbrace>
523  doUserOp_if f tc
524\<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>"
525  apply (rule hoare_pre)
526   apply (rule corres_ex_abs_lift'[OF do_user_op_if_corres'])
527   apply (rule_tac Q="\<lambda>a . (invs and ct_running) and valid_list and valid_sched" in hoare_strengthen_post)
528    apply (wp do_user_op_if_invs)
529   apply clarsimp
530  apply (clarsimp simp: ex_abs_def)
531  apply (rule_tac x=sa in exI)
532  apply (clarsimp simp: active_from_running ct_running_related
533                          schedaction_related)+
534  done
535
536
537
538definition
539  doUserOp_H_if
540  where
541  "doUserOp_H_if uop \<equiv> {(s,e,(tc,s'))| s e tc s'. ((e,tc),s') \<in> fst (split (doUserOp_if uop) s)}"
542
543definition checkActiveIRQ_if :: "(MachineTypes.register \<Rightarrow> 32 word) \<Rightarrow> (10 word option \<times> (MachineTypes.register \<Rightarrow> 32 word)) kernel" where
544"checkActiveIRQ_if tc \<equiv>
545do
546   irq \<leftarrow> doMachineOp (getActiveIRQ False);
547   return (irq, tc)
548od"
549
550crunch (empty_fail) empty_fail: checkActiveIRQ_if
551
552
553lemma getActiveIRQ_nf: "no_fail (\<lambda>_. True) (getActiveIRQ in_kernel)"
554  apply (simp add: getActiveIRQ_def)
555  apply (rule no_fail_pre)
556   apply (rule non_fail_gets non_fail_modify
557               no_fail_return | rule no_fail_bind | simp
558          | intro impI conjI)+
559     apply (wp del: no_irq | simp)+
560  done
561
562lemma dmo_getActiveIRQ_corres: "corres (=) \<top> \<top> (do_machine_op (getActiveIRQ in_kernel))
563     (doMachineOp (getActiveIRQ in_kernel'))"
564  apply (rule SubMonad_R.corres_machine_op)
565     apply (rule corres_Id)
566       apply (simp add: getActiveIRQ_def non_kernel_IRQs_def)
567      apply simp
568     apply (rule getActiveIRQ_nf)
569   done
570
571lemma check_active_irq_if_corres:
572  "corres (=) \<top> \<top> (check_active_irq_if tc) (checkActiveIRQ_if tc)"
573  apply (simp add: checkActiveIRQ_if_def check_active_irq_if_def)
574  apply (rule corres_underlying_split[where r'="(=)"])
575  apply (rule dmo_getActiveIRQ_corres)
576  apply wp+
577  apply clarsimp
578  done
579
580lemma dmo'_getActiveIRQ_wp:
581  "\<lbrace>\<lambda>s. P (irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := (ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>)\<rparr>)\<rbrace> doMachineOp (getActiveIRQ in_kernel)\<lbrace>P\<rbrace>"
582  apply(simp add: doMachineOp_def getActiveIRQ_def non_kernel_IRQs_def)
583  apply(wp modify_wp | wpc)+
584  apply clarsimp
585  apply(erule use_valid)
586   apply (wp modify_wp)
587  apply(auto simp: irq_at_def)
588  done
589
590lemma checkActiveIRQ_if_wp:
591  "\<lbrace>\<lambda>s. P ((irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s))),tc)
592           (s\<lparr>ksMachineState := (ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>)\<rparr>)\<rbrace> checkActiveIRQ_if tc \<lbrace>P\<rbrace>"
593  apply(simp add: checkActiveIRQ_if_def | wp dmo'_getActiveIRQ_wp)+
594  done
595
596lemma checkActiveIRQ_invs'[wp]: "\<lbrace>invs'\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. invs'\<rbrace>"
597  apply (wp checkActiveIRQ_if_wp)
598  apply simp
599  done
600
601lemma checkActiveIRQ_ct_in_state[wp]: "\<lbrace>ct_in_state' st\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. ct_in_state' st\<rbrace>"
602  apply (wp checkActiveIRQ_if_wp)
603  apply simp
604  done
605
606lemma checkActiveIRQ_schedact[wp]: "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>r s. P (ksSchedulerAction s)\<rbrace>"
607  apply (wp checkActiveIRQ_if_wp)
608  apply simp
609  done
610
611lemma checkActiveIRQ_vs_valid_duplicates'[wp]: "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
612  apply (wp checkActiveIRQ_if_wp)
613  apply simp
614  done
615
616
617lemma checkActiveIRQ_ex_abs[wp]: "\<lbrace>ex_abs (einvs)\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>"
618  apply (rule hoare_pre)
619   apply (rule corres_ex_abs_lift[OF check_active_irq_if_corres])
620   apply (rule check_active_irq_if_wp)
621  apply (clarsimp simp: ex_abs_def)
622  done
623
624definition
625  checkActiveIRQ_H_if
626  where
627  "checkActiveIRQ_H_if \<equiv> {((tc, s), irq, (tc', s')). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}"
628
629definition
630  handlePreemption_if :: "(MachineTypes.register \<Rightarrow> 32 word) \<Rightarrow> (MachineTypes.register \<Rightarrow> 32 word) kernel" where
631  "handlePreemption_if tc \<equiv> do
632     irq \<leftarrow> doMachineOp (getActiveIRQ False);
633     when (irq \<noteq> None) $ handleInterrupt (the irq);
634     return tc
635   od"
636
637crunch (empty_fail) empty_fail: handlePreemption_if
638
639lemma handle_preemption_if_corres:
640 "corres (=) (einvs)
641   (invs')
642   (handle_preemption_if tc) (handlePreemption_if tc)"
643  apply (simp add: handlePreemption_if_def handle_preemption_if_def)
644  apply (rule corres_guard_imp)
645    apply (rule corres_split[where r'="(=)"])
646       apply (rule corres_split[where r'="dc"])
647          apply simp
648         apply (rule corres_when)
649          apply simp
650         apply simp
651         apply (rule handle_interrupt_corres)
652        apply (rule hoare_post_taut[where P=\<top>])+
653      apply (rule dmo_getActiveIRQ_corres)
654     apply (rule dmo_getActiveIRQ_wp)
655    apply (rule dmo'_getActiveIRQ_wp)
656   apply clarsimp+
657  apply (clarsimp simp: invs'_def valid_state'_def irq_at_def invs_def
658                        Let_def valid_irq_states'_def)
659  done
660
661lemma handlePreemption_invs'[wp]:
662  "\<lbrace>invs'\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. invs'\<rbrace>"
663  apply (simp add: handlePreemption_if_def)
664  apply (wp dmo'_getActiveIRQ_wp)
665  apply clarsimp
666  done
667
668lemma handlePreemption_if_valid_duplicates[wp]:
669  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> handlePreemption_if tc
670  \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
671  apply (simp add: handlePreemption_if_def)
672  apply (wp dmo'_getActiveIRQ_wp)
673  apply clarsimp
674  done
675
676lemma handlePreemption_ex_abs[wp]:
677  "\<lbrace>invs' and ex_abs (einvs)\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>"
678  apply (rule hoare_pre)
679   apply (rule corres_ex_abs_lift[OF handle_preemption_if_corres])
680   apply (wp handle_preemption_if_invs)
681  apply (auto simp: ex_abs_def non_kernel_IRQs_def)
682   done
683
684lemma handle_preemption_if_valid_domain_time:
685  "\<lbrace>\<lambda>s. 0 < domain_time s \<rbrace>
686   handle_preemption_if tc
687   \<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread \<rbrace>"
688   unfolding handle_preemption_if_def
689   apply (rule hoare_pre)
690   apply (wp handle_interrupt_valid_domain_time)
691   apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)
692   apply (wp, simp)
693   done
694
695definition
696  handlePreemption_H_if
697  where
698  "handlePreemption_H_if \<equiv>
699      {(s, u, s'). s' \<in> fst (split handlePreemption_if s)}"
700
701definition
702  schedule'_if :: "(MachineTypes.register \<Rightarrow> 32 word) \<Rightarrow> (MachineTypes.register \<Rightarrow> 32 word) kernel" where
703  "schedule'_if tc \<equiv> do
704     schedule;
705     activateThread;
706     return tc
707   od"
708
709crunch (empty_fail) empty_fail: schedule'_if
710
711
712lemma schedule_if_corres:
713 "corres (=) (invs and valid_sched and valid_list)
714   (invs')
715   (schedule_if tc) (schedule'_if tc)"
716  apply (simp add: schedule_if_def schedule'_if_def)
717  apply (rule corres_guard_imp)
718    apply (rule corres_split[where r'="dc"])
719       apply (rule corres_split[where r'="dc"])
720          apply simp
721         apply (rule activate_corres)
722        apply (rule hoare_post_taut[where P=\<top>])+
723      apply (rule schedule_corres)
724     apply (wp schedule_invs')+
725   apply clarsimp+
726  done
727
728lemma schedule_if'_invs'_post:
729  "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle')\<rbrace>"
730  apply (simp add: schedule'_if_def)
731  apply (wp activate_invs' schedule_invs' schedule_sch_act_simple | simp)+
732  done
733
734lemma schedule_if'_invs'[wp]:
735  "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. invs'\<rbrace>"
736  apply (rule hoare_post_imp[OF _ schedule_if'_invs'_post])
737  apply simp
738  done
739
740lemma schedule_if'_ct_running_or_idle[wp]:
741  "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>r s. ct_running' s \<or> ct_idle' s\<rbrace>"
742  apply (rule hoare_post_imp[OF _ schedule_if'_invs'_post])
743  apply simp
744  done
745
746
747lemma schedule_if'_rct[wp]:
748  "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>r s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>"
749  apply (simp add: schedule'_if_def)
750  apply (wp activate_sch_act schedule_sch)
751  done
752
753
754lemma scheduler_if'_valid_duplicates[wp]:
755  "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> schedule'_if tc
756  \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
757  apply (simp add: schedule'_if_def)
758  apply (wp | simp)+
759  done
760
761lemma schedule_if_domain_time_left:
762  "\<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<rbrace>
763   schedule_if tc
764   \<lbrace>\<lambda>rv s. 0 < domain_time s \<rbrace>"
765  unfolding schedule_if_def schedule_det_ext_ext_def schedule_switch_thread_fastfail_def
766  supply ethread_get_wp[wp del]
767  supply if_split[split del]
768  apply (rule hoare_pre)
769   apply (wpsimp simp: ethread_get_when_def wp: gts_wp
770          | wp hoare_drop_imp[where f="ethread_get a b" for a b]
771               hoare_drop_imp[where f="tcb_sched_action a b" for a b])+
772  apply (auto split: if_split)
773  done
774
775lemma scheduler'_if_ex_abs[wp]:
776  "\<lbrace>invs' and ex_abs (einvs)\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>"
777  apply (rule hoare_pre)
778   apply (rule corres_ex_abs_lift[OF schedule_if_corres])
779   apply wp
780  apply (auto simp: ex_abs_def)
781  done
782
783definition
784  schedule'_H_if
785  where
786  "schedule'_H_if \<equiv>
787      {(s, e, s'). s' \<in> fst (split schedule'_if s)}"
788
789definition
790  kernelExit_if
791  where
792  "kernelExit_if tc \<equiv> do
793    t' \<leftarrow> getCurThread;
794    threadGet (atcbContextGet o tcbArch) t'
795  od"
796
797crunch (empty_fail) empty_fail: kernelExit_if
798
799lemma kernel_exit_if_corres:
800 "corres (=) (invs)
801   (invs')
802   (kernel_exit_if tc) (kernelExit_if tc)"
803  apply (simp add: kernel_exit_if_def kernelExit_if_def)
804  apply (rule corres_guard_imp)
805    apply (rule corres_split[where r'="(=)"])
806       apply simp
807       apply (rule threadget_corres)
808       apply (clarsimp simp: tcb_relation_def arch_tcb_relation_def
809                             arch_tcb_context_get_def atcbContextGet_def)
810      apply (rule gct_corres)
811     apply wp+
812   apply clarsimp+
813  done
814
815lemma kernelExit_inv[wp]:
816  "\<lbrace>P\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. P\<rbrace>"
817  apply (simp add: kernelExit_if_def)
818  apply wp
819  done
820
821
822definition
823  kernelExit_H_if
824  where
825  "kernelExit_H_if \<equiv>
826      {(s, m, s'). s' \<in> fst (split kernelExit_if s) \<and>
827                   m = (if ct_running' (snd s') then InUserMode else InIdleMode)}"
828
829definition full_invs_if' where
830  "full_invs_if' \<equiv>
831  {s. invs' (internal_state_if s) \<and> ex_abs (einvs) (internal_state_if s)
832      \<and> vs_valid_duplicates' (ksPSpace (internal_state_if s))
833      \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> ksDomainTime (internal_state_if s) > 0)
834      \<and> (ksDomainTime (internal_state_if s) = 0
835           \<longrightarrow> ksSchedulerAction (internal_state_if s) = ChooseNewThread)
836      \<and> valid_domain_list' (internal_state_if s)
837      \<and> (case (snd s)
838          of (KernelEntry e) \<Rightarrow>
839                     (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if s) \<and>
840                                       ksDomainTime (internal_state_if s) \<noteq> 0) \<and>
841                     (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and>
842                     ksSchedulerAction (internal_state_if s) = ResumeCurrentThread
843           | KernelExit \<Rightarrow>
844                     (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and>
845                     ksSchedulerAction (internal_state_if s) = ResumeCurrentThread \<and>
846                     ksDomainTime (internal_state_if s) \<noteq> 0
847           | InUserMode \<Rightarrow>
848                     ct_running' (internal_state_if s) \<and>
849                     ksSchedulerAction (internal_state_if s) = ResumeCurrentThread
850           | InIdleMode \<Rightarrow>
851                     ct_idle' (internal_state_if s) \<and>
852                     ksSchedulerAction (internal_state_if s) = ResumeCurrentThread
853           | _ \<Rightarrow> True) }"
854
855definition has_srel_state where
856"has_srel_state srel P \<equiv> {s. \<exists>s'. (s,s') \<in> srel \<and> s' \<in> P}"
857
858definition lift_fst_rel where
859  "lift_fst_rel srel \<equiv> {(r,r'). snd r = snd r' \<and> (fst r, fst r') \<in> srel}"
860
861(*Includes serializability*)
862definition step_corres where
863  "step_corres nf srel mode G G' \<equiv>
864         \<lambda>mabs mconc. \<forall>(s,s')\<in>srel. (s',mode) \<in> G' \<and> (s,mode) \<in> G  \<longrightarrow>
865                      ((nf \<longrightarrow> (\<exists>e' t'. (s',e',t') \<in> mconc)) \<and>
866                      (\<forall>e' t'. (s',e',t') \<in> mconc \<longrightarrow>
867                         (\<exists>e t. (s,e,t) \<in> mabs \<and> (t,t') \<in> srel \<and> e = e')))"
868
869
870definition lift_snd_rel where
871  "lift_snd_rel srel \<equiv> {(r,r'). fst r = fst r' \<and> (snd r, snd r') \<in> srel}"
872
873definition preserves where
874"preserves mode mode' P f \<equiv> \<forall>(s,e,s') \<in> f. (s,mode) \<in> P \<longrightarrow> (s',mode') \<in> P"
875
876(*Special case for KernelExit*)
877definition preserves' where
878"preserves' mode P f \<equiv> \<forall>(s,e,s') \<in> f. (s,mode) \<in> P \<longrightarrow> (s',e) \<in> P"
879
880lemma preservesE:
881  assumes preserves: "preserves mode mode' P f"
882  assumes inf: "(s,e,s') \<in> f"
883  assumes P: "(s,mode) \<in> P"
884  assumes a: "(s',mode') \<in> P \<Longrightarrow> Q"
885  shows "Q"
886  apply (rule a)
887  apply (insert preserves inf P)
888  apply (clarsimp simp: preserves_def)
889  apply fastforce
890  done
891
892lemma preserves'E:
893  assumes preserves: "preserves' mode P f"
894  assumes inf: "(s,e,s') \<in> f"
895  assumes P: "(s,mode) \<in> P"
896  assumes a: "(s',e) \<in> P \<Longrightarrow> Q"
897  shows "Q"
898  apply (rule a)
899  apply (insert preserves inf P)
900  apply (clarsimp simp: preserves'_def)
901  apply fastforce
902  done
903
904lemma step_corres_bothE:
905    assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc"
906    assumes preserves: "preserves mode mode' invs_conc f_conc"
907    assumes a: "(s, s') \<in> srel"
908    assumes e: "(s, mode) \<in> invs_abs"
909    assumes b: "(s', mode) \<in> invs_conc"
910    assumes c: "(s', e, t') \<in> f_conc"
911    assumes d: "\<And>t.
912             (s, e, t) \<in> f_abs \<Longrightarrow>
913             (t,mode') \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow>
914             (t, t') \<in> srel \<Longrightarrow> P"
915    shows "P"
916  apply (insert corres a b c e)
917  apply (clarsimp simp: step_corres_def)
918  apply (drule_tac x="(s,s')" in bspec,clarsimp+)
919  apply (drule_tac x=e in spec)
920  apply (drule_tac x="t'" in spec)
921  apply simp
922  apply clarsimp
923  apply (rule_tac t=t in d,simp+)
924  apply (clarsimp simp: has_srel_state_def lift_fst_rel_def)
925  apply (rule preservesE[OF preserves],assumption+)
926  apply fastforce+
927    done
928
929lemma step_corres_both'E:
930    assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc"
931    assumes preserves: "preserves' mode invs_conc f_conc"
932    assumes a: "(s, s') \<in> srel"
933    assumes e: "(s, mode) \<in> invs_abs"
934    assumes b: "(s', mode) \<in> invs_conc"
935    assumes c: "(s', e, t') \<in> f_conc"
936    assumes d: "\<And>t.
937             (s, e, t) \<in> f_abs \<Longrightarrow>
938             (t,e) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow>
939             (t, t') \<in> srel \<Longrightarrow> P"
940    shows "P"
941  apply (insert corres a b c e)
942  apply (clarsimp simp: step_corres_def)
943  apply (drule_tac x="(s,s')" in bspec,clarsimp+)
944  apply (drule_tac x=e in spec)
945  apply (drule_tac x="t'" in spec)
946  apply simp
947  apply clarsimp
948  apply (rule_tac t=t in d,simp+)
949   apply (clarsimp simp: has_srel_state_def lift_fst_rel_def)
950   apply (rule preserves'E[OF preserves],assumption+)
951   apply fastforce+
952    done
953
954lemma step_corresE:
955    assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc"
956    assumes a: "(s, s') \<in> srel"
957    assumes e: "(s, mode) \<in> invs_abs"
958    assumes b: "(s', mode) \<in> invs_conc"
959    assumes c: "(s', e, t') \<in> f_conc"
960    assumes d: "\<And>t.
961             (s, e, t) \<in> f_abs \<Longrightarrow>
962             (t, t') \<in> srel \<Longrightarrow> P"
963    shows "P"
964    apply (insert corres a b c e)
965    apply (clarsimp simp: step_corres_def)
966    apply (drule_tac x="(s,s')" in bspec,clarsimp+)
967    apply (drule_tac x=e in spec)
968    apply (drule_tac x=t' in spec)
969    apply clarsimp
970    apply (rule d)
971    apply simp+
972    done
973end
974
975locale global_automaton_invs =
976  fixes check_active_irq
977  fixes do_user_op
978  fixes kernel_call
979  fixes handle_preemption
980  fixes schedule
981  fixes kernel_exit
982  fixes invs :: "('a global_sys_state) set"
983  fixes ADT :: "(('a global_sys_state),'o, unit) data_type"
984  fixes extras :: "'a global_sys_state set"
985  assumes step_adt: "Step ADT =
986                     (\<lambda>u. (global_automaton_if check_active_irq do_user_op kernel_call handle_preemption schedule kernel_exit) \<inter> {(s,s'). s' \<in> extras})"
987  assumes check_active_irq_invs: "preserves InUserMode InUserMode invs check_active_irq"
988  assumes check_active_irq_idle_invs: "preserves InIdleMode InIdleMode invs check_active_irq"
989  assumes check_active_irq_invs_entry: "preserves InUserMode (KernelEntry Interrupt) invs check_active_irq"
990  assumes check_active_irq_idle_invs_entry: "preserves InIdleMode (KernelEntry Interrupt) invs check_active_irq"
991
992  assumes do_user_op_invs: "preserves InUserMode InUserMode invs do_user_op"
993  assumes do_user_op_invs_entry: "preserves InUserMode (KernelEntry e) invs do_user_op"
994  assumes kernel_call_invs: "e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted invs (kernel_call e)"
995  assumes kernel_call_invs_sched: "preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) invs (kernel_call e)"
996  assumes handle_preemption_invs: "preserves KernelPreempted (KernelSchedule True) invs handle_preemption"
997  assumes schedule_invs: "preserves (KernelSchedule b) KernelExit invs schedule"
998  assumes kernel_exit_invs: "preserves' KernelExit invs kernel_exit"
999  assumes init_invs: "(Init ADT) s \<subseteq> invs"
1000  assumes init_extras: "(Init ADT) s \<subseteq> extras"
1001  begin
1002
1003  lemma ADT_extras: "ADT \<Turnstile> extras"
1004    apply (rule invariantI)
1005    apply (clarsimp simp: init_extras)
1006    apply (clarsimp simp: step_adt)
1007    done
1008
1009  lemma ADT_invs: "ADT \<Turnstile> invs"
1010    apply (rule invariantI)
1011    apply (intro allI)
1012     apply (rule init_invs)
1013    apply (clarsimp simp: step_adt global_automaton_if_def)
1014    apply (elim disjE exE conjE,simp_all)
1015apply (rule preservesE[OF kernel_call_invs])
1016             apply (rule preservesE[OF kernel_call_invs],assumption+)
1017            apply (rule preservesE[OF kernel_call_invs_sched],assumption+)
1018           apply (rule preservesE[OF handle_preemption_invs],assumption+)
1019          apply (rule preservesE[OF schedule_invs],assumption+)
1020         apply (rule preserves'E[OF kernel_exit_invs],assumption+)
1021        apply (rule preservesE[OF check_active_irq_invs],assumption+)
1022        apply (rule preservesE[OF do_user_op_invs_entry],assumption+)
1023       apply (rule preservesE[OF check_active_irq_invs],assumption+)
1024       apply (rule preservesE[OF do_user_op_invs],assumption+)
1025      apply (rule preservesE[OF check_active_irq_invs_entry],assumption+)
1026     apply (rule preservesE[OF check_active_irq_idle_invs_entry],assumption+)
1027    apply (rule preservesE[OF check_active_irq_idle_invs],assumption+)
1028    done
1029end
1030
1031
1032lemma invariant_holds_inter: "A \<Turnstile> I \<Longrightarrow> A \<Turnstile> S \<Longrightarrow> A \<Turnstile> (I \<inter> S)"
1033  apply (clarsimp simp: invariant_holds_def)
1034  apply blast
1035  done
1036
1037lemma preserves_lift_ret: "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>)
1038      \<Longrightarrow>
1039      preserves mode mode' P
1040       {((tc, s), irq, tc', s').
1041        ((irq, tc'), s') \<in> fst (f tc s)}"
1042  apply (clarsimp simp: preserves_def valid_def)
1043  apply fastforce
1044  done
1045
1046lemma preserves_lift: "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),mode') \<in> P\<rbrace>)
1047      \<Longrightarrow>
1048      preserves mode mode' P
1049       {((tc, s), irq, tc', s').
1050        (tc', s') \<in> fst (f tc s)}"
1051  apply (clarsimp simp: preserves_def valid_def)
1052  done
1053
1054
1055lemma preserves_lift':"(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f uop tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>)
1056      \<Longrightarrow>
1057       preserves mode mode' P
1058        {((a, b), e, tc, s') |a b e tc s'.
1059            ((e, tc), s') \<in> fst (f uop a b)}"
1060  apply (clarsimp simp: preserves_def valid_def)
1061  apply fastforce
1062  done
1063
1064lemma preserves_lift'':
1065   "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f e tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>) \<Longrightarrow>
1066       preserves mode mode' P
1067         {((a, b), ba, tc, s') |a b ba tc s'.
1068          \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and> ba = (r \<noteq> Inr ())}"
1069  apply (clarsimp simp: preserves_def valid_def)
1070  apply fastforce
1071  done
1072
1073lemma preserves_lift''': "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),mode') \<in> P\<rbrace>)
1074        \<Longrightarrow>
1075        preserves mode mode' P
1076           {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)}"
1077  apply (clarsimp simp: preserves_def valid_def)
1078  done
1079
1080
1081lemma preserves'_lift:
1082  "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),y s') \<in> P\<rbrace>)
1083        \<Longrightarrow>
1084  preserves' mode P
1085        {(s, m, s').
1086         s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and>
1087         m = (y (snd s'))}"
1088  apply (clarsimp simp: preserves'_def valid_def)
1089  apply fastforce
1090  done
1091
1092lemmas preserves_lifts = preserves_lift_ret preserves_lift preserves_lift'
1093                         preserves_lift'' preserves_lift''' preserves'_lift
1094
1095
1096
1097
1098defs step_restrict_def:
1099  "step_restrict \<equiv> \<lambda>s. s \<in> has_srel_state (lift_fst_rel (lift_snd_rel state_relation)) full_invs_if'"
1100
1101context begin interpretation Arch .
1102lemma abstract_invs:
1103  "global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop)
1104                         kernel_call_A_if kernel_handle_preemption_if
1105                         kernel_schedule_if kernel_exit_A_if
1106                         (full_invs_if) (ADT_A_if uop) {s. step_restrict s}"
1107  supply conj_cong[cong]
1108  apply (unfold_locales)
1109               apply (simp add: ADT_A_if_def)
1110              apply (simp_all add: check_active_irq_A_if_def do_user_op_A_if_def
1111                                    kernel_call_A_if_def kernel_handle_preemption_if_def
1112                                    kernel_schedule_if_def kernel_exit_A_if_def split del: if_split)[12]
1113              apply (rule preserves_lifts |
1114                     wp check_active_irq_if_wp do_user_op_if_invs
1115                    | clarsimp simp add: full_invs_if_def)+
1116          apply (rule_tac Q="\<lambda>r s'. (invs and ct_running) s' \<and>
1117                   valid_list s' \<and>
1118                   valid_sched s' \<and> scheduler_action s' = resume_cur_thread \<and>
1119                   valid_domain_list s' \<and>
1120                   (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread)" in hoare_post_imp)
1121           apply (clarsimp)
1122          apply (wp do_user_op_if_invs hoare_vcg_imp_lift)
1123             apply clarsimp+
1124         apply (rule preserves_lifts)
1125         apply (simp add: full_invs_if_def)
1126         apply (rule_tac Q="\<lambda>r s'. (invs and ct_running) s' \<and>
1127                  valid_list s' \<and>
1128                   valid_domain_list s' \<and>
1129                  domain_time s' \<noteq> 0 \<and>
1130                  valid_sched s' \<and> scheduler_action s' = resume_cur_thread" in hoare_post_imp)
1131          apply (clarsimp simp: active_from_running)
1132         apply (wp do_user_op_if_invs kernel_entry_if_invs kernel_entry_if_valid_sched ; clarsimp)
1133        (* KernelEntry \<rightarrow> KernelPreempted *)
1134        apply (rule preserves_lifts, simp add: full_invs_if_def)
1135        subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched
1136                        kernel_entry_if_domain_time_inv
1137                     ; clarsimp simp: active_from_running)
1138
1139       (* KernelEntry \<rightarrow> KernelSchedule (e = Interrupt) *)
1140       apply (rule preserves_lifts, simp add: full_invs_if_def)
1141       apply (case_tac "e = Interrupt")
1142        subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched kernel_entry_if_valid_domain_time
1143                     | clarsimp simp: active_from_running)+
1144       apply (clarsimp simp: conj_left_commute)
1145       subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched kernel_entry_if_domain_time_inv
1146                    ; clarsimp simp: active_from_running)
1147      (* KernelPreempted \<rightarrow> KernelSchedule True *)
1148      apply (rule preserves_lifts, simp add: full_invs_if_def)
1149      subgoal for tc
1150        apply (rule hoare_pre)
1151         apply (wp handle_preemption_if_invs)
1152         apply (wp handle_preemption_if_valid_domain_time)
1153        apply (clarsimp simp: non_kernel_IRQs_def)
1154        done
1155     (* KernelSchedule \<rightarrow> KernelExit *)
1156     apply (rule preserves_lifts, simp add: full_invs_if_def)
1157     subgoal by (rule hoare_pre, wp schedule_if_domain_time_left, fastforce)
1158    (* KernelExit \<rightarrow> InUserMode \<or> InIdleMode *)
1159    apply (rule preserves_lifts, simp add: full_invs_if_def)
1160    subgoal by (clarsimp cong: conj_cong | wp)+
1161   apply (fastforce simp: full_invs_if_def ADT_A_if_def step_restrict_def)+
1162  done
1163end
1164
1165definition ADT_H_if where
1166"ADT_H_if uop \<equiv> \<lparr>Init = \<lambda>s. ({user_context_of s} \<times> {s'. absKState s' = (internal_state_if s)}) \<times> {sys_mode_of s} \<inter> full_invs_if',
1167                  Fin = \<lambda>((uc,s),m). ((uc, absKState s),m),
1168                  Step = (\<lambda>u. global_automaton_if
1169                              checkActiveIRQ_H_if (doUserOp_H_if uop)
1170                              kernelCall_H_if handlePreemption_H_if
1171                              schedule'_H_if kernelExit_H_if)\<rparr>"
1172
1173crunch ksDomainTime_inv[wp]: doUserOp_if "(\<lambda>s. P (ksDomainTime s))"
1174  (wp: select_wp)
1175
1176crunch ksDomSchedule_inv[wp]: doUserOp_if "(\<lambda>s. P (ksDomSchedule s))"
1177  (wp: select_wp)
1178
1179crunch ksDomainTime_inv[wp]: checkActiveIRQ_if "\<lambda>s. P (ksDomainTime s)"
1180
1181crunch ksDomSchedule_inv[wp]:
1182  kernelEntry_if, handlePreemption_if, checkActiveIRQ_if, schedule'_if
1183  "\<lambda>s. P (ksDomSchedule s)"
1184
1185lemma kernelEntry_if_ksDomainTime_inv:
1186  "\<lbrace> K (e \<noteq> Interrupt) and (\<lambda>s. P (ksDomainTime s)) \<rbrace>
1187   kernelEntry_if e tc
1188   \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
1189   unfolding kernelEntry_if_def
1190   by (wp handleEvent_ksDomainTime_inv) simp
1191
1192lemma kernelEntry_if_valid_domain_time:
1193  "\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace>
1194   kernelEntry_if Interrupt tc
1195   \<lbrace>\<lambda>_ s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread \<rbrace>"
1196   unfolding kernelEntry_if_def
1197  apply (clarsimp simp: handleEvent_def)
1198  apply (rule hoare_pre)
1199   apply (wp handleInterrupt_valid_domain_time | wpc | clarsimp)+
1200       apply (rule hoare_false_imp) \<comment> \<open>debugPrint\<close>
1201       apply (wp handleInterrupt_valid_domain_time hoare_vcg_all_lift hoare_drop_imps | simp)+
1202  done
1203
1204lemma handlePreemption_if_valid_domain_time:
1205  "\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace>
1206   handlePreemption_if tc
1207   \<lbrace>\<lambda>r s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread \<rbrace>"
1208   unfolding handlePreemption_if_def
1209   apply (rule hoare_pre)
1210   apply (wp handleInterrupt_valid_domain_time)
1211   apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, fastforce)
1212   apply (wp, simp)
1213   done
1214
1215lemma schedule'_if_domain_time_left:
1216  "\<lbrace>\<lambda>s. valid_domain_list' s \<and> (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace>
1217   schedule'_if tc
1218   \<lbrace>\<lambda>rv s. 0 < ksDomainTime s \<rbrace>"
1219   unfolding schedule'_if_def
1220   apply (rule hoare_pre)
1221   apply wp
1222   apply (rule hoare_post_imp[OF _ schedule_domain_time_left'])
1223   apply clarsimp+
1224   done
1225
1226lemma kernelEntry_if_no_preempt:
1227  "\<lbrace> \<top> \<rbrace> kernelEntry_if Interrupt ctx \<lbrace>\<lambda>(interrupt,_) _. interrupt = Inr () \<rbrace>"
1228  unfolding kernelEntry_if_def handleEvent_def
1229  by (wp | clarsimp intro!: validE_cases_valid)+
1230
1231lemma haskell_invs:
1232  "global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop)
1233                         kernelCall_H_if handlePreemption_H_if
1234                         schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV"
1235  supply conj_cong[cong]
1236  apply (unfold_locales)
1237               apply (simp add: ADT_H_if_def)
1238              apply (simp_all add: checkActiveIRQ_H_if_def doUserOp_H_if_def
1239                                    kernelCall_H_if_def handlePreemption_H_if_def
1240                                    schedule'_H_if_def kernelExit_H_if_def split del: if_split)[12]
1241              apply (rule preserves_lifts | wp | simp add: full_invs_if'_def
1242                  | wp_once hoare_vcg_disj_lift)+
1243          apply (wp | wp_once hoare_vcg_disj_lift hoare_drop_imps)+
1244         apply simp
1245        apply (rule preserves_lifts)
1246        apply (simp add: full_invs_if'_def)
1247        apply (wp kernelEntry_if_ksDomainTime_inv ; simp)
1248
1249     subgoal for e
1250       apply (rule preserves_lifts, simp add: full_invs_if'_def)
1251       apply wp
1252          apply (case_tac "e = Interrupt")
1253           apply clarsimp
1254           apply (wp kernelEntry_if_valid_domain_time ; simp)
1255          apply clarsimp
1256         apply (wp kernelEntry_if_ksDomainTime_inv ; simp)
1257        apply fastforce+
1258       done
1259      subgoal
1260        apply (rule preserves_lifts, simp add: full_invs_if'_def)
1261        apply (rule hoare_pre)
1262        apply (wp handlePreemption_if_valid_domain_time ; simp)
1263        apply fastforce
1264        done
1265     subgoal
1266       apply (rule preserves_lifts, simp add: full_invs_if'_def)
1267       apply (rule hoare_pre)
1268       apply (wp schedule'_if_domain_time_left)
1269       apply fastforce
1270       done
1271    subgoal by (rule preserves_lifts, simp add: full_invs_if'_def)
1272                (wp, fastforce)
1273   apply (clarsimp simp: ADT_H_if_def)+
1274  done
1275
1276lemma step_corres_exE:
1277  assumes step: "step_corres nf srel mode invs_abs invs_conc f f'"
1278  assumes nf: "nf"
1279  assumes invsC: "(s',mode) \<in> invs_conc"
1280  assumes invsA: "(s,mode) \<in> invs_abs"
1281  assumes srel: "(s,s') \<in> srel"
1282  assumes ex: "\<And>e t' t. (s',e,t') \<in> f' \<Longrightarrow> (s,e,t) \<in> f \<Longrightarrow> (t,t') \<in> srel \<Longrightarrow> P"
1283  shows P
1284  apply (insert step invsC invsA srel nf)
1285  apply (clarsimp simp: step_corres_def)
1286  apply (drule_tac x="(s,s')" in bspec,clarsimp+)
1287  apply (drule_tac x=e' in spec)
1288  apply (drule_tac x=t' in spec)
1289  apply clarsimp
1290  apply (rule ex)
1291  apply assumption+
1292  done
1293
1294
1295
1296locale global_automata_refine =
1297abs : global_automaton_invs check_active_irq_abs do_user_op_abs
1298                      kernel_call_abs handle_preemption_abs
1299                      schedule_abs kernel_exit_abs invs_abs
1300                      ADT_abs extras_abs +
1301conc: global_automaton_invs check_active_irq_conc do_user_op_conc
1302                      kernel_call_conc handle_preemption_conc
1303                      schedule_conc kernel_exit_conc invs_conc
1304                      ADT_conc "UNIV"
1305for                   check_active_irq_abs and
1306                      do_user_op_abs and
1307                      kernel_call_abs and handle_preemption_abs and
1308                      schedule_abs and kernel_exit_abs and invs_abs and
1309                      ADT_abs :: "(('a global_sys_state),'o, unit) data_type" and extras_abs and
1310                      check_active_irq_conc and
1311                      do_user_op_conc  and
1312                      kernel_call_conc and handle_preemption_conc and
1313                      schedule_conc and kernel_exit_conc and
1314                      invs_conc and
1315                      ADT_conc :: "(('c global_sys_state),'o, unit) data_type" +
1316  fixes srel :: "((user_context \<times> 'a) \<times> (user_context \<times> 'c)) set"
1317  fixes nf :: "bool"
1318  assumes extras_abs_intro: "has_srel_state (lift_fst_rel srel) invs_conc \<subseteq> extras_abs"
1319  assumes srel_Fin: "(s,s') \<in> srel \<Longrightarrow> (s,mode) \<in> invs_abs \<Longrightarrow> (s',mode) \<in> invs_conc \<Longrightarrow> (Fin (ADT_conc)) (s',mode) = (Fin (ADT_abs)) (s,mode)"
1320  assumes init_refinement: "((Init (ADT_conc)) a) \<subseteq> lift_fst_rel srel `` ((Init (ADT_abs)) a)"
1321  assumes corres_check_active_irq: "step_corres nf srel InUserMode (invs_abs) invs_conc check_active_irq_abs check_active_irq_conc"
1322  assumes corres_check_active_irq_idle: "step_corres nf srel InIdleMode (invs_abs) invs_conc check_active_irq_abs check_active_irq_conc"
1323  assumes corres_do_user_op: "step_corres nf srel InUserMode (invs_abs) invs_conc (do_user_op_abs) (do_user_op_conc)"
1324  assumes corres_kernel_call: "step_corres nf srel (KernelEntry e) (invs_abs) invs_conc (kernel_call_abs e) (kernel_call_conc e)"
1325  assumes corres_handle_preemption: "step_corres nf srel KernelPreempted (invs_abs) invs_conc handle_preemption_abs handle_preemption_conc"
1326  assumes corres_schedule: "step_corres nf srel (KernelSchedule b) (invs_abs) invs_conc schedule_abs schedule_conc"
1327  assumes corres_kernel_exit: "step_corres nf srel KernelExit (invs_abs) invs_conc kernel_exit_abs kernel_exit_conc"
1328  assumes kernel_call_no_preempt:
1329    "\<And>s s' b. (s, b, s') \<in> kernel_call_abs Interrupt \<Longrightarrow> b = False"
1330
1331  begin
1332
1333
1334lemma extras_inter'[dest!]: "(t,mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> (t,mode) \<in> extras_abs"
1335  apply (rule set_mp)
1336  apply (rule extras_abs_intro)
1337  apply simp
1338  done
1339
1340
1341  lemma fw_sim_abs_conc:
1342  "LI (ADT_abs)
1343      (ADT_conc)
1344      (lift_fst_rel srel)
1345      (invs_abs \<times> invs_conc)"
1346  apply (unfold LI_def )
1347  apply (intro conjI allI)
1348  apply (rule init_refinement)
1349     apply (clarsimp simp: rel_semi_def relcomp_unfold lift_fst_rel_def
1350                           abs.step_adt conc.step_adt)
1351     apply (clarsimp simp: global_automaton_if_def)
1352     apply (elim disjE exE conjE,simp_all)
1353     apply (rule step_corres_bothE[OF  corres_kernel_call conc.kernel_call_invs],assumption+,auto)[1]
1354              apply (rule step_corres_bothE[OF  corres_kernel_call conc.kernel_call_invs_sched],assumption+,auto)[1]
1355            apply (rule step_corres_bothE[OF  corres_handle_preemption conc.handle_preemption_invs],assumption+,auto)[1]
1356           apply (rule step_corres_bothE[OF  corres_schedule conc.schedule_invs],assumption+,auto)[1]
1357          apply (rule step_corres_both'E[OF  corres_kernel_exit conc.kernel_exit_invs],assumption+,auto)[1]
1358         apply (rule preservesE[OF conc.check_active_irq_invs],assumption+)
1359         apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs],assumption+,clarsimp)
1360         apply (rule preservesE[OF abs.check_active_irq_invs],assumption+)
1361         apply (rule_tac s'="(ac,be)" in step_corres_bothE[OF corres_do_user_op conc.do_user_op_invs_entry],assumption+,auto)[1]
1362         apply (rule preservesE[OF conc.check_active_irq_invs],assumption+)
1363         apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs],assumption+,clarsimp)
1364         apply (rule preservesE[OF abs.check_active_irq_invs],assumption+)
1365         apply (rule_tac s'="(ac,be)" in step_corres_bothE[OF corres_do_user_op conc.do_user_op_invs],assumption+,auto)[1]
1366         apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs_entry],assumption+,auto)[1]
1367         apply (rule step_corres_bothE[OF corres_check_active_irq_idle conc.check_active_irq_idle_invs_entry],assumption+,auto)[1]
1368        apply (rule preservesE[OF conc.check_active_irq_idle_invs],assumption+)
1369        apply (rule step_corres_bothE[OF corres_check_active_irq_idle conc.check_active_irq_idle_invs],assumption+,auto)[1]
1370    apply (fastforce intro!: srel_Fin simp: lift_fst_rel_def)
1371    done
1372
1373  lemma fw_simulates: "ADT_conc \<sqsubseteq>\<^sub>F ADT_abs"
1374    apply (rule L_invariantI)
1375      apply (rule abs.ADT_invs)
1376     apply (rule conc.ADT_invs)
1377    apply (rule fw_sim_abs_conc)
1378    done
1379
1380  lemma refinement: "ADT_conc \<sqsubseteq> ADT_abs"
1381    apply (rule sim_imp_refines[OF fw_simulates])
1382    done
1383
1384  lemma conc_serial:
1385    assumes uop_sane: "\<And>s e t. (s,e,t) \<in> do_user_op_conc \<Longrightarrow>
1386                       e \<noteq> Some Interrupt"
1387    assumes no_fail: "nf"
1388    shows
1389    "serial_system (ADT_conc) {s'. \<exists>s. (s,s') \<in> (lift_fst_rel srel) \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}"
1390    apply (insert no_fail)
1391    apply (unfold_locales)
1392    apply (rule fw_inv_transport)
1393    apply (rule abs.ADT_invs)
1394     apply (rule conc.ADT_invs)
1395     apply (rule fw_sim_abs_conc)
1396    apply (clarsimp simp: conc.step_adt global_automaton_if_def lift_fst_rel_def)
1397    apply (case_tac ba,simp_all)
1398         apply (rule step_corres_exE[OF corres_check_active_irq],assumption+)
1399         apply (rule preservesE[OF conc.check_active_irq_invs],assumption+)
1400         apply (rule preservesE[OF abs.check_active_irq_invs],assumption+)
1401         apply (rule_tac s=t and s'=t' in step_corres_exE[OF corres_do_user_op],assumption+)
1402         apply (rule_tac s=t and s'=t' in step_corresE[OF corres_do_user_op],assumption+)
1403         apply clarsimp
1404         apply (case_tac e)
1405          apply (case_tac ea)
1406           apply fastforce
1407          apply simp
1408          apply (frule uop_sane)
1409          apply fastforce
1410         apply (case_tac ea)
1411          apply fastforce
1412         apply fastforce
1413        apply (rule step_corres_exE[OF corres_check_active_irq_idle],assumption+)
1414        apply (case_tac e)
1415         apply fastforce
1416        apply fastforce
1417       apply clarsimp
1418       apply (rule step_corres_exE[OF corres_kernel_call],assumption+)
1419       apply (case_tac e ; fastforce dest: kernel_call_no_preempt)
1420      apply (rule step_corres_exE[OF corres_handle_preemption],assumption+)
1421      apply fastforce
1422     apply (rule step_corres_exE[OF corres_schedule],assumption+)
1423     apply fastforce
1424    apply (rule step_corres_exE[OF corres_kernel_exit],assumption+)
1425    apply fastforce
1426    done
1427
1428lemma abs_serial:
1429  assumes constrained_B: "\<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow>
1430        \<exists>s'. s' \<in> invs_conc \<and> (s, s') \<in> lift_fst_rel srel"
1431  assumes uop_sane: "\<And>s e t. (s,e,t) \<in> do_user_op_conc \<Longrightarrow>
1432                       e \<noteq> Some Interrupt"
1433  assumes no_fail: "nf"
1434  shows
1435  "serial_system (ADT_abs) (invs_abs \<inter> extras_abs)"
1436  apply (rule serial_system.fw_sim_serial)
1437       apply (rule conc_serial)
1438        apply (rule uop_sane,simp)
1439       apply (rule no_fail)
1440      apply (rule fw_sim_abs_conc)
1441     apply (rule invariant_holds_inter)
1442      apply (rule abs.ADT_invs)
1443     apply (rule abs.ADT_extras)
1444    apply clarsimp
1445   apply simp
1446  apply (frule constrained_B)
1447  apply (clarsimp simp: lift_fst_rel_def)
1448  apply auto
1449  done
1450
1451
1452end
1453
1454(*Unused*)
1455  lemma Init_Fin_ADT_H: "s' \<in> full_invs_if' \<Longrightarrow> s' \<in> Init (ADT_H_if uop) (Fin (ADT_H_if uop) s')"
1456    apply (clarsimp simp: ADT_H_if_def)
1457    apply (case_tac s')
1458    apply simp
1459    apply (case_tac a)
1460    apply simp
1461    done
1462
1463(*Unused*)
1464  lemma Fin_Init_ADT_H: "s' \<in> (Init (ADT_H_if uop) s) \<Longrightarrow> s' \<in> full_invs_if' \<Longrightarrow> s \<in> Fin (ADT_H_if uop) ` Init (ADT_H_if uop) s"
1465    apply (clarsimp simp: ADT_H_if_def)
1466    apply (case_tac s)
1467    apply simp
1468    apply clarsimp
1469    apply (simp add: image_def)
1470    apply (rule_tac x="((a,b),baa)" in bexI)
1471    apply clarsimp
1472    apply clarsimp
1473    done
1474
1475
1476lemma
1477  step_corres_lift:
1478   "(\<And>tc. corres_underlying srel False nf (=)
1479             (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc)) \<Longrightarrow>
1480    (\<And>tc. nf \<Longrightarrow> empty_fail (f' tc)) \<Longrightarrow>
1481    step_corres nf (lift_snd_rel srel) mode P
1482     P'
1483     {((tc, s), irq, tc', s').
1484      ((irq, tc'), s') \<in> fst (f tc s)}
1485     {((tc, s), irq, tc', s').
1486      ((irq, tc'), s') \<in> fst (f' tc s)}"
1487  apply (clarsimp simp: corres_underlying_def step_corres_def
1488                        lift_snd_rel_def empty_fail_def)
1489  apply fastforce
1490  done
1491
1492lemma step_corres_lift':
1493  "(\<And>tc. corres_underlying srel False nf (=)
1494            (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f u tc) (f' u tc)) \<Longrightarrow>
1495   (\<And>tc. nf \<Longrightarrow> empty_fail (f' u tc)) \<Longrightarrow>
1496   step_corres nf (lift_snd_rel srel) mode
1497         P P'
1498         {((a, b), e, tc, s') |a b e tc s'.
1499          ((e, tc), s') \<in> fst (f u a b)}
1500         {((a, b), e, tc, s') |a b e tc s'.
1501          ((e, tc), s') \<in> fst (f' u a b)}"
1502  apply (clarsimp simp: corres_underlying_def step_corres_def
1503                        lift_snd_rel_def empty_fail_def)
1504  apply fastforce
1505  done
1506
1507
1508lemma step_corres_lift'':
1509  "(\<And>tc. corres_underlying srel False nf (\<lambda>r r'. ((fst r) = Inr ()) = ((fst r') = Inr ()) \<and> (snd r) = (snd r'))
1510            (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f e tc) (f' e tc)) \<Longrightarrow>
1511  (\<And>tc. nf \<Longrightarrow> empty_fail (f' e tc)) \<Longrightarrow>
1512  step_corres nf (lift_snd_rel srel) mode
1513         P P'
1514         {((a, b), ba, tc, s') |a b ba tc s'.
1515          \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and>
1516              ba = (r \<noteq> Inr ())}
1517         {((a, b), ba, tc, s') |a b ba tc s'.
1518          \<exists>r. ((r, tc), s') \<in> fst (f' e a b) \<and>
1519              ba = (r \<noteq> Inr ())}"
1520  apply (clarsimp simp: corres_underlying_def step_corres_def
1521                        lift_snd_rel_def empty_fail_def)
1522  apply fastforce
1523  done
1524
1525lemma step_corres_lift''':
1526  "(\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc,s),mode) \<in> P)
1527            (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc)) \<Longrightarrow>
1528   (\<And>tc. nf \<Longrightarrow> empty_fail (f' tc)) \<Longrightarrow>
1529  step_corres nf (lift_snd_rel srel) mode
1530     P P'
1531     {(s, u, s').
1532      s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)}
1533     {(s, u, s').
1534      s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa)}"
1535  apply (clarsimp simp: corres_underlying_def step_corres_def
1536                        lift_snd_rel_def empty_fail_def)
1537  apply fastforce
1538  done
1539
1540lemma step_corres_lift'''':
1541  "(\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc,s),mode) \<in> P)
1542            (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc)) \<Longrightarrow>
1543   (\<And>tc. nf \<Longrightarrow> empty_fail (f' tc)) \<Longrightarrow>
1544   (\<And>tc s s'. (s,s') \<in> srel \<Longrightarrow> S' s' \<Longrightarrow> S s \<Longrightarrow> y s = y' s') \<Longrightarrow>
1545      (\<And>tc. \<lbrace>\<lambda>s'. ((tc,s'),mode) \<in> P'\<rbrace> (f' tc) \<lbrace>\<lambda>_. S'\<rbrace>) \<Longrightarrow>
1546      (\<And>tc. \<lbrace>\<lambda>s'. ((tc,s'),mode) \<in> P\<rbrace> (f tc) \<lbrace>\<lambda>_. S\<rbrace>) \<Longrightarrow>
1547   step_corres nf (lift_snd_rel srel) mode P
1548     P'
1549     {(s, m, s').
1550      s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and>
1551      m = (y (snd s'))}
1552     {(s, m, s').
1553      s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa) \<and>
1554      m = (y' (snd s'))}"
1555  apply (clarsimp simp: corres_underlying_def step_corres_def
1556                        lift_snd_rel_def empty_fail_def)
1557  apply (clarsimp simp: valid_def)
1558  apply (drule_tac x=a in meta_spec)+
1559  apply fastforce
1560  done
1561
1562
1563lemmas step_corres_lifts = step_corres_lift step_corres_lift'
1564                           step_corres_lift'' step_corres_lift'''
1565                           step_corres_lift''''
1566
1567
1568lemma st_tcb_at_coerce_haskell: "\<lbrakk>st_tcb_at P t a; (a, c) \<in> state_relation; tcb_at' t c\<rbrakk>
1569\<Longrightarrow> st_tcb_at' (\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) t c"
1570  apply (clarsimp simp: state_relation_def
1571                        pspace_relation_def
1572                        obj_at_def st_tcb_at'_def
1573
1574                        st_tcb_at_def)
1575  apply (drule_tac x=t in bspec)
1576   apply fastforce
1577  apply clarsimp
1578  apply (simp add: other_obj_relation_def)
1579  apply clarsimp
1580  apply (clarsimp simp: obj_at'_def)
1581  apply (simp add: projectKO_eq)
1582  apply (case_tac "ko",simp_all)
1583  apply (simp add: project_inject)
1584  apply (rule_tac x="tcb_state tcb" in exI)
1585  apply simp
1586  apply (simp add: tcb_relation_def)
1587  done
1588
1589
1590lemma ct_running'_related: "\<lbrakk>(a, c) \<in> state_relation; invs' c; ct_running a\<rbrakk> \<Longrightarrow> ct_running' c"
1591  apply (clarsimp simp: ct_in_state_def ct_in_state'_def
1592                        curthread_relation)
1593  apply (frule(1) st_tcb_at_coerce_haskell)
1594  apply (simp add: invs'_def cur_tcb'_def curthread_relation)
1595  apply (erule pred_tcb'_weakenE)
1596  apply (case_tac st, simp_all)[1]
1597  done
1598
1599lemma ct_idle'_related: "\<lbrakk>(a, c) \<in> state_relation; invs' c; ct_idle a\<rbrakk> \<Longrightarrow> ct_idle' c"
1600  apply (clarsimp simp: ct_in_state_def ct_in_state'_def
1601                        curthread_relation)
1602  apply (frule(1) st_tcb_at_coerce_haskell)
1603  apply (simp add: invs'_def cur_tcb'_def curthread_relation)
1604  apply (erule pred_tcb'_weakenE)
1605  apply (case_tac st, simp_all)[1]
1606  done
1607
1608lemma invs_machine_state:
1609  "invs s \<Longrightarrow> valid_machine_state s"
1610  by (clarsimp simp: invs_def valid_state_def)
1611
1612(* FIXME MOVE to where sched_act_rct_related *)
1613lemma sched_act_cnt_related:
1614  "\<lbrakk> (a, c) \<in> state_relation; ksSchedulerAction c = ChooseNewThread \<rbrakk>
1615     \<Longrightarrow> scheduler_action a = choose_new_thread"
1616  by (case_tac "scheduler_action a", simp_all add: state_relation_def)
1617
1618
1619lemma haskell_to_abs: "uop_nonempty uop \<Longrightarrow> global_automata_refine
1620                               check_active_irq_A_if (do_user_op_A_if uop)
1621                               kernel_call_A_if kernel_handle_preemption_if
1622                               kernel_schedule_if kernel_exit_A_if
1623                               full_invs_if (ADT_A_if uop) {s. step_restrict s}
1624                               checkActiveIRQ_H_if (doUserOp_H_if uop)
1625                               kernelCall_H_if handlePreemption_H_if
1626                               schedule'_H_if kernelExit_H_if
1627                               full_invs_if' (ADT_H_if uop) (lift_snd_rel state_relation) True"
1628  apply (simp add: global_automata_refine_def)
1629  apply (intro conjI)
1630    apply (rule abstract_invs)
1631   apply (rule haskell_invs)
1632  apply (unfold_locales)
1633            apply (simp add: step_restrict_def)
1634           apply (simp add: ADT_H_if_def ADT_A_if_def)
1635           apply (clarsimp simp add: lift_snd_rel_def full_invs_if_def full_invs_if'_def)
1636           apply (frule valid_device_abs_state_eq[OF invs_machine_state])
1637           apply (frule absKState_correct[rotated])
1638             apply simp+
1639          apply (simp add: ADT_H_if_def ADT_A_if_def lift_fst_rel_def)
1640          apply (clarsimp simp: lift_snd_rel_def)
1641          apply (subgoal_tac "((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation")
1642           apply (fastforce simp: step_restrict_def has_srel_state_def
1643                                  lift_fst_rel_def lift_snd_rel_def)
1644          apply (simp add: full_invs_if'_def)
1645          apply (clarsimp simp: ex_abs_def)
1646          apply (frule(1) absKState_correct[rotated],simp+)
1647          apply (simp add: full_invs_if_def)
1648          apply (frule valid_device_abs_state_eq[OF invs_machine_state])
1649          apply (case_tac ba; clarsimp simp: domain_time_rel_eq domain_list_rel_eq)
1650              apply (fastforce simp: active_from_running ct_running_related ct_idle_related schedaction_related)+
1651           apply (simp add: sched_act_cnt_related)
1652          apply (fastforce simp: active_from_running ct_running_related ct_idle_related schedaction_related)+
1653         apply (simp add: check_active_irq_A_if_def checkActiveIRQ_H_if_def)
1654         apply (rule step_corres_lifts)
1655          apply (rule corres_guard_imp)
1656            apply (rule check_active_irq_if_corres,simp+)
1657         apply (rule checkActiveIRQ_if_empty_fail)
1658        apply (simp add: check_active_irq_A_if_def checkActiveIRQ_H_if_def)
1659        apply (rule step_corres_lifts)
1660         apply (rule corres_guard_imp)
1661           apply (rule check_active_irq_if_corres,simp+)
1662        apply (rule checkActiveIRQ_if_empty_fail)
1663       apply (simp add: do_user_op_A_if_def doUserOp_H_if_def)
1664       apply (rule step_corres_lifts)
1665        apply (rule corres_guard_imp)
1666          apply (rule do_user_op_if_corres)
1667         apply (fastforce simp: full_invs_if_def uop_nonempty_def)
1668        apply (simp add: full_invs_if'_def uop_nonempty_def)
1669       apply (rule doUserOp_if_empty_fail)
1670      apply (simp add: kernelCall_H_if_def kernel_call_A_if_def)
1671      apply (rule step_corres_lifts)
1672       apply (rule corres_rel_imp)
1673        apply (rule corres_guard_imp)
1674          apply (rule kernel_entry_if_corres)
1675         apply clarsimp
1676         apply ((clarsimp simp: full_invs_if_def full_invs_if'_def)+)[2]
1677       apply (fastforce simp: prod_lift_def)
1678      apply (rule kernelEntry_if_empty_fail)
1679     apply (simp add: kernel_handle_preemption_if_def handlePreemption_H_if_def)
1680     apply (rule step_corres_lifts)
1681      apply (rule corres_guard_imp)
1682        apply (rule handle_preemption_if_corres)
1683       apply (simp add: full_invs_if_def)
1684      apply (simp add: full_invs_if'_def)
1685     apply (rule handlePreemption_if_empty_fail)
1686    apply (simp add: kernel_schedule_if_def schedule'_H_if_def)
1687    apply (rule step_corres_lifts)
1688     apply (rule corres_guard_imp)
1689       apply (rule schedule_if_corres)
1690      apply (simp add: full_invs_if_def)
1691     apply (simp add: full_invs_if'_def)
1692    apply (rule schedule'_if_empty_fail)
1693   apply (simp add: kernel_exit_A_if_def kernelExit_H_if_def split del: if_split)
1694   apply (rule_tac S="\<top>" and S'="invs'" in step_corres_lifts(5))
1695       apply (rule corres_guard_imp)
1696         apply (rule kernel_exit_if_corres)
1697        apply ((simp add: full_invs_if_def full_invs_if'_def)+)[2]
1698      apply (rule kernelExit_if_empty_fail)
1699     apply clarsimp
1700     apply (clarsimp simp: ct_running'_related ct_running_related)
1701    apply wp
1702    apply (clarsimp simp: full_invs_if'_def)
1703   apply wp
1704  apply (clarsimp simp: kernel_call_A_if_def)
1705  apply (drule use_valid[OF _ kernel_entry_if_no_preempt]; simp)
1706  done
1707
1708lemma doUserOp_if_no_interrupt: "\<lbrace>K(uop_sane uop)\<rbrace> doUserOp_if uop tc \<lbrace>\<lambda>r s. (fst r) \<noteq> Some Interrupt\<rbrace>"
1709  apply (simp add: doUserOp_if_def del: split_paired_All)
1710  apply (wp select_wp | wpc)+
1711  apply (clarsimp simp: uop_sane_def simp del: split_paired_All)
1712  done
1713
1714lemma ADT_A_if_Init_Fin_serial: "uop_sane uop \<Longrightarrow>
1715       Init_Fin_serial (ADT_A_if uop) s0 (full_invs_if \<inter> {s. step_restrict s})"
1716  apply (simp add: Init_Fin_serial_def)
1717  apply (rule conjI)
1718   apply (rule global_automata_refine.abs_serial[OF haskell_to_abs])
1719      apply (simp add: uop_sane_def uop_nonempty_def)
1720     apply (fastforce simp: step_restrict_def has_srel_state_def)
1721   apply (clarsimp simp add: doUserOp_H_if_def)
1722   apply (frule use_valid[OF _ doUserOp_if_no_interrupt])
1723    apply simp+
1724  apply (unfold_locales)
1725   apply (clarsimp simp: ADT_A_if_def)+
1726  done
1727
1728lemma ADT_A_if_enabled:
1729  "uop_sane uop \<Longrightarrow> enabled_system (ADT_A_if uop) s0"
1730  apply (rule Init_Fin_serial.enabled)
1731  apply (rule ADT_A_if_Init_Fin_serial)
1732  apply simp
1733  done
1734
1735lemma (in valid_initial_state_noenabled) uop_nonempty:
1736  "uop_nonempty utf"
1737  apply (simp add: uop_nonempty_def utf_non_empty)
1738  done
1739
1740lemma (in valid_initial_state_noenabled) uop_sane:
1741  "uop_sane utf"
1742  apply (simp add: uop_sane_def utf_non_empty)
1743  apply (cut_tac utf_non_interrupt)
1744  apply blast
1745  done
1746
1747sublocale valid_initial_state_noenabled \<subseteq> valid_initial_state
1748     apply (unfold_locales)
1749      using ADT_A_if_enabled[of utf s0, OF uop_sane]
1750      apply (fastforce simp: enabled_system_def s0_def)
1751     using ADT_A_if_Init_Fin_serial[OF uop_sane, of s0]
1752     apply (simp only: Init_Fin_serial_def serial_system_def Init_Fin_serial_axioms_def s0_def)+
1753  done
1754
1755end
1756