1(*
2 * Copyright 2017, Data61, CSIRO
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(DATA61_GPL)
9 *)
10
11chapter "Toplevel Refinement Statement"
12
13(* In progress c refinement *)
14
15theory Refine_C
16imports
17  Init_C
18
19  (* FIXME: Fastpath_C left out, imports lifted here: *)
20  SyscallArgs_C
21  Delete_C
22  Syscall_C
23  "Refine.RAB_FN"
24  "CLib.MonadicRewrite_C"
25
26  "../lib/CToCRefine"
27begin
28
29context begin interpretation Arch . (*FIXME: arch_split*)
30crunch ksQ[wp]: handleVMFault "\<lambda>s. P (ksReadyQueues s)"
31end
32
33context kernel_m
34begin
35
36declare liftE_handle [simp]
37
38lemma schedule_sch_act_wf:
39  "\<lbrace>invs'\<rbrace> schedule \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
40apply (rule hoare_post_imp)
41 apply (erule invs_sch_act_wf')
42apply (rule schedule_invs')
43done
44
45lemma ucast_8_32_neq:
46  "x \<noteq> 0xFF \<Longrightarrow> UCAST(8 \<rightarrow> 32 signed) x \<noteq> 0xFF"
47  by uint_arith (clarsimp simp: uint_up_ucast is_up)
48
49lemma Arch_finaliseInterrupt_ccorres:
50  "ccorres dc xfdc \<top> UNIV [] (return a) (Call Arch_finaliseInterrupt_'proc)"
51  apply (rule ccorres_from_vcg)
52  apply (rule allI, rule conseqPre, vcg)
53  apply (simp add: return_def)
54  done
55
56lemma handleInterruptEntry_ccorres:
57  "ccorres dc xfdc
58           (invs' and sch_act_simple)
59           UNIV []
60           (callKernel Interrupt) (Call handleInterruptEntry_'proc)"
61proof -
62  show ?thesis
63  apply (cinit')
64   apply (simp add: callKernel_def handleEvent_def minus_one_norm)
65   apply (simp add: liftE_bind bind_assoc)
66    apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
67    apply (rule ccorres_Guard_Seq)?
68    apply wpc
69     apply (simp add: irqInvalid_def)
70     apply (rule ccorres_symb_exec_r)
71       apply (ctac (no_vcg) add: schedule_ccorres)
72        apply (rule ccorres_add_return2)
73        apply (ctac (no_vcg) add: activateThread_ccorres)
74         apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
75         apply (rule allI, rule conseqPre, vcg)
76         apply (clarsimp simp: return_def)
77        apply (wp schedule_sch_act_wf schedule_invs'
78             | strengthen invs_queues_imp invs_valid_objs_strengthen)+
79      apply vcg
80     apply vcg
81    apply (clarsimp simp: irqInvalid_def ucast_8_32_neq)
82    apply (rule ccorres_rhs_assoc)
83    apply (ctac (no_vcg) add: handleInterrupt_ccorres)
84     apply (rule ccorres_add_return, ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres)
85      apply (ctac (no_vcg) add: schedule_ccorres)
86       apply (rule ccorres_add_return2)
87       apply (ctac (no_vcg) add: activateThread_ccorres)
88        apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
89        apply (rule allI, rule conseqPre, vcg)
90        apply (clarsimp simp: return_def)
91       apply (wp schedule_sch_act_wf schedule_invs'
92             | strengthen invs_queues_imp invs_valid_objs_strengthen)+
93   apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF" in hoare_post_imp)
94    apply (clarsimp simp: non_kernel_IRQs_def)
95   apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
96  apply (clarsimp simp: invs'_def valid_state'_def)
97  done
98qed
99
100lemma handleUnknownSyscall_ccorres:
101  "ccorres dc xfdc
102           (invs' and ct_running' and
103              (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
104           (UNIV \<inter> {s. of_nat n = w_' s}) []
105           (callKernel (UnknownSyscall n)) (Call handleUnknownSyscall_'proc)"
106  apply (cinit' lift: w_')
107   apply (simp add: callKernel_def handleEvent_def)
108   apply (simp add: liftE_bind bind_assoc)
109   apply (rule ccorres_symb_exec_r)
110     apply (rule ccorres_pre_getCurThread)
111     apply (ctac (no_vcg) add: handleFault_ccorres)
112      apply (ctac (no_vcg) add: schedule_ccorres)
113       apply (rule ccorres_add_return2)
114       apply (ctac (no_vcg) add: activateThread_ccorres)
115        apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
116         apply (rule allI, rule conseqPre, vcg)
117        apply (clarsimp simp: return_def)
118       apply (wp schedule_sch_act_wf schedule_invs'
119              | strengthen invs_queues_imp invs_valid_objs_strengthen)+
120    apply (clarsimp, vcg)
121   apply (clarsimp, rule conseqPre, vcg, clarsimp)
122  apply clarsimp
123  apply (intro impI conjI allI)
124      apply fastforce
125     apply (clarsimp simp: ct_not_ksQ)
126    apply (clarsimp simp add: sch_act_simple_def split: scheduler_action.split)
127   apply (rule active_ex_cap')
128    apply (erule active_from_running')
129   apply (erule invs_iflive')
130  apply (clarsimp simp: ct_in_state'_def)
131  apply (frule st_tcb_idle'[rotated])
132   apply (erule invs_valid_idle')
133  apply (clarsimp simp: cfault_rel_def seL4_Fault_UnknownSyscall_lift is_cap_fault_def)
134  done
135
136lemma handleVMFaultEvent_ccorres:
137  "ccorres dc xfdc
138           (invs' and sch_act_simple and ct_running' and
139               (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
140           (UNIV \<inter> {s.  vm_faultType_' s = vm_fault_type_from_H vmfault_type}) []
141           (callKernel (VMFaultEvent vmfault_type)) (Call handleVMFaultEvent_'proc)"
142  apply (cinit' lift:vm_faultType_')
143   apply (simp add: callKernel_def handleEvent_def)
144   apply (simp add: liftE_bind bind_assoc)
145   apply (rule ccorres_pre_getCurThread)
146   apply (simp add: catch_def)
147   apply (rule ccorres_rhs_assoc2)
148   apply (rule ccorres_split_nothrow_novcg)
149       apply (rule ccorres_split_nothrow_case_sum)
150            apply (ctac (no_vcg) add: handleVMFault_ccorres)
151           apply ceqv
152          apply clarsimp
153         apply clarsimp
154         apply (rule ccorres_cond_univ)
155         apply (rule_tac P="\<lambda>s. ksCurThread s = rv" in ccorres_cross_over_guard)
156         apply (rule_tac xf'=xfdc in ccorres_call)
157            apply (ctac (no_vcg) add: handleFault_ccorres)
158           apply simp
159          apply simp
160         apply simp
161        apply (wp hv_inv_ex')
162       apply (simp add: guard_is_UNIV_def)
163       apply clarsimp
164       apply (vcg exspec=handleVMFault_modifies)
165      apply ceqv
166     apply clarsimp
167     apply (ctac (no_vcg) add: schedule_ccorres)
168      apply (rule ccorres_add_return2)
169      apply (ctac (no_vcg) add: activateThread_ccorres)
170       apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
171       apply (rule allI, rule conseqPre, vcg)
172       apply (clarsimp simp: return_def)
173      apply (wp schedule_sch_act_wf schedule_invs'
174             | strengthen invs_queues_imp invs_valid_objs_strengthen)+
175     apply (case_tac x, clarsimp, wp)
176     apply (clarsimp, wp, simp)
177    apply wp
178   apply (simp add: guard_is_UNIV_def)
179  apply (clarsimp simp: simple_sane_strg[unfolded sch_act_sane_not])
180  by (auto simp: ct_in_state'_def cfault_rel_def is_cap_fault_def ct_not_ksQ
181              elim: pred_tcb'_weakenE st_tcb_ex_cap''
182              dest: st_tcb_at_idle_thread' rf_sr_ksCurThread)
183
184
185lemma handleUserLevelFault_ccorres:
186  "ccorres dc xfdc
187           (invs' and sch_act_simple and ct_running' and
188               (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
189           (UNIV \<inter> {s.  w_a_' s = word1} \<inter> {s. w_b_' s = word2 }) []
190           (callKernel (UserLevelFault word1 word2)) (Call handleUserLevelFault_'proc)"
191  apply (cinit' lift:w_a_' w_b_')
192   apply (simp add: callKernel_def handleEvent_def)
193   apply (simp add: liftE_bind bind_assoc)
194   apply (rule ccorres_symb_exec_r)
195     apply (rule ccorres_pre_getCurThread)
196     apply (ctac (no_vcg) add: handleFault_ccorres)
197      apply (ctac (no_vcg) add: schedule_ccorres)
198       apply (rule ccorres_add_return2)
199       apply (ctac (no_vcg) add: activateThread_ccorres)
200        apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
201        apply (rule allI, rule conseqPre, vcg)
202        apply (clarsimp simp: return_def)
203       apply (wp schedule_sch_act_wf schedule_invs'
204              | strengthen invs_queues_imp invs_valid_objs_strengthen)+
205    apply (clarsimp, vcg)
206   apply (clarsimp, rule conseqPre, vcg, clarsimp)
207  apply clarsimp
208  apply (intro impI conjI allI)
209      apply (simp add: ct_in_state'_def)
210      apply (erule pred_tcb'_weakenE)
211      apply simp
212     apply (clarsimp simp: ct_not_ksQ)
213    apply (clarsimp simp add: sch_act_simple_def split: scheduler_action.split)
214   apply (rule active_ex_cap')
215    apply (erule active_from_running')
216   apply (erule invs_iflive')
217  apply (clarsimp simp: ct_in_state'_def)
218  apply (frule st_tcb_idle'[rotated])
219   apply (erule invs_valid_idle')
220   apply simp
221  apply (clarsimp simp: cfault_rel_def seL4_Fault_UserException_lift)
222  apply (simp add: is_cap_fault_def)
223  done
224
225lemmas syscall_defs =
226  Kernel_C.SysSend_def Kernel_C.SysNBSend_def
227  Kernel_C.SysCall_def Kernel_C.SysRecv_def Kernel_C.SysNBRecv_def
228  Kernel_C.SysReply_def Kernel_C.SysReplyRecv_def Kernel_C.SysYield_def
229
230lemma ct_active_not_idle'_strengthen:
231  "invs' s \<and> ct_active' s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s"
232  by clarsimp
233
234
235
236lemma handleSyscall_ccorres:
237  "ccorres dc xfdc
238           (invs' and
239               sch_act_simple and ct_running' and
240               (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
241           (UNIV \<inter> {s. syscall_' s = syscall_from_H sysc }) []
242           (callKernel (SyscallEvent sysc)) (Call handleSyscall_'proc)"
243  apply (cinit' lift: syscall_')
244   apply (simp add: callKernel_def handleEvent_def minus_one_norm)
245   apply (simp add: handleE_def handleE'_def)
246   apply (rule ccorres_split_nothrow_novcg)
247       apply wpc
248              prefer 3
249              \<comment> \<open>SysSend\<close>
250              apply (clarsimp simp: syscall_from_H_def syscall_defs)
251              apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
252              apply (simp add: handleSend_def)
253              apply (rule ccorres_split_nothrow_case_sum)
254                   apply (ctac (no_vcg) add: handleInvocation_ccorres)
255                  apply ceqv
256                 apply clarsimp
257                 apply (rule ccorres_cond_empty)
258                 apply (rule ccorres_returnOk_skip[unfolded returnOk_def,simplified])
259                apply clarsimp
260                apply (rule ccorres_cond_univ)
261                apply (simp add: liftE_def bind_assoc)
262                apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
263                 apply (rule ccorres_Guard)?
264                 apply (simp only: irqInvalid_def)?
265                 apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm)
266                 apply (subst ccorres_seq_skip'[symmetric])
267                 apply (rule ccorres_split_nothrow_novcg)
268                     apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
269                      apply (case_tac rv, clarsimp, clarsimp simp: ucast_8_32_neq)
270                     apply (rule ccorres_add_return2)
271                     apply (ctac (no_vcg) add: handleInterrupt_ccorres)
272                      apply (ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres, wp)
273                    apply ceqv
274                   apply (rule_tac r=dc and xf=xfdc in ccorres_returnOk_skip[unfolded returnOk_def,simplified])
275                  apply wp
276                 apply (simp add: guard_is_UNIV_def)
277                apply clarsimp
278                apply (rule_tac Q="\<lambda>rv s. invs' s \<and>
279                 (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF"
280                                             in hoare_post_imp)
281                 apply (clarsimp simp: non_kernel_IRQs_def)
282                apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
283               apply (rule_tac Q=" invs' " in hoare_post_imp_dc2E, wp)
284               apply (simp add: invs'_def valid_state'_def)
285              apply clarsimp
286              apply (vcg exspec=handleInvocation_modifies)
287             prefer 3
288             \<comment> \<open>SysNBSend\<close>
289             apply (clarsimp simp: syscall_from_H_def syscall_defs)
290             apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
291             apply (simp add: handleSend_def)
292             apply (rule ccorres_split_nothrow_case_sum)
293                  apply (ctac (no_vcg) add: handleInvocation_ccorres)
294                 apply ceqv
295                apply clarsimp
296                apply (rule ccorres_cond_empty)
297                apply (rule ccorres_returnOk_skip[unfolded returnOk_def,simplified])
298               apply clarsimp
299               apply (rule ccorres_cond_univ)
300               apply (simp add: liftE_def bind_assoc irqInvalid_def)
301               apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
302                apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm)
303                apply (subst ccorres_seq_skip'[symmetric])
304                apply (rule ccorres_split_nothrow_novcg)
305                    apply (rule ccorres_Guard)?
306                    apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
307                     apply (case_tac rv, clarsimp, clarsimp simp: ucast_8_32_neq)
308                     apply (rule ccorres_add_return2)
309                    apply (ctac (no_vcg) add: handleInterrupt_ccorres)
310                     apply (ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres, wp)
311                   apply ceqv
312                  apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified])
313                 apply wp
314                apply (simp add: guard_is_UNIV_def)
315               apply clarsimp
316               apply (rule_tac Q="\<lambda>rv s. invs' s \<and>
317                (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF"
318                                     in hoare_post_imp)
319                apply (clarsimp simp: non_kernel_IRQs_def)
320               apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
321              apply (rule_tac Q=" invs' " in hoare_post_imp_dc2E, wp)
322              apply (simp add: invs'_def valid_state'_def)
323             apply clarsimp
324             apply (vcg exspec=handleInvocation_modifies)
325            \<comment> \<open>SysCall\<close>
326            apply (clarsimp simp: syscall_from_H_def syscall_defs)
327            apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
328            apply (simp add: handleCall_def)
329            apply (rule ccorres_split_nothrow_case_sum)
330                 apply (ctac (no_vcg) add: handleInvocation_ccorres)
331                apply ceqv
332               apply clarsimp
333               apply (rule ccorres_cond_empty)
334               apply (rule ccorres_returnOk_skip[unfolded returnOk_def,simplified])
335              apply clarsimp
336              apply (rule ccorres_cond_univ)
337              apply (simp add: liftE_def bind_assoc irqInvalid_def)
338              apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
339               apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm)
340               apply (subst ccorres_seq_skip'[symmetric])
341               apply (rule ccorres_split_nothrow_novcg)
342                   apply (rule ccorres_Guard)?
343                   apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
344                    apply (case_tac rv, clarsimp)
345                    apply (clarsimp simp: ucast_8_32_neq)
346                   apply clarsimp
347                   apply (rule ccorres_add_return2)
348                   apply (ctac (no_vcg) add: handleInterrupt_ccorres)
349                    apply (ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres, wp)
350                  apply ceqv
351                 apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified])
352                apply wp
353               apply (simp add: guard_is_UNIV_def)
354              apply clarsimp
355              apply (rule_tac Q="\<lambda>rv s. invs' s \<and>
356               (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF"
357                                        in hoare_post_imp)
358               apply (clarsimp simp: non_kernel_IRQs_def)
359              apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
360             apply (rule_tac Q=" invs' " in hoare_post_imp_dc2E, wp)
361             apply (simp add: invs'_def valid_state'_def)
362            apply clarsimp
363            apply (vcg exspec=handleInvocation_modifies)
364           prefer 2
365           \<comment> \<open>SysRecv\<close>
366           apply (clarsimp simp: syscall_from_H_def syscall_defs)
367           apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
368           apply (simp add: liftE_bind)
369           apply (subst ccorres_seq_skip'[symmetric])
370           apply (ctac (no_vcg) add: handleRecv_ccorres)
371            apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified])
372           apply wp
373          prefer 2
374          \<comment> \<open>SysReply\<close>
375          apply (clarsimp simp: syscall_from_H_def syscall_defs)
376          apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
377          apply (simp add: liftE_bind)
378          apply (subst ccorres_seq_skip'[symmetric])
379          apply (ctac (no_vcg) add: handleReply_ccorres)
380           apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified])
381          apply wp
382         \<comment> \<open>SysReplyRecv\<close>
383         apply (clarsimp simp: syscall_from_H_def syscall_defs)
384         apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
385         apply (simp add: liftE_bind bind_assoc)
386         apply (ctac (no_vcg) add: handleReply_ccorres)
387          apply (subst ccorres_seq_skip'[symmetric])
388          apply (ctac (no_vcg) add: handleRecv_ccorres)
389           apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified])
390          apply wp[1]
391         apply clarsimp
392         apply wp
393         apply (rule_tac Q="\<lambda>rv s. ct_in_state' simple' s \<and> sch_act_sane s \<and>
394                            (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))"
395                              in hoare_post_imp)
396          apply (simp add: ct_in_state'_def)
397         apply (wp handleReply_sane handleReply_ct_not_ksQ)
398        \<comment> \<open>SysYield\<close>
399        apply (clarsimp simp: syscall_from_H_def syscall_defs)
400        apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
401        apply (simp add: liftE_bind)
402        apply (subst ccorres_seq_skip'[symmetric])
403        apply (ctac (no_vcg) add: handleYield_ccorres)
404         apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified])
405        apply wp
406       \<comment> \<open>SysNBRecv\<close>
407       apply (clarsimp simp: syscall_from_H_def syscall_defs)
408       apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
409       apply (simp add: liftE_bind)
410       apply (subst ccorres_seq_skip'[symmetric])
411       apply (ctac (no_vcg) add: handleRecv_ccorres)
412        apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified])
413       apply wp
414      \<comment> \<open>rest of body\<close>
415      apply ceqv
416     apply (ctac (no_vcg) add: schedule_ccorres)
417      apply (rule ccorres_add_return2)
418      apply (ctac (no_vcg) add: activateThread_ccorres)
419       apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
420       apply (rule allI, rule conseqPre, vcg)
421       apply (clarsimp simp: return_def)
422      apply (wp schedule_invs' schedule_sch_act_wf | strengthen invs_queues_imp invs_valid_objs_strengthen)+
423     apply (simp
424          | wpc
425          | wp hoare_drop_imp handleReply_sane handleReply_nonz_cap_to_ct schedule_invs'
426               handleReply_ct_not_ksQ[simplified]
427          | strengthen ct_active_not_idle'_strengthen invs_valid_objs_strengthen)+
428      apply (rule_tac  Q="\<lambda>rv. invs' and ct_active'" in hoare_post_imp, simp)
429      apply (wp hy_invs')
430     apply (clarsimp simp add: liftE_def)
431     apply wp
432     apply (rule_tac  Q="\<lambda>rv. invs' and ct_active'" in hoare_post_imp, simp)
433     apply (wp hy_invs')
434    apply (clarsimp simp: liftE_def)
435    apply (wp)
436    apply (rule_tac Q="\<lambda>_. invs'" in hoare_post_imp, simp)
437    apply (wp hw_invs')
438   apply (simp add: guard_is_UNIV_def)
439  apply clarsimp
440  apply (drule active_from_running')
441  apply (frule active_ex_cap')
442   apply (clarsimp simp: invs'_def valid_state'_def)
443  apply (clarsimp simp: simple_sane_strg ct_in_state'_def st_tcb_at'_def obj_at'_def
444                        isReply_def ct_not_ksQ)
445  apply (rule conjI, fastforce)
446  apply (auto simp: syscall_from_H_def Kernel_C.SysSend_def
447              split: option.split_asm)
448  done
449
450lemma ccorres_corres_u:
451  "\<lbrakk> ccorres dc xfdc P (Collect P') [] H C; no_fail P H \<rbrakk> \<Longrightarrow>
452  corres_underlying rf_sr nf nf' dc P P' H (exec_C \<Gamma> C)"
453  apply (clarsimp simp: ccorres_underlying_def corres_underlying_def)
454  apply (drule (1) bspec)
455  apply (clarsimp simp: exec_C_def no_fail_def)
456  apply (rule conjI)
457   apply clarsimp
458   apply (erule_tac x=0 in allE)
459   apply (erule_tac x="Normal y" in allE)
460   apply simp
461   apply (erule impE)
462    apply (drule EHOther [where hs="[]"], simp)
463    apply simp
464   apply fastforce
465  apply clarsimp
466  apply (case_tac xs, simp_all)
467    apply (fastforce intro: EHAbrupt EHEmpty)
468   apply (fastforce intro: EHOther)+
469  done
470
471lemma ccorres_corres_u_xf:
472  "\<lbrakk> ccorres rel xf P (Collect P') [] H C; no_fail P H \<rbrakk> \<Longrightarrow>
473  corres_underlying rf_sr nf nf' rel P P' H ((exec_C \<Gamma> C) >>= (\<lambda>_. gets xf))"
474  apply (clarsimp simp: ccorres_underlying_def corres_underlying_def)
475  apply (drule (1) bspec)
476  apply (clarsimp simp: exec_C_def no_fail_def)
477  apply (drule_tac x = a in spec)
478  apply (clarsimp simp:gets_def NonDetMonad.bind_def get_def return_def)
479  apply (rule conjI)
480   apply clarsimp
481   apply (erule_tac x=0 in allE)
482   apply (erule_tac x="Normal y" in allE)
483   apply simp
484   apply (erule impE)
485    apply (drule EHOther [where hs="[]"], simp)
486    apply simp
487   apply (simp add: unif_rrel_def)
488  apply (clarsimp simp:image_def)
489  apply (case_tac xs, simp_all)
490    apply (fastforce intro: EHAbrupt EHEmpty)
491   apply (fastforce intro: EHOther)+
492  done
493
494definition
495  "all_invs' e \<equiv> \<lambda>s'. \<exists>s :: det_state.
496    (s,s') \<in> state_relation \<and>
497    (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and>
498      scheduler_action s = resume_cur_thread \<and> domain_time s \<noteq> 0) \<and>
499    (invs' s' \<and>
500      (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and>
501      ksSchedulerAction s' = ResumeCurrentThread  \<and> ksDomainTime s' \<noteq> 0)"
502
503lemma no_fail_callKernel:
504  "no_fail (all_invs' e) (callKernel e)"
505  unfolding all_invs'_def
506  apply (rule corres_nofail)
507   apply (rule corres_guard_imp)
508     apply (rule kernel_corres)
509    apply force
510   apply (simp add: sch_act_simple_def)
511  apply metis
512  done
513
514lemma handleHypervisorEvent_ccorres:
515  "ccorres dc xfdc
516           (invs' and sch_act_simple)
517           UNIV []
518           (callKernel (HypervisorEvent t)) handleHypervisorEvent_C"
519  apply (simp add: callKernel_def handleEvent_def handleHypervisorEvent_C_def)
520  apply (simp add: liftE_def bind_assoc)
521  apply (rule ccorres_guard_imp)
522    apply (rule ccorres_symb_exec_l)
523       apply (cases t; simp add: handleHypervisorFault_def)
524       apply (ctac (no_vcg) add: schedule_ccorres)
525        apply (ctac (no_vcg) add: activateThread_ccorres)
526       apply (wp schedule_sch_act_wf schedule_invs'
527              | strengthen invs_queues_imp invs_valid_objs_strengthen)+
528    apply clarsimp+
529  done
530
531lemma callKernel_corres_C:
532  "corres_underlying rf_sr False True dc
533           (all_invs' e)
534           \<top>
535           (callKernel e) (callKernel_C e)"
536  using no_fail_callKernel [of e]
537  apply (clarsimp simp: callKernel_C_def)
538  apply (cases e, simp_all)
539      prefer 4
540      apply (rule ccorres_corres_u)
541       apply simp
542       apply (rule ccorres_guard_imp)
543         apply (rule handleInterruptEntry_ccorres)
544        apply (clarsimp simp: all_invs'_def sch_act_simple_def)
545       apply simp
546      apply assumption
547     prefer 2
548     apply (rule ccorres_corres_u [rotated], assumption)
549     apply simp
550     apply (rule ccorres_guard_imp)
551       apply (rule ccorres_call)
552          apply (rule handleUnknownSyscall_ccorres)
553         apply (clarsimp simp: all_invs'_def sch_act_simple_def)+
554    prefer 3
555    apply (rule ccorres_corres_u [rotated], assumption)
556     apply (rule ccorres_guard_imp)
557       apply (rule ccorres_call)
558          apply (rule handleVMFaultEvent_ccorres)
559         apply (clarsimp simp: all_invs'_def sch_act_simple_def)+
560   prefer 2
561   apply (rule ccorres_corres_u [rotated], assumption)
562    apply (rule ccorres_guard_imp)
563      apply (rule ccorres_call)
564         apply (rule handleUserLevelFault_ccorres)
565        apply (clarsimp simp: all_invs'_def sch_act_simple_def)+
566  apply (rule ccorres_corres_u [rotated], assumption)
567   apply (rule ccorres_guard_imp)
568     apply (rule ccorres_call)
569        apply (rule handleSyscall_ccorres)
570       apply (clarsimp simp: all_invs'_def sch_act_simple_def)+
571   apply (rule ccorres_corres_u [rotated], assumption)
572    apply (rule ccorres_guard_imp)
573         apply (rule handleHypervisorEvent_ccorres)
574        apply (clarsimp simp: all_invs'_def sch_act_simple_def)
575       apply simp
576  done
577
578lemma ccorres_add_gets:
579  "ccorresG rf_sr \<Gamma> rv xf P P' hs (do v \<leftarrow> gets f; m od) c
580    \<Longrightarrow> ccorresG rf_sr \<Gamma> rv xf P P' hs m c"
581  by (simp add: gets_bind_ign)
582
583lemma ccorres_get_registers:
584  "\<lbrakk> \<And>cptr msgInfo. ccorres dc xfdc
585     ((\<lambda>s. P s \<and> Q s \<and>
586           obj_at' (\<lambda>tcb. (user_regs o atcbContextGet o tcbArch) tcb X64.capRegister = cptr
587                      \<and>   (user_regs o atcbContextGet o tcbArch) tcb X64.msgInfoRegister = msgInfo)
588             (ksCurThread s) s) and R)
589     (UNIV \<inter> \<lbrace>\<acute>cptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c \<rbrakk>
590      \<Longrightarrow>
591   ccorres dc xfdc
592     (P and Q and ct_in_state' \<top> and R)
593     {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v
594              \<and> cptr_' s = index (registers_C (tcbContext_C (tcbArch_C v))) (unat Kernel_C.capRegister)
595              \<and> msgInfo_' s = index (registers_C (tcbContext_C (tcbArch_C v))) (unat Kernel_C.msgInfoRegister)} []
596     m c"
597  apply (rule ccorres_assume_pre)
598  apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def)
599  apply (drule obj_at_ko_at', clarsimp)
600  apply (erule_tac x="(user_regs o atcbContextGet o tcbArch) ko X64.capRegister" in meta_allE)
601  apply (erule_tac x="(user_regs o atcbContextGet o tcbArch) ko X64.msgInfoRegister" in meta_allE)
602  apply (erule ccorres_guard_imp2)
603  apply (clarsimp simp: rf_sr_ksCurThread)
604  apply (drule(1) obj_at_cslift_tcb, clarsimp simp: obj_at'_def projectKOs)
605  apply (clarsimp simp: ctcb_relation_def ccontext_relation_def cregs_relation_def
606                        X64.msgInfoRegister_def X64.capRegister_def
607                        carch_tcb_relation_def
608                        "StrictC'_register_defs")
609  done
610
611(* FIXME: move *)
612lemma st_tcb_at'_opeq_simp:
613  "st_tcb_at' ((=) Structures_H.thread_state.Running) (ksCurThread s) s
614    = st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s"
615  by (fastforce simp add: st_tcb_at'_def obj_at'_def)
616
617(* FIXME: fastpath
618lemma callKernel_withFastpath_corres_C:
619  "corres_underlying rf_sr False True dc
620           (all_invs' e)
621           \<top>
622           (callKernel e) (callKernel_withFastpath_C e)"
623  using no_fail_callKernel [of e] callKernel_corres_C [of e]
624  apply (cases "e = SyscallEvent syscall.SysCall \<or>
625            e = SyscallEvent syscall.SysReplyRecv")
626  apply (simp_all add: callKernel_withFastpath_C_def
627                  del: Collect_const cong: call_ignore_cong)
628  apply (erule ccorres_corres_u[rotated])
629  apply (rule ccorres_guard_imp2)
630   apply (rule ccorres_rhs_assoc)+
631   apply (rule ccorres_symb_exec_r)+
632       apply (rule ccorres_Cond_rhs)
633        apply (simp add: dc_def[symmetric])
634        apply (ctac add: ccorres_get_registers[OF fastpath_call_ccorres_callKernel])
635       apply (simp add: dc_def[symmetric])
636       apply (ctac add: ccorres_get_registers[OF fastpath_reply_recv_ccorres_callKernel])
637      apply vcg
638     apply (rule conseqPre, vcg, clarsimp)
639    apply vcg
640   apply (rule conseqPre, vcg, clarsimp)
641  apply (clarsimp simp: all_invs'_def rf_sr_ksCurThread)
642  apply (frule(1) obj_at_cslift_tcb[OF tcb_at_invs'])
643  apply (clarsimp simp: typ_heap_simps' ct_in_state'_def
644                        "StrictC'_register_defs" word_sle_def word_sless_def
645                        st_tcb_at'_opeq_simp)
646  apply (rule conjI, fastforce simp: st_tcb_at'_def)
647  apply (auto elim!: pred_tcb'_weakenE cnode_caps_gsCNodes_from_sr[rotated])
648  done
649*)
650
651lemma threadSet_all_invs_triv':
652  "\<lbrace>all_invs' e and (\<lambda>s. t = ksCurThread s)\<rbrace>
653  threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_. all_invs' e\<rbrace>"
654  unfolding all_invs'_def
655  apply (rule hoare_pre)
656   apply (rule wp_from_corres_unit)
657     apply (rule threadset_corresT [where f="tcb_arch_update (arch_tcb_context_set f)"])
658        apply (simp add: tcb_relation_def arch_tcb_context_set_def
659                         atcbContextSet_def arch_tcb_relation_def)
660       apply (simp add: tcb_cap_cases_def)
661      apply (simp add: tcb_cte_cases_def)
662     apply (simp add: exst_same_def)
663    apply (wp thread_set_invs_trivial thread_set_ct_running thread_set_not_state_valid_sched
664              threadSet_invs_trivial threadSet_ct_running' static_imp_wp
665              thread_set_ct_idle
666           | simp add: tcb_cap_cases_def tcb_arch_ref_def
667           | rule threadSet_ct_in_state'
668           | wp_once hoare_vcg_disj_lift)+
669  apply clarsimp
670  apply (rule exI, rule conjI, assumption)
671  apply (clarsimp simp: invs_def invs'_def cur_tcb_def cur_tcb'_def)
672  apply (simp add: state_relation_def)
673  done
674
675lemma getContext_corres:
676  "t' = tcb_ptr_to_ctcb_ptr t \<Longrightarrow>
677  corres_underlying rf_sr False True (=) (tcb_at' t) \<top>
678                    (threadGet (atcbContextGet o tcbArch) t) (gets (getContext_C t'))"
679  apply (clarsimp simp: corres_underlying_def simpler_gets_def)
680  apply (drule obj_at_ko_at')
681  apply clarsimp
682  apply (frule threadGet_eq)
683  apply (rule bexI)
684   prefer 2
685   apply assumption
686  apply clarsimp
687  apply (clarsimp simp: getContext_C_def)
688  apply (drule cmap_relation_ko_atD [rotated])
689   apply fastforce
690  apply (clarsimp simp: typ_heap_simps ctcb_relation_def carch_tcb_relation_def from_user_context_C)
691  done
692
693lemma callKernel_cur:
694  "\<lbrace>all_invs' e\<rbrace> callKernel e \<lbrace>\<lambda>rv s. tcb_at' (ksCurThread s) s\<rbrace>"
695  apply (rule hoare_chain)
696    apply (rule ckernel_invs)
697   apply (clarsimp simp: all_invs'_def sch_act_simple_def)
698  apply clarsimp
699  done
700
701lemma entry_corres_C:
702  "fp = False \<Longrightarrow> (* FIXME: fastpath *)
703  corres_underlying rf_sr False True (=)
704           (all_invs' e)
705           \<top>
706           (kernelEntry e uc) (kernelEntry_C fp e uc)"
707  apply (simp add: kernelEntry_C_def kernelEntry_def getCurThread_def)
708  apply (rule corres_guard_imp)
709    apply (rule corres_split [where P=\<top> and P'=\<top> and r'="\<lambda>t t'. t' = tcb_ptr_to_ctcb_ptr t"])
710       prefer 2
711       apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
712      apply (rule corres_split)
713         prefer 2
714         apply (rule setTCBContext_C_corres, rule ccontext_rel_to_C, simp)
715         apply simp
716        apply (rule corres_split)
717           prefer 2
718(* FIXME: fastpath
719           apply (rule corres_cases[where R=fp], simp_all add: dc_def[symmetric])[1]
720            apply (rule callKernel_withFastpath_corres_C, simp)
721*)
722           apply (rule callKernel_corres_C[unfolded dc_def], simp)
723          apply (rule corres_split [where P=\<top> and P'=\<top> and r'="\<lambda>t t'. t' = tcb_ptr_to_ctcb_ptr t"])
724             prefer 2
725             apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
726            apply (rule getContext_corres[unfolded o_def], simp)
727           apply (wp threadSet_all_invs_triv' callKernel_cur)+
728   apply (clarsimp simp: all_invs'_def invs'_def cur_tcb'_def valid_state'_def)
729  apply simp
730  done
731
732lemma entry_refinement_C:
733  "\<lbrakk>all_invs' e s; (s, t) \<in> rf_sr; fp = False (* FIXME: fastpath *) \<rbrakk>
734     \<Longrightarrow> \<not> snd (kernelEntry_C fp e tc t)
735        \<and> (\<forall>tc' t'. (tc',t') \<in> fst (kernelEntry_C fp e tc t)
736            \<longrightarrow> (\<exists>s'. (tc', s') \<in> fst (kernelEntry e tc s) \<and> (s',t') \<in> rf_sr))"
737  using entry_corres_C [where e=e and fp=False]
738  by (fastforce simp add: corres_underlying_def)
739
740lemma ct_running'_C:
741  "\<lbrakk> (s, t) \<in> rf_sr; invs' s \<rbrakk> \<Longrightarrow> ct_running' s = ct_running_C t"
742  apply (simp add: ct_running_C_def Let_def ct_in_state'_def st_tcb_at'_def)
743  apply (clarsimp simp: rf_sr_def cstate_relation_def cpspace_relation_def Let_def)
744  apply (rule iffI)
745   apply (drule obj_at_ko_at')
746   apply clarsimp
747   apply (erule (1) cmap_relation_ko_atE)
748   apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def)
749  apply clarsimp
750  apply (drule (1) cmap_relation_cs_atD [where addr_fun=tcb_ptr_to_ctcb_ptr])
751   apply simp
752  apply clarsimp
753  apply (frule (1) map_to_ko_atI')
754  apply (erule obj_at'_weakenE)
755  apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def)
756  apply (case_tac "tcbState ko", simp_all add:
757    ThreadState_Running_def
758    ThreadState_BlockedOnReceive_def
759    ThreadState_BlockedOnSend_def
760    ThreadState_BlockedOnReply_def
761    ThreadState_BlockedOnNotification_def
762    ThreadState_Inactive_def
763    ThreadState_IdleThreadState_def
764    ThreadState_Restart_def)
765  done
766
767lemma full_invs_both:
768  "ADT_H uop \<Turnstile>
769  {s'. \<exists>s. (s,s') \<in> lift_state_relation state_relation \<and>
770     s \<in> full_invs \<and> s' \<in> full_invs'}"
771  apply (rule fw_inv_transport)
772    apply (rule akernel_invariant)
773   apply (rule ckernel_invariant)
774  apply (rule fw_sim_A_H)
775  done
776end
777
778(* FIXME: move to somewhere sensible *)
779lemma dom_eq:
780  "dom um = dom um' \<longleftrightarrow> (\<forall>a. um a = None \<longleftrightarrow> um' a = None)"
781  apply (simp add: dom_def del: not_None_eq)
782  apply (rule iffI)
783   apply (rule allI)
784   apply (simp add: set_eq_iff)
785   apply (drule_tac x=a in spec)
786   apply auto
787done
788
789lemma dom_user_mem':
790  "dom (user_mem' s) = {p. typ_at' UserDataT (p && ~~ mask pageBits) s}"
791  by (clarsimp simp:user_mem'_def dom_def pointerInUserData_def split:if_splits)
792
793(* FIXME:move *)
794lemma dom_device_mem':
795  "dom (device_mem' s) = {p. typ_at' UserDataDeviceT (p && ~~ mask pageBits) s}"
796  by (clarsimp simp: device_mem'_def dom_def pointerInDeviceData_def split: if_splits)
797
798context kernel_m
799begin
800
801lemma user_memory_update_corres_C_helper:
802      "\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a;
803        dom um \<subseteq> dom (user_mem' a)\<rbrakk>
804       \<Longrightarrow> (ksMachineState_update
805            (underlying_memory_update
806              (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m [p\<leftarrow>e. p \<in> dom um])) a,
807            b\<lparr>globals := globals b
808               \<lparr>t_hrs_' :=
809                  (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b)))
810                    [p\<leftarrow>e. p \<in> dom um],
811                   snd (t_hrs_' (globals b)))\<rparr>\<rparr>)
812           \<in> rf_sr"
813apply (induct e)
814 apply simp
815 apply (subgoal_tac
816          "ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a = a")
817  apply (simp (no_asm_simp))
818 apply simp
819apply (rename_tac x xs)
820apply (simp add: foldl_fun_upd_eq_foldr)
821apply (case_tac "x \<in> dom um", simp_all)
822apply (frule_tac ptr=x and b="the (um x)" in storeByteUser_rf_sr_upd)
823   apply simp
824  apply simp
825 apply (thin_tac "(x,y) : rf_sr" for x y)+
826 apply (fastforce simp add: pointerInUserData_def dom_user_mem')
827apply (simp add: o_def hrs_mem_update_def)
828done
829
830lemma user_memory_update_corres_C:
831  "corres_underlying rf_sr False nf (%_ _. True)
832     (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom um \<subseteq> dom (user_mem' s))
833     \<top>
834     (doMachineOp (user_memory_update um)) (setUserMem_C um)"
835  apply (clarsimp simp: corres_underlying_def)
836  apply (rule conjI)
837   prefer 2
838   apply (clarsimp simp add: setUserMem_C_def simpler_modify_def)
839  apply (subgoal_tac
840       "doMachineOp (user_memory_update um) a =
841        modify (ksMachineState_update (underlying_memory_update
842                 (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m [p\<leftarrow>enum. p \<in> dom um])))
843               a")
844  prefer 2
845   apply (clarsimp simp add: doMachineOp_def user_memory_update_def
846                             simpler_modify_def simpler_gets_def select_f_def
847                             NonDetMonad.bind_def return_def)
848   apply (thin_tac P for P)+
849   apply (case_tac a, clarsimp)
850   apply (case_tac ksMachineState, clarsimp)
851   apply (rule ext)
852   apply (simp add: foldl_fun_upd_value dom_def split: option.splits)
853  apply clarsimp
854  apply (cut_tac s'=a and s="globals b" in user_mem_C_relation[symmetric])
855    apply (simp add: rf_sr_def cstate_relation_def Let_def cpspace_relation_def)
856   apply simp+
857  apply (simp add: setUserMem_C_def_foldl)
858  apply (clarsimp simp add: simpler_modify_def)
859  apply (thin_tac "doMachineOp p s = x" for p s x)
860  apply (drule sym, simp)
861  apply (rule user_memory_update_corres_C_helper,auto)[1]
862  done
863
864lemma device_update_corres_C:
865  "corres_underlying rf_sr False nf (=) (\<lambda>_. True) (\<lambda>_. True)
866   (doMachineOp (device_memory_update ms))
867   (setDeviceState_C ms)"
868  apply (clarsimp simp: corres_underlying_def)
869  apply (rule conjI)
870    prefer 2
871    apply (clarsimp simp add: setDeviceState_C_def simpler_modify_def)
872  apply (rule ballI)
873  apply (clarsimp simp: simpler_modify_def setDeviceState_C_def)
874  apply (clarsimp simp: doMachineOp_def device_memory_update_def NonDetMonad.bind_def in_monad
875                        gets_def get_def return_def simpler_modify_def select_f_def)
876  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
877                        cmachine_state_relation_def)
878  done
879
880lemma mem_dom_split:
881 "(dom um \<subseteq> dom (user_mem' s) \<union> dom (device_mem' s))
882 \<Longrightarrow> um = restrict_map um (dom (user_mem' s)) ++ restrict_map um (dom (device_mem' s))"
883 apply (rule ext)
884 apply (auto simp: map_add_def restrict_map_def split:if_splits option.splits)
885 done
886
887lemma dom_if_rewrite:
888  "dom (\<lambda>x. if P x then Some (f x) else None) = dom (\<lambda>x. if P x then Some () else None)"
889  by (auto split:if_splits)
890
891crunch dmo_typ_at_pre_dom[wp]: doMachineOp "\<lambda>s. P (dom (\<lambda>x. if typ_at' T (x && ~~ mask pageBits) s then Some () else None))"
892  (wp: crunch_wps simp: crunch_simps device_mem'_def)
893
894lemma dmo_domain_device_mem'[wp]:
895  "\<lbrace>\<lambda>s. P (dom (device_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (device_mem' sa))\<rbrace>"
896  apply (simp add:device_mem'_def pointerInDeviceData_def)
897  apply (rule hoare_pre)
898  apply (subst dom_if_rewrite)
899  apply (wp doMachineOp_typ_at')
900  apply (erule arg_cong[where f = P,THEN iffD1,rotated])
901  apply (auto split:if_splits)
902  done
903
904lemma dmo_domain_user_mem'[wp]:
905  "\<lbrace>\<lambda>s. P (dom (user_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (user_mem' sa))\<rbrace>"
906  apply (simp add:user_mem'_def pointerInUserData_def)
907  apply (rule hoare_pre)
908  apply (subst dom_if_rewrite)
909  apply (wp doMachineOp_typ_at')
910  apply (erule arg_cong[where f = P,THEN iffD1,rotated])
911  apply (auto split:if_splits)
912  done
913
914lemma do_user_op_corres_C:
915  "corres_underlying rf_sr False False (=) (invs' and ex_abs einvs) \<top>
916                     (doUserOp f tc) (doUserOp_C f tc)"
917  apply (simp only: doUserOp_C_def doUserOp_def split_def)
918  apply (rule corres_guard_imp)
919    apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split)
920       prefer 2
921       apply (clarsimp simp: simpler_gets_def getCurThread_def
922                corres_underlying_def rf_sr_def cstate_relation_def Let_def)
923      apply (rule_tac P=valid_state' and P'=\<top> and r'="(=)" in corres_split)
924         prefer 2
925         apply (clarsimp simp: cstate_to_A_def absKState_def
926                               rf_sr_def cstate_to_H_correct ptable_lift_def)
927        apply (rule_tac P=valid_state' and P'=\<top> and r'="(=)" in corres_split)
928           prefer 2
929           apply (clarsimp simp: cstate_to_A_def absKState_def
930                                 rf_sr_def cstate_to_H_correct ptable_rights_def)
931          apply (rule_tac P=pspace_distinct' and P'=\<top> and r'="(=)"
932                 in corres_split)
933             prefer 2
934             apply clarsimp
935             apply (rule fun_cong[where x=ptrFromPAddr])
936             apply (rule_tac f=comp in arg_cong)
937             apply (rule user_mem_C_relation[symmetric])
938              apply (simp add: rf_sr_def cstate_relation_def Let_def
939                               cpspace_relation_def)
940             apply assumption
941            apply (rule_tac P=pspace_distinct' and P'=\<top> and r'="(=)"
942                 in corres_split)
943               prefer 2
944               apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
945                               cpspace_relation_def)
946               apply (drule(1) device_mem_C_relation[symmetric])
947               apply (simp add: comp_def)
948              apply (rule_tac P=valid_state' and P'=\<top> and r'="(=)" in corres_split)
949                 prefer 2
950                 apply (clarsimp simp: cstate_relation_def rf_sr_def
951                   Let_def cmachine_state_relation_def)
952                apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split)
953                   prefer 2
954                   apply (clarsimp simp add: corres_underlying_def fail_def
955                        assert_def return_def
956                        split:if_splits)
957                  apply simp
958                  apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split)
959                    prefer 2
960                    apply (clarsimp simp add: corres_underlying_def fail_def
961                         assert_def return_def
962                         split:if_splits)
963                   apply simp
964                   apply (rule_tac r'="(=)" in corres_split[OF _ corres_select])
965                      prefer 2
966                      apply clarsimp
967                     apply simp
968                     apply (rule corres_split[OF _ user_memory_update_corres_C])
969                         apply (rule corres_split[OF _ device_update_corres_C,
970                                         where R="\<top>\<top>" and R'="\<top>\<top>"])
971                        apply (wp select_wp | simp)+
972   apply (intro conjI allI ballI impI)
973     apply ((clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def)+)[5]
974    apply (clarsimp simp:  ex_abs_def restrict_map_def
975                  split: if_splits)
976    apply (drule ptable_rights_imp_UserData[rotated -1])
977     apply fastforce+
978    apply (clarsimp simp: invs'_def valid_state'_def user_mem'_def device_mem'_def
979                   split: if_splits)
980    apply (drule_tac c = x in subsetD[where B = "dom S" for S])
981     apply (simp add:dom_def)
982    apply fastforce
983   apply clarsimp
984  done
985
986lemma check_active_irq_corres_C:
987  "corres_underlying rf_sr False True (=)
988             (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) \<top>
989             (checkActiveIRQ) (checkActiveIRQ_C)"
990  apply (simp add: checkActiveIRQ_C_def checkActiveIRQ_def getActiveIRQ_C_def)
991  apply (rule corres_guard_imp)
992    apply (subst bind_assoc[symmetric])
993    apply (rule corres_split)
994       apply simp
995       apply (rule ccorres_corres_u_xf)
996       apply (rule ccorres_rel_imp, rule ccorres_guard_imp)
997          apply (ctac add:getActiveIRQ_ccorres)
998         apply (rule TrueI)
999        apply (simp (no_asm))
1000       apply (clarsimp simp: irqInvalid_def ucast_up_ucast_id
1001                             is_up_def source_size_def target_size_def word_size
1002                       split: option.splits )
1003      apply (rule no_fail_dmo')
1004      apply (rule no_fail_getActiveIRQ)
1005     apply (rule hoare_TrueI)+
1006     apply (wp|simp)+
1007  done
1008
1009
1010lemma refinement2_both:
1011  "fp = False \<Longrightarrow> (* FIXME: fastpath *)
1012  \<lparr> Init = Init_C, Fin = Fin_C,
1013     Step = (\<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)) \<rparr>
1014   \<sqsubseteq> ADT_H uop"
1015  supply word_neq_0_conv[simp]
1016  apply (rule sim_imp_refines)
1017  apply (rule L_invariantI [where I\<^sub>c=UNIV and r="lift_state_relation rf_sr"])
1018    apply (rule full_invs_both)
1019   apply simp
1020  apply (unfold LI_def)
1021  apply (rule conjI)
1022   apply (simp add: ADT_H_def)
1023   apply (blast intro!: init_refinement_C)
1024  apply (rule conjI)
1025   prefer 2
1026   apply (simp add: ADT_H_def)
1027   apply (clarsimp simp: Fin_C_def)
1028   apply (drule lift_state_relationD)
1029   apply (clarsimp simp: cstate_to_A_def)
1030    apply (subst cstate_to_H_correct)
1031     apply (fastforce simp: full_invs'_def invs'_def)
1032    apply (clarsimp simp: rf_sr_def)
1033   apply (simp add:absKState_def observable_memory_def absExst_def)
1034   apply (rule MachineTypes.machine_state.equality,simp_all)[1]
1035   apply (rule ext)
1036   apply (clarsimp simp: user_mem'_def option_to_0_def split:if_splits)
1037  apply (simp add: ADT_H_def)
1038  apply (clarsimp simp: rel_semi_def global_automaton_def relcomp_unfold
1039                        in_lift_state_relation_eq)
1040
1041  apply (erule_tac P="a \<and> (\<exists>x. b x)" for a b in disjE)
1042  apply (clarsimp simp add: kernel_call_C_def kernel_call_H_def)
1043  apply (subgoal_tac "all_invs' x b")
1044   apply (drule_tac fp=fp and tc=af in entry_refinement_C, simp+)
1045   apply clarsimp
1046   apply (drule spec, drule spec, drule(1) mp)
1047   apply (clarsimp simp: full_invs'_def)
1048   apply (frule use_valid, rule kernelEntry_invs',
1049          simp add: sch_act_simple_def)
1050    apply (fastforce simp: ct_running'_C)
1051    apply (clarsimp simp: full_invs_def full_invs'_def all_invs'_def)
1052   apply fastforce
1053
1054  apply (erule_tac P="a \<and> b \<and> c \<and> d \<and> e" for a b c d e in disjE)
1055   apply (clarsimp simp add: do_user_op_C_def do_user_op_H_def monad_to_transition_def)
1056   apply (rule rev_mp, rule_tac f="uop" and tc=af in do_user_op_corres_C)
1057   apply (clarsimp simp: corres_underlying_def invs_def ex_abs_def)
1058   apply (fastforce simp: full_invs'_def ex_abs_def)
1059
1060  apply (erule_tac P="a \<and> b \<and> c \<and> (\<exists>x. e x)" for a b c d e in disjE)
1061   apply (clarsimp simp add: do_user_op_C_def do_user_op_H_def monad_to_transition_def)
1062   apply (rule rev_mp, rule_tac f="uop" and tc=af in do_user_op_corres_C)
1063   apply (clarsimp simp: corres_underlying_def invs_def ex_abs_def)
1064   apply (fastforce simp: full_invs'_def ex_abs_def)
1065
1066  apply (clarsimp simp: check_active_irq_C_def check_active_irq_H_def)
1067  apply (rule rev_mp, rule check_active_irq_corres_C)
1068  apply (fastforce simp: corres_underlying_def full_invs'_def ex_abs_def)
1069  done
1070
1071theorem refinement2:
1072  "ADT_C uop \<sqsubseteq> ADT_H uop"
1073  unfolding ADT_C_def
1074  by (rule refinement2_both) simp
1075
1076(* FIXME: fastpath
1077theorem fp_refinement:
1078  "ADT_FP_C uop \<sqsubseteq> ADT_H uop"
1079  unfolding ADT_FP_C_def
1080  by (rule refinement2_both)
1081*)
1082
1083theorem seL4_refinement:
1084  "ADT_C uop \<sqsubseteq> ADT_A uop"
1085  by (blast intro: refinement refinement2 refinement_trans)
1086
1087(* FIXME: fastpath
1088theorem seL4_fastpath_refinement:
1089  "ADT_FP_C uop \<sqsubseteq> ADT_A uop"
1090  by (blast intro: refinement fp_refinement refinement_trans)
1091*)
1092
1093lemma exec_C_Basic:
1094  "exec_C Gamma (Basic f) = (modify f)"
1095  apply (rule ext)
1096  apply (simp add: exec_C_def simpler_modify_def)
1097  apply (auto elim: exec.cases intro: exec.intros)
1098  done
1099
1100lemma in_monad_imp_rewriteE:
1101  "\<lbrakk> (a, b) \<in> fst (f' s); monadic_rewrite F False \<top> f f'; F \<longrightarrow> \<not> snd (f s) \<rbrakk>
1102     \<Longrightarrow> (a, b) \<in> fst (f s)"
1103  by (auto simp add: monadic_rewrite_def)
1104
1105lemma ccorres_underlying_Fault:
1106  "\<lbrakk> ccorres_underlying srel Gamma rrefl xf arrel axf G G' hs m c;
1107           \<exists>s. (s, s') \<in> srel \<and> G s \<and> s' \<in> G' \<and> \<not> snd (m s) \<rbrakk>
1108      \<Longrightarrow> \<not> Gamma \<turnstile> \<langle>c, Normal s'\<rangle> \<Rightarrow> Fault ft"
1109  apply clarsimp
1110  apply (erule(4) ccorresE)
1111   apply (erule exec_handlers.EHOther)
1112   apply simp
1113  apply simp
1114  done
1115
1116lemma monadic_rewrite_\<Gamma>:
1117  "monadic_rewrite True False \<top>
1118    (exec_C \<Gamma> c)
1119    (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c)"
1120  using spec_refine [of symbol_table domain]
1121  using spec_simulates_to_exec_simulates
1122  apply (clarsimp simp: spec_statefn_simulates_via_statefn
1123                        o_def map_option_case monadic_rewrite_def exec_C_def
1124                   split: option.splits
1125                   cong: option.case_cong)
1126  apply blast
1127  done
1128
1129lemma no_fail_getActiveIRQ_C:
1130  "\<not>snd (getActiveIRQ_C s)"
1131  apply (clarsimp simp: getActiveIRQ_C_def exec_C_def)
1132  apply (drule getActiveIRQ_Normal)
1133  apply (clarsimp simp: isNormal_def)
1134  done
1135
1136lemma kernel_all_subset_kernel:
1137  "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop)
1138       (kernel_global.kernel_call_C symbol_table fp)
1139       \<subseteq> global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)"
1140  apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def
1141                        relcomp_unfold in_lift_state_relation_eq)
1142  apply (intro conjI)
1143   apply (simp_all add: kernel_global.kernel_call_C_def
1144                    kernel_call_C_def kernelEntry_C_def
1145                    setTCBContext_C_def
1146                    kernel_global.kernelEntry_C_def
1147                     exec_C_Basic
1148                    kernel_global.setTCBContext_C_def
1149                    kernel_call_H_def kernelEntry_def
1150                    getContext_C_def
1151                    check_active_irq_C_def checkActiveIRQ_C_def
1152                    kernel_global.check_active_irq_C_def kernel_global.checkActiveIRQ_C_def
1153                    check_active_irq_H_def checkActiveIRQ_def)
1154       apply clarsimp
1155       apply (erule in_monad_imp_rewriteE[where F=True])
1156        apply (rule monadic_rewrite_imp)
1157         apply (rule monadic_rewrite_bind_tail)+
1158           apply (rule monadic_rewrite_bind_head[where P=\<top>])
1159           apply (simp add: callKernel_C_def callKernel_withFastpath_C_def
1160                            kernel_global.callKernel_C_def
1161                            kernel_global.callKernel_withFastpath_C_def
1162                            handleHypervisorEvent_C_def
1163                       split: event.split if_split)
1164           apply (intro allI impI conjI monadic_rewrite_\<Gamma>)[1]
1165          apply ((wp | simp)+)[3]
1166        apply (clarsimp simp: snd_bind snd_modify in_monad gets_def)
1167       apply clarsimp
1168      apply clarsimp
1169     apply clarsimp
1170    apply (clarsimp simp: in_monad)
1171    apply (erule (1) notE[OF _ in_monad_imp_rewriteE[where F=True]])
1172     apply (simp add: kernel_global.getActiveIRQ_C_def getActiveIRQ_C_def)
1173     apply (rule monadic_rewrite_\<Gamma>)
1174    apply (simp add: no_fail_getActiveIRQ_C)
1175   apply (clarsimp simp: in_monad)
1176   apply (erule (1) notE[OF _ in_monad_imp_rewriteE[where F=True]])
1177    apply (simp add: kernel_global.getActiveIRQ_C_def getActiveIRQ_C_def)
1178    apply (rule monadic_rewrite_\<Gamma>)
1179   apply (simp add: no_fail_getActiveIRQ_C)
1180  apply (clarsimp simp: in_monad)
1181  apply (erule (1) notE[OF _ in_monad_imp_rewriteE[where F=True]])
1182   apply (simp add: kernel_global.getActiveIRQ_C_def getActiveIRQ_C_def)
1183   apply (rule monadic_rewrite_\<Gamma>)
1184  apply (simp add: no_fail_getActiveIRQ_C)
1185  done
1186
1187theorem true_refinement:
1188  "kernel_global.ADT_C symbol_table x64KSKernelVSpace_C uop
1189   \<sqsubseteq> ADT_H uop"
1190  apply (rule refinement_trans[OF _ refinement2])
1191  apply (simp add: kernel_global.ADT_C_def ADT_C_def)
1192  apply (rule sim_imp_refines)
1193  apply (clarsimp simp: fw_simulates_def)
1194  apply (rule_tac x=Id in exI)
1195  using kernel_all_subset_kernel
1196  apply (simp add: fw_sim_def rel_semi_def)
1197  done
1198
1199(* FIXME: fastpath
1200theorem true_fp_refinement:
1201  "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop
1202   \<sqsubseteq> ADT_H uop"
1203  apply (rule refinement_trans[OF _ fp_refinement])
1204  apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def)
1205  apply (rule sim_imp_refines)
1206  apply (clarsimp simp: fw_simulates_def)
1207  apply (rule_tac x=Id in exI)
1208  using kernel_all_subset_kernel
1209  apply (simp add: fw_sim_def rel_semi_def)
1210  done
1211*)
1212
1213end
1214
1215end
1216