1(*
2 * Copyright 2014, General Dynamics C4 Systems
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(GD_GPL)
9 *)
10
11theory SyscallArgs_C
12imports
13  TcbQueue_C
14  CSpace_RAB_C
15  StoreWord_C  DetWP
16begin
17
18(*FIXME: arch_split: C kernel names hidden by Haskell names *)
19context kernel_m begin
20abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters"
21lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def
22end
23
24context begin interpretation Arch . (*FIXME: arch_split*)
25
26declare word_neq_0_conv[simp del]
27
28definition
29  cintr :: "irq \<Rightarrow> word32 \<Rightarrow> errtype \<Rightarrow> bool"
30where
31 "cintr a x err \<equiv> x = scast EXCEPTION_PREEMPTED"
32
33definition
34  replyOnRestart :: "word32 \<Rightarrow> word32 list \<Rightarrow> bool \<Rightarrow> unit kernel"
35where
36 "replyOnRestart thread reply isCall \<equiv>
37  do state \<leftarrow> getThreadState thread;
38     when (state = Restart) (do
39       _ \<leftarrow> when isCall (replyFromKernel thread (0, reply));
40       setThreadState Running thread
41     od)
42  od"
43
44crunch typ_at'[wp]: replyOnRestart "\<lambda>s. P (typ_at' T p s)"
45  (wp: crunch_wps simp: crunch_simps)
46
47lemmas replyOnRestart_typ_ats[wp] = typ_at_lifts [OF replyOnRestart_typ_at']
48
49lemma replyOnRestart_invs'[wp]:
50  "\<lbrace>invs'\<rbrace> replyOnRestart thread reply isCall \<lbrace>\<lambda>rv. invs'\<rbrace>"
51  including no_pre
52  apply (simp add: replyOnRestart_def)
53  apply (wp setThreadState_nonqueued_state_update rfk_invs' static_imp_wp)
54  apply (rule hoare_vcg_all_lift)
55  apply (wp setThreadState_nonqueued_state_update rfk_invs' hoare_vcg_all_lift rfk_ksQ)
56   apply (rule hoare_strengthen_post, rule gts_sp')
57  apply (clarsimp simp: pred_tcb_at')
58  apply (auto elim!: pred_tcb'_weakenE st_tcb_ex_cap''
59               dest: st_tcb_at_idle_thread')
60  done
61
62
63declare psubset_singleton[simp]
64
65lemma gts_eq:
66  "st_tcb_at' (\<lambda>st. st = state) t s
67     \<Longrightarrow> (getThreadState t s = return state s)"
68  apply (simp add: prod_eq_iff return_def)
69  apply (subst conj_commute, rule context_conjI)
70   apply (rule no_failD[OF no_fail_getThreadState])
71   apply (erule pred_tcb_at')
72  apply (rule not_psubset_eq)
73   apply clarsimp
74   apply (drule empty_failD [OF empty_fail_getThreadState])
75   apply simp
76  apply clarsimp
77  apply (frule in_inv_by_hoareD[OF gts_inv'])
78  apply (drule use_valid [OF _ gts_sp', OF _ TrueI])
79  apply (clarsimp simp: st_tcb_at'_def obj_at'_def projectKOs objBits_simps)
80  done
81
82lemma replyOnRestart_twice':
83  "((), s') \<in> fst (replyOnRestart t reply isCall s)
84       \<Longrightarrow> replyOnRestart t reply' isCall' s'
85             = return () s'"
86  apply (clarsimp simp add: replyOnRestart_def in_monad)
87  apply (drule use_valid [OF _ gts_sp', OF _ TrueI])
88  apply (case_tac "state = Restart")
89   apply clarsimp
90   apply (drule use_valid [OF _ setThreadState_st_tcb'], simp)
91   apply (simp add: gts_eq when_def cong: bind_apply_cong)
92  apply (simp add: gts_eq when_def cong: bind_apply_cong)
93  done
94
95lemma replyOnRestart_twice[simplified]:
96  "do replyOnRestart t reply isCall; replyOnRestart t reply' isCall'; m od
97   = do replyOnRestart t reply isCall; m od"
98  apply (rule ext)
99  apply (rule bind_apply_cong[OF refl])
100  apply simp
101  apply (subst bind_apply_cong [OF _ refl])
102   apply (erule replyOnRestart_twice')
103  apply simp
104  done
105
106end
107
108context kernel_m begin
109
110lemma ccorres_pre_getWorkUnits:
111  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
112  shows "ccorres r xf
113   (\<lambda>s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> P rv s)
114   {s. \<forall>rv. s \<in> P' rv} hs (getWorkUnits >>= f) c"
115  apply (simp add: getWorkUnits_def)
116  apply (rule ccorres_guard_imp)
117    apply (rule ccorres_symb_exec_l)
118       defer
119       apply wp[1]
120      apply (rule gets_sp)
121     apply (clarsimp simp: empty_fail_def simpler_gets_def)
122    apply assumption
123   apply clarsimp
124   defer
125   apply (rule ccorres_guard_imp)
126     apply (rule cc)
127    apply clarsimp
128   apply assumption
129  apply clarsimp
130  done
131
132lemma preemptionPoint_ccorres:
133  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
134      invs' UNIV []
135      preemptionPoint (Call preemptionPoint_'proc)"
136  apply (cinit simp: workUnitsLimit_def whenE_def)
137   apply (rule ccorres_liftE_Seq)
138   apply (rule ccorres_split_nothrow
139               [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc])
140       apply (rule ccorres_from_vcg)
141       apply (rule allI, rule conseqPre, vcg)
142       apply (clarsimp simp: modifyWorkUnits_def simpler_modify_def)
143       apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
144                             carch_state_relation_def
145                             cmachine_state_relation_def)
146      apply ceqv
147     apply (rule ccorres_liftE_Seq)
148     apply (rule ccorres_pre_getWorkUnits)
149     apply (rule ccorres_cond_seq)
150     apply (rule_tac R="\<lambda>s. rv = ksWorkUnitsCompleted s" in ccorres_cond2)
151       apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
152      prefer 2
153      apply simp
154      apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
155      apply (rule allI, rule conseqPre, vcg)
156      apply (simp add: returnOk_def return_def)
157     apply (rule ccorres_liftE_Seq)
158     apply (rule ccorres_rhs_assoc)+
159     apply (rule ccorres_split_nothrow
160                 [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc])
161         apply (rule ccorres_from_vcg)
162         apply (rule allI, rule conseqPre, vcg)
163         apply (thin_tac "P" for P)+
164         apply (clarsimp simp: setWorkUnits_def simpler_modify_def)
165         apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
166                               carch_state_relation_def
167                               cmachine_state_relation_def)
168        apply ceqv
169       apply (rule ccorres_liftE_Seq)
170       apply (ctac (no_vcg) add: isIRQPending_ccorres)
171        apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
172        apply (rule allI, rule conseqPre, vcg)
173        apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
174                         return_def split: option.splits)
175        apply (clarsimp simp: cintr_def exception_defs)
176       apply wp+
177     apply vcg
178    apply (unfold modifyWorkUnits_def)[1]
179    apply wp
180   apply vcg
181  apply simp
182  done
183
184definition
185  "invocationCatch thread isBlocking isCall inject
186   \<equiv>
187   sum.case_sum (throwError \<circ> Inl)
188    (\<lambda>oper. doE y \<leftarrow> liftE (setThreadState Structures_H.thread_state.Restart thread);
189             reply \<leftarrow> RetypeDecls_H.performInvocation isBlocking isCall (inject oper)
190                           >>= sum.case_sum (throwError \<circ> Inr) returnOk;
191             liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return ()
192                        else replyOnRestart thread reply isCall)
193       odE)"
194
195definition
196  "intr_and_se_rel seOrIRQ status err
197    \<equiv> case seOrIRQ of Inl se \<Rightarrow> syscall_error_rel se status err
198           | Inr irq \<Rightarrow> cintr irq status err"
199
200lemma intr_and_se_rel_simps[simp]:
201  "intr_and_se_rel (Inl se) = syscall_error_rel se"
202  "intr_and_se_rel (Inr irq) = cintr irq"
203  by (rule ext | simp add: intr_and_se_rel_def)+
204
205lemma errstate_globals_overwrite[simp]:
206  "errstate (s \<lparr> globals := globals t \<rparr>) = errstate t"
207  by (simp add: errstate_def)
208
209definition
210  array_to_list :: "('a['b :: finite]) \<Rightarrow> 'a list"
211where
212 "array_to_list arr \<equiv> map (index arr) ([0 ..< card (UNIV :: 'b set)])"
213
214definition
215  interpret_excaps :: "extra_caps_C \<Rightarrow> cte_C ptr list"
216where
217 "interpret_excaps excps \<equiv>
218    (takeWhile (\<lambda>x. ptr_val x \<noteq> 0)
219          (array_to_list (excaprefs_C excps)))"
220
221lemma interpret_excaps_test_null[unfolded array_to_list_def, simplified]:
222  "\<lbrakk> length (interpret_excaps excps) \<ge> n;
223        n < length (array_to_list (excaprefs_C excps)) \<rbrakk>
224     \<Longrightarrow> (index (excaprefs_C excps) n = NULL) = (length (interpret_excaps excps) = n)"
225  apply (simp add: interpret_excaps_def)
226  apply (rule iffI)
227   apply (erule order_antisym[rotated])
228   apply (rule length_takeWhile_le)
229   apply (simp add: array_to_list_def)
230  apply simp
231  apply (drule length_takeWhile_ge)
232  apply (simp add: array_to_list_def NULL_ptr_val)
233  done
234
235definition
236  excaps_map :: "(capability \<times> word32) list
237                     \<Rightarrow> cte_C ptr list"
238where
239 "excaps_map \<equiv> map (\<lambda>(cp, slot). cte_Ptr slot)"
240
241definition
242  slotcap_in_mem :: "capability \<Rightarrow> word32
243                        \<Rightarrow> cte_heap \<Rightarrow> bool"
244where
245 "slotcap_in_mem cap slot
246    \<equiv> \<lambda>cte_heap. \<exists>cte. cte_heap slot = Some cte \<and> cap = cteCap cte"
247
248lemma slotcap_in_mem_def2:
249  "slotcap_in_mem cap slot (ctes_of s)
250    = cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s"
251  by (simp add: slotcap_in_mem_def cte_wp_at_ctes_of)
252
253definition
254  excaps_in_mem :: "(capability \<times> word32) list
255                            \<Rightarrow> cte_heap \<Rightarrow> bool"
256where
257 "excaps_in_mem cps \<equiv> \<lambda>cte_heap.
258     \<forall>(cp, slot) \<in> set cps. slotcap_in_mem cp slot cte_heap"
259
260
261lemma ccorres_alternative1:
262  "ccorres rvr xf P P' hs f c
263     \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c"
264  apply (simp add: ccorres_underlying_def)
265  apply (erule ballEI, clarsimp del: allI)
266  apply (simp add: alternative_def)
267  apply (elim allEI)
268  apply (auto simp: alternative_def split: xstate.split_asm)
269  done
270
271lemma ccorres_alternative2:
272  "ccorres rvr xf P P' hs g c
273     \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c"
274  apply (simp add: ccorres_underlying_def)
275  apply (erule ballEI, clarsimp del: allI)
276  apply (simp add: alternative_def)
277  apply (elim allEI)
278  apply (auto simp: alternative_def split: xstate.split_asm)
279  done
280
281lemma o_xo_injector:
282  "((f o f') \<currency> r) = ((f \<currency> r) o case_sum (Inl o f') Inr)"
283  by (intro ext, simp split: sum.split)
284
285lemma ccorres_invocationCatch_Inr:
286  "ccorres (f \<currency> r) xf P P' hs
287   (invocationCatch thread isBlocking isCall injector (Inr v)) c
288   =
289   ccorres ((f \<circ> Inr) \<currency> r) xf P P' hs
290   (do _ \<leftarrow> setThreadState Restart thread;
291       doE reply \<leftarrow> performInvocation isBlocking isCall (injector v);
292           if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk ()
293                         else liftE (replyOnRestart thread reply isCall)
294       odE od) c"
295  apply (simp add: invocationCatch_def liftE_bindE o_xo_injector)
296  apply (subst ccorres_liftM_simp[symmetric])
297  apply (simp add: liftM_def bind_assoc bindE_def)
298  apply (rule_tac f="\<lambda>f. ccorres rvr xs P P' hs f c" for rvr xs in arg_cong)
299  apply (rule ext)
300  apply (rule bind_apply_cong [OF refl])+
301  apply (simp add: throwError_bind returnOk_bind lift_def liftE_def
302                   alternative_bind
303            split: sum.split if_split)
304  apply (simp add: throwError_def)
305  done
306
307lemma getSlotCap_eq:
308  "slotcap_in_mem cap slot (ctes_of s)
309    \<Longrightarrow> getSlotCap slot s = return cap s"
310  apply (clarsimp simp: slotcap_in_mem_def2 getSlotCap_def)
311  apply (frule cte_wp_at_weakenE'[OF _ TrueI])
312  apply (drule no_failD[OF no_fail_getCTE])
313  apply (clarsimp simp: cte_wp_at'_def getCTE_def[symmetric]
314                        bind_def return_def)
315  done
316
317lemma getSlotCap_ccorres_fudge:
318  "ccorres_underlying sr Gamm rvr xf ar axf P Q hs (do rv \<leftarrow> getSlotCap slot; _ \<leftarrow> assert (rv = cp); a rv od) c
319    \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf
320          (P and (slotcap_in_mem cp slot o ctes_of))
321          Q hs (a cp) c"
322  apply (simp add: ccorres_underlying_def)
323  apply (erule ballEI, clarsimp del: allI)
324  apply (simp add: bind_apply_cong [OF getSlotCap_eq refl]
325             cong: xstate.case_cong)
326  done
327
328lemma getSlotCap_ccorres_fudge_n:
329  "ccorres_underlying sr Gamm rvr xf ar axf P Q hs
330     (do rv \<leftarrow> getSlotCap (snd (vals ! n));
331         _ \<leftarrow> assert (rv = fst (vals ! n)); a od) c
332    \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf
333            ((\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = fst (vals ! n))
334                        (snd (vals ! n)) s \<longrightarrow> P s)
335              and (excaps_in_mem vals \<circ> ctes_of) and K (n < length vals)) Q
336           hs a c"
337  apply (rule ccorres_guard_imp2)
338   apply (erule getSlotCap_ccorres_fudge)
339  apply (clarsimp simp: excaps_in_mem_def)
340  apply (drule bspec, erule nth_mem)
341  apply (clarsimp simp: slotcap_in_mem_def cte_wp_at_ctes_of)
342  done
343
344definition
345 "is_syscall_error_code f code
346    = (\<forall>Q. (\<Gamma> \<turnstile> {s. global_exn_var_'_update (\<lambda>_. Return)
347                      (ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR)
348                        (globals_update (current_syscall_error_'_update f) s)) \<in> Q}
349           code {}, Q))"
350
351abbreviation(input)
352  (* no longer needed *)
353  "Basic_with_globals f == (Basic f)"
354
355lemma is_syscall_error_codes:
356  "is_syscall_error_code f
357       (Basic (globals_update (current_syscall_error_'_update f));;
358        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
359  "is_syscall_error_code (f' o f)
360       (Basic (globals_update (current_syscall_error_'_update f));;
361        Basic (globals_update (current_syscall_error_'_update f'));;
362        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
363  "is_syscall_error_code (f'' o f' o f)
364       (Basic (globals_update (current_syscall_error_'_update f));;
365        Basic (globals_update (current_syscall_error_'_update f'));;
366        Basic (globals_update (current_syscall_error_'_update f''));;
367        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
368  "is_syscall_error_code f
369       (SKIP;;
370        Basic (globals_update (current_syscall_error_'_update f));;
371        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
372  "is_syscall_error_code (f' o f)
373       (SKIP;;
374        Basic (globals_update (current_syscall_error_'_update f));;
375        Basic (globals_update (current_syscall_error_'_update f'));;
376        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
377  "is_syscall_error_code (f'' o f' o f)
378       (SKIP;;
379        Basic (globals_update (current_syscall_error_'_update f));;
380        Basic (globals_update (current_syscall_error_'_update f'));;
381        Basic (globals_update (current_syscall_error_'_update f''));;
382        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
383  "is_syscall_error_code f
384       (Basic_with_globals (globals_update (current_syscall_error_'_update f));;
385        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
386  "is_syscall_error_code (f' o f)
387       (Basic_with_globals (globals_update (current_syscall_error_'_update f));;
388        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
389        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
390  "is_syscall_error_code (f'' o f' o f)
391       (Basic_with_globals (globals_update (current_syscall_error_'_update f));;
392        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
393        Basic_with_globals (globals_update (current_syscall_error_'_update f''));;
394        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
395  "is_syscall_error_code (f'''' \<circ> f''' \<circ> f'' o f' o f)
396       (
397        Basic_with_globals (globals_update (current_syscall_error_'_update f));;
398        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
399        Basic_with_globals (globals_update (current_syscall_error_'_update f''));;
400        Basic_with_globals (globals_update (current_syscall_error_'_update f'''));;
401        Basic_with_globals (globals_update (current_syscall_error_'_update f''''));;
402        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
403  "is_syscall_error_code f
404       (SKIP;;
405        Basic_with_globals (globals_update (current_syscall_error_'_update f));;
406        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
407  "is_syscall_error_code (f' o f)
408       (SKIP;;
409        Basic_with_globals (globals_update (current_syscall_error_'_update f));;
410        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
411        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
412  "is_syscall_error_code (f'' o f' o f)
413       (SKIP;;
414        Basic_with_globals (globals_update (current_syscall_error_'_update f));;
415        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
416        Basic_with_globals (globals_update (current_syscall_error_'_update f''));;
417        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
418  by ((rule iffD2[OF is_syscall_error_code_def], intro allI,
419      rule conseqPre, vcg, safe, (simp_all add: o_def)?)+)
420
421lemma syscall_error_throwError_ccorres_direct:
422  "\<lbrakk> is_syscall_error_code f code;
423     \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk>
424   \<Longrightarrow>
425   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_')
426      \<top> (UNIV) (SKIP # hs)
427      (throwError (Inl err)) code"
428  apply (rule ccorres_from_vcg_throws)
429  apply (rule allI, rule conseqPre)
430  apply (erule iffD1[OF is_syscall_error_code_def, THEN spec])
431  apply (clarsimp simp: throwError_def return_def)
432  apply (simp add: syscall_error_rel_def exception_defs)
433  done
434
435lemma syscall_error_throwError_ccorres_succs:
436  "\<lbrakk> is_syscall_error_code f code;
437     \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk>
438   \<Longrightarrow>
439   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_')
440      \<top> (UNIV) (SKIP # hs)
441      (throwError (Inl err)) (code ;; remainder)"
442  apply (rule ccorres_guard_imp2,
443         rule ccorres_split_throws)
444    apply (erule syscall_error_throwError_ccorres_direct)
445    apply simp
446   apply (rule HoarePartialProps.augment_Faults)
447    apply (erule iffD1[OF is_syscall_error_code_def, THEN spec])
448   apply simp+
449  done
450
451lemmas syscall_error_throwError_ccorres_n =
452    is_syscall_error_codes[THEN syscall_error_throwError_ccorres_direct,
453                           simplified o_apply]
454    is_syscall_error_codes[THEN syscall_error_throwError_ccorres_succs,
455                           simplified o_apply]
456
457definition idButNot :: "'a \<Rightarrow> 'a"
458where "idButNot x = x"
459
460lemma interpret_excaps_test_null2:
461  "n < 3 \<Longrightarrow>
462   (index (excaprefs_C excps) n = NULL)
463      = (length (interpret_excaps excps) \<le> n
464            \<and> index (idButNot excaprefs_C excps) n = NULL)"
465  unfolding idButNot_def
466  apply safe
467  apply (rule ccontr, simp only: linorder_not_le)
468  apply (frule(1) interpret_excaps_test_null [OF order_less_imp_le])
469  apply simp
470  done
471
472lemma interpret_excaps_eq[unfolded array_to_list_def, simplified]:
473  "interpret_excaps excps = xs \<Longrightarrow>
474   \<forall>n < length xs. (index (excaprefs_C excps) n) = (xs ! n)
475         \<and> (length xs < length (array_to_list (excaprefs_C excps))
476              \<longrightarrow> index (excaprefs_C excps) (length xs) = NULL)"
477  apply (clarsimp simp: interpret_excaps_def)
478  apply (drule length_takeWhile_gt)
479  apply (clarsimp simp: nth_append)
480  apply (clarsimp simp: array_to_list_def)
481  apply (frule_tac f=length in arg_cong, subst(asm) length_map,
482         simp(no_asm_use))
483  apply (rule conjI)
484   apply (rule trans, erule map_upt_eq_vals_D, simp)
485   apply (simp add: nth_append)
486  apply clarsimp
487  apply (frule nth_length_takeWhile)
488  apply (rule trans, erule map_upt_eq_vals_D, simp)
489  apply (simp add: nth_append NULL_ptr_val)
490  done
491
492lemma ctes_of_0_contr[elim]:
493  "\<lbrakk> ctes_of s 0 = Some cte; valid_mdb' s \<rbrakk> \<Longrightarrow> P"
494  by (drule(1) ctes_of_not_0, simp)
495
496lemma invocationCatch_use_injection_handler:
497  "(v >>= invocationCatch thread isBlocking isCall injector)
498     = (injection_handler Inl v >>=E
499           (invocationCatch thread isBlocking isCall injector o Inr))"
500  apply (simp add: injection_handler_def handleE'_def
501                   bind_bindE_assoc)
502  apply (rule ext, rule bind_apply_cong [OF refl])
503  apply (simp add: invocationCatch_def return_returnOk
504            split: sum.split)
505  done
506
507lemma injection_handler_returnOk:
508  "injection_handler injector (returnOk v) = returnOk v"
509  by (simp add: returnOk_liftE injection_liftE)
510
511lemma injection_handler_If:
512  "injection_handler injector (If P a b)
513     = If P (injection_handler injector a)
514            (injection_handler injector b)"
515  by (simp split: if_split)
516
517(* FIXME: duplicated in CSpace_All *)
518lemma injection_handler_liftM:
519  "injection_handler f
520    = liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv)"
521  apply (intro ext, simp add: injection_handler_def liftM_def
522                              handleE'_def)
523  apply (rule bind_apply_cong, rule refl)
524  apply (simp add: throwError_def split: sum.split)
525  done
526
527lemma injection_handler_throwError:
528  "injection_handler f (throwError v) = throwError (f v)"
529  by (simp add: injection_handler_def handleE'_def
530                throwError_bind)
531
532lemmas injection_handler_bindE = injection_bindE [OF refl refl]
533lemmas injection_handler_wp = injection_wp [OF refl]
534
535lemma ccorres_injection_handler_csum1:
536  "ccorres (f \<currency> r) xf P P' hs a c
537    \<Longrightarrow> ccorres
538           ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r) xf P P' hs
539           (injection_handler injector a) c"
540  apply (simp add: injection_handler_liftM)
541  apply (erule ccorres_rel_imp)
542  apply (auto split: sum.split)
543  done
544
545lemma ccorres_injection_handler_csum2:
546  "ccorres ((f o injector) \<currency> r) xf P P' hs a c
547    \<Longrightarrow> ccorres (f \<currency> r) xf P P' hs
548            (injection_handler injector a) c"
549  apply (simp add: injection_handler_liftM)
550  apply (erule ccorres_rel_imp)
551  apply (auto split: sum.split)
552  done
553
554definition
555  is_nondet_refinement :: "('a, 's) nondet_monad
556                              \<Rightarrow> ('a, 's) nondet_monad \<Rightarrow> bool"
557where
558 "is_nondet_refinement f g \<equiv> \<forall>s. (snd (f s) \<longrightarrow> snd (g s)) \<and> fst (f s) \<subseteq> fst (g s)"
559
560lemma is_nondet_refinement_refl[simp]:
561  "is_nondet_refinement a a"
562  by (simp add: is_nondet_refinement_def)
563
564lemma is_nondet_refinement_bind:
565  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
566     \<Longrightarrow> is_nondet_refinement (a >>= b) (c >>= d)"
567  apply (clarsimp simp: is_nondet_refinement_def bind_def split_def)
568  apply fast
569  done
570
571lemma is_nondet_refinement_bindE:
572  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
573     \<Longrightarrow> is_nondet_refinement (a >>=E b) (c >>=E d)"
574  apply (simp add: bindE_def)
575  apply (erule is_nondet_refinement_bind)
576  apply (simp add: lift_def split: sum.split)
577  done
578
579lemma ccorres_nondet_refinement:
580  "\<lbrakk> is_nondet_refinement a b;
581       ccorres_underlying sr Gamm rvr xf arrel axf G G' hs a c \<rbrakk>
582     \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G G' hs b c"
583  apply (simp add: ccorres_underlying_def is_nondet_refinement_def
584                   split_def)
585  apply (rule ballI, drule(1) bspec)
586  apply (intro impI)
587  apply (drule mp, blast)
588  apply (elim allEI)
589  apply (clarsimp split: xstate.split_asm)
590  apply blast
591  done
592
593lemma is_nondet_refinement_alternative1:
594  "is_nondet_refinement a (a \<sqinter> b)"
595  by (clarsimp simp add: is_nondet_refinement_def alternative_def)
596
597lemma ccorres_defer:
598  assumes c: "ccorres r xf P P' hs H C"
599  assumes f: "no_fail Q H"
600  shows "ccorres (\<lambda>_. r rv) xf (\<lambda>s. P s \<and> Q s \<and> (P s \<and> Q s \<longrightarrow> fst (H s) = {(rv,s)})) P' hs (return ()) C"
601  using c
602  apply (clarsimp simp: ccorres_underlying_def split: xstate.splits)
603  apply (drule (1) bspec)
604  apply clarsimp
605  apply (erule impE)
606   apply (insert f)[1]
607   apply (clarsimp simp: no_fail_def)
608  apply (clarsimp simp: return_def)
609  apply (rule conjI)
610   apply clarsimp
611   apply (rename_tac s)
612   apply (erule_tac x=n in allE)
613   apply (erule_tac x="Normal s" in allE)
614   apply (clarsimp simp: unif_rrel_def)
615  apply fastforce
616  done
617
618lemma no_fail_loadWordUser:
619  "no_fail (pointerInUserData x and K (is_aligned x 2)) (loadWordUser x)"
620  apply (simp add: loadWordUser_def)
621  apply (rule no_fail_pre, wp no_fail_stateAssert)
622  apply simp
623  done
624
625lemma no_fail_getMRs:
626  "no_fail (tcb_at' thread and case_option \<top> valid_ipc_buffer_ptr' buffer)
627           (getMRs thread buffer info)"
628  apply (rule det_wp_no_fail)
629  apply (rule det_wp_getMRs)
630  done
631
632lemma msgRegisters_scast:
633  "n < unat (scast n_msgRegisters :: word32) \<Longrightarrow>
634  unat (scast (index msgRegistersC n)::word32) = unat (index msgRegistersC n)"
635  apply (simp add: msgRegisters_def fupdate_def update_def n_msgRegisters_def fcp_beta
636                   Kernel_C.R2_def Kernel_C.R3_def Kernel_C.R4_def Kernel_C.R5_def
637                   Kernel_C.R6_def Kernel_C.R7_def)
638  done
639
640lemma asUser_cur_obj_at':
641  assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
642  shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace>
643          asUser t f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (atcbContextGet (tcbArch tcb))) (ksCurThread s) s\<rbrace>"
644  apply (simp add: asUser_def split_def)
645  apply (wp)
646     apply (rule hoare_lift_Pf2 [where f=ksCurThread])
647      apply (wp threadSet_obj_at'_really_strongest)+
648   apply (clarsimp simp: threadGet_def)
649   apply (wp getObject_tcb_wp)
650  apply clarsimp
651  apply (drule obj_at_ko_at')
652  apply clarsimp
653  apply (rename_tac tcb)
654  apply (rule_tac x=tcb in exI)
655  apply clarsimp
656  apply (drule use_valid, rule f, assumption)
657  apply clarsimp
658  done
659
660lemma asUser_const_rv:
661  assumes f: "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
662  shows "\<lbrace>\<lambda>s. P\<rbrace> asUser t f \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
663  apply (simp add: asUser_def split_def)
664  apply (wp)
665  apply (clarsimp simp: threadGet_def)
666  apply (wp getObject_tcb_wp)
667  apply clarsimp
668  apply (drule obj_at_ko_at')
669  apply clarsimp
670  apply (rename_tac tcb)
671  apply (rule_tac x=tcb in exI)
672  apply clarsimp
673  apply (drule use_valid, rule f, assumption)
674  apply clarsimp
675  done
676
677
678lemma getMRs_tcbContext:
679  "\<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace>
680  getMRs thread buffer info
681  \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (ARM_HYP_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace>"
682  apply (rule hoare_assume_pre)
683  apply (elim conjE)
684  apply (thin_tac "thread = t" for t)
685  apply (clarsimp simp add: getMRs_def)
686  apply (wp|wpc)+
687    apply (rule_tac P="n < length x" in hoare_gen_asm)
688    apply (clarsimp simp: nth_append)
689    apply (wp mapM_wp' static_imp_wp)+
690    apply simp
691    apply (rule asUser_cur_obj_at')
692    apply (simp add: getRegister_def msgRegisters_unfold)
693    apply (simp add: mapM_Cons bind_assoc mapM_empty)
694    apply wp
695   apply (wp hoare_drop_imps hoare_vcg_all_lift)
696   apply (wp asUser_cur_obj_at')
697    apply (simp add: getRegister_def msgRegisters_unfold)
698    apply (simp add: mapM_Cons bind_assoc mapM_empty)
699    apply (wp asUser_const_rv)
700   apply clarsimp
701   apply (wp asUser_const_rv)
702  apply (clarsimp simp: n_msgRegisters_def msgRegisters_unfold)
703  apply (simp add: nth_Cons' cur_tcb'_def split: if_split)
704  done
705
706lemma threadGet_tcbIpcBuffer_ccorres [corres]:
707  "ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs
708           (threadGet tcbIPCBuffer tptr)
709           (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr tptr\<rbrace>
710               (\<acute>w_bufferPtr :==
711                  h_val (hrs_mem \<acute>t_hrs)
712                   (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::word32 ptr)))"
713  apply (rule ccorres_guard_imp2)
714   apply (rule ccorres_add_return2)
715   apply (rule ccorres_pre_threadGet)
716   apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and
717                   P'="{s'. \<exists>ctcb.
718          cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and>
719                 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg)
720   apply (rule allI, rule conseqPre, vcg)
721   apply clarsimp
722   apply (clarsimp simp: return_def typ_heap_simps')
723  apply (clarsimp simp: obj_at'_def ctcb_relation_def)
724  done
725
726(* FIXME: move *)
727lemma ccorres_case_bools:
728  assumes P: "ccorres r xf P P' hs (a True) (c True)"
729  assumes Q: "ccorres r xf Q Q' hs (a False) (c False)"
730  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
731                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'})
732                      hs (a b) (c b)"
733  apply (cases b)
734   apply (auto simp: P Q)
735  done
736
737lemma ccorres_cond_both':
738  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
739  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
740  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
741  shows  "ccorres_underlying sr G r xf arrel axf
742          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
743          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
744          hs
745          (if P then a else b) (Cond P' c d)"
746  apply (rule ccorres_guard_imp2)
747   apply (rule ccorres_if_lhs)
748    apply (rule ccorres_cond_true)
749    apply (erule ac)
750   apply (rule ccorres_cond_false)
751   apply (erule bd)
752  apply clarsimp
753  apply (frule abs[rule_format, OF conjI], simp+)
754  done
755
756lemma pageBitsForSize_32 [simp]:
757  "pageBitsForSize sz < 32"
758  by (cases sz, auto)
759
760lemma ccap_relation_frame_tags:
761  "ccap_relation (ArchObjectCap (PageCap dev v0 v1 v2 v3)) cap \<Longrightarrow>
762  cap_get_tag cap = scast cap_frame_cap \<or> cap_get_tag cap = scast cap_small_frame_cap"
763  apply (case_tac "v2 = ARMSmallPage")
764   apply (auto simp: cap_get_tag_isCap_unfolded_H_cap)
765  done
766
767(* FIXME: move *)
768lemma ccorres_case_bools':
769  assumes P: "b \<Longrightarrow> ccorres r xf P P' hs (a True) (c True)"
770  assumes Q: "\<not> b \<Longrightarrow> ccorres r xf Q Q' hs (a False) (c False)"
771  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
772                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'})
773                      hs (a b) (c b)"
774  apply (cases b)
775   apply (auto simp: P Q)
776  done
777
778lemma capFVMRights_range:
779  "\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow>
780   cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) \<le> 3"
781  "\<And>cap. cap_get_tag cap = scast cap_small_frame_cap \<Longrightarrow>
782   cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) \<le> 3"
783  by (simp add: cap_frame_cap_lift_def cap_small_frame_cap_lift_def
784                cap_lift_def cap_tag_defs word_and_le1 mask_def)+
785
786lemma dumb_bool_for_all: "(\<forall>x. x) = False"
787  by auto
788
789lemma dumb_bool_split_for_vcg:
790  "\<lbrace>d \<longrightarrow> \<acute>ret__unsigned_long \<noteq> 0\<rbrace> \<inter> \<lbrace>\<not> d \<longrightarrow> \<acute>ret__unsigned_long = 0\<rbrace>
791  = \<lbrace>d = to_bool \<acute>ret__unsigned_long \<rbrace>"
792  by (auto simp: to_bool_def)
793
794lemma ccap_relation_page_is_device:
795  "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3)) c
796   \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift c) \<noteq> 0) = d"
797   apply (clarsimp simp: ccap_relation_def Let_def map_option_Some_eq2 cap_to_H_def)
798   apply (case_tac z)
799    apply (auto split: if_splits simp: to_bool_def generic_frame_cap_get_capFIsDevice_CL_def Let_def)
800   done
801
802lemma lookupIPCBuffer_ccorres[corres]:
803  "ccorres ((=) \<circ> option_to_ptr) ret__ptr_to_unsigned_long_'
804           (tcb_at' t)
805           (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}
806                  \<inter> {s. isReceiver_' s = from_bool isReceiver}) []
807      (lookupIPCBuffer isReceiver t) (Call lookupIPCBuffer_'proc)"
808  apply (cinit lift: thread_' isReceiver_')
809   apply (rule ccorres_split_nothrow)
810       apply simp
811       apply (rule threadGet_tcbIpcBuffer_ccorres)
812      apply ceqv
813     apply (simp add: getThreadBufferSlot_def locateSlot_conv
814                      cte_C_size word_sle_def Collect_True
815                 del: Collect_const)
816     apply ccorres_remove_UNIV_guard
817     apply (rule ccorres_getSlotCap_cte_at)
818     apply (rule ccorres_move_array_assertion_tcb_ctes
819                 ccorres_move_c_guard_tcb_ctes)+
820     apply (ctac (no_vcg))
821       apply csymbr
822       apply (rule_tac b="isArchObjectCap rva \<and> isPageCap (capCap rva)" in ccorres_case_bools')
823        apply simp
824        apply (rule ccorres_symb_exec_r)
825          apply (rule_tac b="capVPSize (capCap rva) \<noteq> ARMSmallPage" in ccorres_case_bools')
826           apply (rule ccorres_cond_true_seq)
827           apply (rule ccorres_rhs_assoc)+
828           apply csymbr
829           apply csymbr
830           apply (rule ccorres_cond_false_seq)
831           apply (simp(no_asm))
832           apply csymbr
833           apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools')
834            apply (rule ccorres_cond_true_seq)
835            apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
836             apply vcg
837            apply (rule conseqPre, vcg,
838                clarsimp simp: isCap_simps return_def
839                option_to_ptr_def option_to_0_def)
840           apply (rule ccorres_cond_false_seq)
841           apply simp
842           apply csymbr
843           apply (clarsimp simp: isCap_simps)
844           apply (rule ccorres_guard_imp[where A=\<top> and A'=UNIV],
845               rule ccorres_cond [where R=\<top>])
846               apply (clarsimp simp: from_bool_0 isCap_simps)
847               apply (frule ccap_relation_PageCap_generics)
848               apply clarsimp
849               apply (clarsimp simp: vmrights_to_H_def)
850               apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def
851                           Kernel_C.VMReadWrite_def Kernel_C.VMNoAccess_def
852                         split: if_split)
853               apply clarsimp
854               apply (drule less_4_cases)
855               apply auto[1]
856               apply (frule cap_get_tag_isCap_unfolded_H_cap(17),simp)
857               apply (frule capFVMRights_range)
858               apply (simp add: cap_frame_cap_lift
859                               generic_frame_cap_get_capFVMRights_CL_def)
860               apply (clarsimp simp: cap_to_H_def vmrights_to_H_def to_bool_def
861                               word_le_make_less Kernel_C.VMNoAccess_def
862                               Kernel_C.VMReadWrite_def Kernel_C.VMReadOnly_def
863                               Kernel_C.VMKernelOnly_def
864                               dest: word_less_cases)
865              apply (rule ccorres_rhs_assoc)+
866              apply csymbr
867              apply csymbr
868              apply csymbr
869              apply csymbr
870              apply csymbr
871              apply csymbr
872              apply (rule ccorres_Guard)
873              apply simp
874              apply (rule ccorres_assert)+
875              apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
876              apply (rule allI, rule conseqPre, vcg)
877              apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps)
878              apply (clarsimp dest!: ccap_relation_PageCap_generics simp: mask_def)
879             apply (ctac add: ccorres_return_C)
880            apply clarsimp
881           apply (clarsimp simp: if_1_0_0 Collect_const_mem isCap_simps word_less_nat_alt
882              option_to_ptr_def from_bool_0 option_to_0_def dest!:ccap_relation_frame_tags)
883          apply (rule ccorres_cond_false_seq)
884          apply (simp(no_asm))
885          apply (rule ccorres_cond_false_seq)
886          apply (simp(no_asm))
887          apply csymbr
888            apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools')
889             apply (rule ccorres_cond_true_seq)
890             apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
891              apply vcg
892             apply (rule conseqPre, vcg,
893                    clarsimp simp: isCap_simps return_def
894                                   option_to_ptr_def option_to_0_def)
895            apply (rule ccorres_cond_false_seq)
896            apply simp
897            apply csymbr
898            apply (clarsimp simp: isCap_simps)
899            apply (rule ccorres_guard_imp[where A=\<top> and A'=UNIV],
900                rule ccorres_cond [where R=\<top>])
901                apply (clarsimp simp: from_bool_0 isCap_simps)
902                apply (frule ccap_relation_PageCap_generics)
903                apply clarsimp
904                apply (clarsimp simp: vmrights_to_H_def)
905                apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def
906                                 Kernel_C.VMReadWrite_def Kernel_C.VMNoAccess_def
907                          split: if_split)
908                apply clarsimp
909                apply (drule less_4_cases)
910                apply auto[1]
911               apply (frule cap_get_tag_isCap_unfolded_H_cap(16),simp)
912               apply (frule capFVMRights_range)
913               apply (simp add: cap_frame_cap_lift
914                                generic_frame_cap_get_capFVMRights_CL_def)
915                apply (clarsimp simp: cap_to_H_def vmrights_to_H_def to_bool_def
916                                      word_le_make_less Kernel_C.VMNoAccess_def
917                                      Kernel_C.VMReadWrite_def Kernel_C.VMReadOnly_def
918                                      Kernel_C.VMKernelOnly_def
919                                dest: word_less_cases)
920               apply (rule ccorres_rhs_assoc)+
921               apply csymbr
922               apply csymbr
923               apply csymbr
924               apply csymbr
925               apply csymbr
926               apply csymbr
927               apply (rule ccorres_Guard)
928               apply simp
929               apply (rule ccorres_assert)+
930               apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
931               apply (rule allI, rule conseqPre, vcg)
932               apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps)
933               apply (clarsimp dest!: ccap_relation_PageCap_generics simp: mask_def)
934              apply (ctac add: ccorres_return_C)
935             apply clarsimp
936            apply (clarsimp simp: if_1_0_0 Collect_const_mem isCap_simps word_less_nat_alt
937               option_to_ptr_def option_to_0_def dest!:ccap_relation_frame_tags)
938           apply (clarsimp simp: from_bool_0)
939           apply vcg
940          apply clarsimp
941          apply (rule conseqPre, vcg)
942          apply (clarsimp simp: from_bool_0 isCap_simps Collect_const_mem)
943       apply (simp (no_asm))
944       apply (rule ccorres_symb_exec_r)
945         apply (rule ccorres_cond_true_seq)
946         apply (rule ccorres_rhs_assoc)+
947         apply csymbr
948         apply csymbr
949         apply (rule ccorres_cond_true_seq)
950         apply simp
951         apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
952         apply (rule allI, rule conseqPre, vcg)
953         apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps
954                               dumb_bool_for_all
955                        split: capability.splits arch_capability.splits bool.splits)
956
957        apply vcg
958       apply (rule conseqPre, vcg)
959       apply clarsimp
960      apply clarsimp
961      apply wp
962     apply (clarsimp simp: if_1_0_0 Collect_const_mem)
963     apply (rule conjI)
964      apply (clarsimp simp: isCap_simps word_less_nat_alt )
965      apply (frule ccap_relation_page_is_device)
966      apply (frule ccap_relation_PageCap_generics)
967      apply (frule ccap_relation_frame_tags)
968      apply clarsimp
969      apply (rule conjI,clarsimp)
970       apply (simp add: to_bool_neq_0 cap_get_tag_PageCap_small_frame
971                        cap_get_tag_PageCap_frame cap_frame_cap_lift
972                 split: if_splits)
973      apply (erule disjE)
974       apply ((clarsimp simp: cap_small_frame_cap_lift cap_get_tag_PageCap_frame
975                              to_bool_neq_0 cap_get_tag_PageCap_small_frame
976                       split: if_splits)+)[2]
977     apply (rule ccontr)
978     apply clarsimp
979     apply (erule disjE)
980      apply ((fastforce simp: cap_get_tag_PageCap_frame
981                              cap_get_tag_PageCap_small_frame isCap_simps)+)[2]
982    apply wp
983   apply vcg
984  apply (simp add: word_sle_def Collect_const_mem
985                   tcb_cnode_index_defs tcbSlots cte_level_bits_def
986                   size_of_def)
987  done
988
989
990lemma doMachineOp_pointerInUserData:
991  "\<lbrace>pointerInUserData p\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. pointerInUserData p\<rbrace>"
992  by (simp add: pointerInUserData_def) wp
993
994lemma loadWordUser_wp:
995  "\<lbrace>\<lambda>s. is_aligned p 2 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace>
996    loadWordUser p
997   \<lbrace>P\<rbrace>"
998  apply (simp add: loadWordUser_def loadWord_def stateAssert_def
999                   user_word_at_def valid_def)
1000  apply (clarsimp simp: in_monad in_doMachineOp)
1001  done
1002
1003lemma ccorres_pre_loadWordUser:
1004  "(\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow>
1005   ccorres r xf (valid_pspace' and K (is_aligned ptr 2) and
1006                 (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s))
1007     {s. \<forall>v. cslift s (Ptr ptr :: word32 ptr) = Some v \<longrightarrow>
1008               s \<in> Q v} hs
1009     (loadWordUser ptr >>= a) c"
1010  apply (rule ccorres_guard_imp)
1011    apply (rule_tac Q="\<lambda>rv. P rv and user_word_at rv ptr" and Q'=Q in
1012          ccorres_symb_exec_l [OF _ loadWordUser_inv loadWordUser_wp])
1013     apply (fastforce intro: ccorres_guard_imp)
1014    apply simp
1015   apply simp
1016  apply clarsimp
1017  apply (drule(1) user_word_at_cross_over, simp)
1018  apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff)
1019  done
1020
1021lemma loadWordUser_user_word_at:
1022  "\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>"
1023  apply (simp add: loadWordUser_def user_word_at_def
1024                   doMachineOp_def split_def)
1025  apply wp
1026  apply (clarsimp simp: pointerInUserData_def
1027                        loadWord_def in_monad
1028                        is_aligned_mask)
1029  done
1030
1031lemma mapM_loadWordUser_user_words_at:
1032  "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s)
1033              \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace>
1034    mapM loadWordUser xs \<lbrace>Q\<rbrace>"
1035  apply (induct xs arbitrary: Q)
1036   apply (simp add: mapM_def sequence_def)
1037   apply wp
1038  apply (simp add: mapM_Cons)
1039  apply wp
1040   apply assumption
1041  apply (wp loadWordUser_user_word_at)
1042  apply clarsimp
1043  apply (drule spec, erule mp)
1044  apply clarsimp
1045  apply (case_tac x)
1046   apply simp
1047  apply simp
1048  done
1049
1050
1051lemma getMRs_user_word:
1052  "\<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info
1053      \<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace>
1054  getMRs thread (Some buffer) info
1055  \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace>"
1056  apply (rule hoare_assume_pre)
1057  apply (elim conjE)
1058  apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y)
1059  apply (simp add: getMRs_def)
1060  apply wp
1061   apply (rule_tac P="length hardwareMRValues = unat n_msgRegisters" in hoare_gen_asm)
1062   apply (clarsimp simp: nth_append word_le_nat_alt
1063                         word_less_nat_alt word_size
1064                         linorder_not_less [symmetric])
1065   apply (wp mapM_loadWordUser_user_words_at)
1066   apply (wp hoare_vcg_all_lift)
1067    apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post)
1068     apply wp
1069    apply clarsimp
1070    defer
1071    apply simp
1072    apply (wp asUser_const_rv)
1073   apply (simp add: msgRegisters_unfold n_msgRegisters_def)
1074  apply (erule_tac x="unat i - unat n_msgRegisters" in allE)
1075  apply (erule impE)
1076   apply (simp add: msgRegisters_unfold
1077                    msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
1078   apply (drule (1) order_less_le_trans)
1079   apply (simp add: word_less_nat_alt word_le_nat_alt)
1080  apply (simp add: msgRegisters_unfold
1081                   msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
1082  apply (simp add: upto_enum_word del: upt_rec_numeral)
1083  apply (subst (asm) nth_map)
1084   apply (simp del: upt_rec_numeral)
1085   apply (drule (1) order_less_le_trans)
1086   apply (simp add: word_less_nat_alt word_le_nat_alt)
1087  apply (subst (asm) nth_upt)
1088   apply simp
1089   apply (drule (1) order_less_le_trans)
1090   apply (simp add: word_less_nat_alt word_le_nat_alt)
1091  apply (simp add: word_le_nat_alt add.commute add.left_commute mult.commute mult.left_commute
1092                   wordSize_def')
1093  done
1094
1095declare if_split [split]
1096
1097definition
1098  "getMRs_rel args buffer \<equiv> \<lambda>s. \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}"
1099
1100definition
1101  "sysargs_rel args buffer \<equiv>
1102          cur_tcb'
1103          and case_option \<top> valid_ipc_buffer_ptr' buffer
1104          and getMRs_rel args buffer
1105          and (\<lambda>_. length args > unat (scast n_msgRegisters :: word32) \<longrightarrow> buffer \<noteq> None)"
1106
1107definition
1108  "sysargs_rel_n args buffer n \<equiv> \<lambda>s. n < length args \<and> (unat (scast n_msgRegisters :: word32) \<le> n \<longrightarrow> buffer \<noteq> None)"
1109
1110lemma sysargs_rel_to_n:
1111  "sysargs_rel args buffer s \<Longrightarrow> sysargs_rel_n args buffer n s = (n < length args)"
1112  by (auto simp add: sysargs_rel_def sysargs_rel_n_def)
1113
1114lemma getMRs_rel:
1115  "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and>
1116        case_option \<top> valid_ipc_buffer_ptr' buffer s \<and>
1117        cur_tcb' s\<rbrace>
1118  getMRs thread buffer mi \<lbrace>\<lambda>args. getMRs_rel args buffer\<rbrace>"
1119  apply (simp add: getMRs_rel_def)
1120  apply (rule hoare_pre)
1121   apply (rule_tac x=mi in hoare_vcg_exI)
1122   apply wp
1123   apply (rule_tac Q="\<lambda>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv,s)}" in hoare_strengthen_post)
1124    apply (wp det_result det_wp_getMRs)
1125   apply clarsimp
1126  apply (clarsimp simp: cur_tcb'_def)
1127  done
1128
1129lemma length_msgRegisters:
1130  "length ARM_HYP_H.msgRegisters = unat (scast n_msgRegisters :: word32)"
1131  by (simp add: msgRegisters_unfold n_msgRegisters_def)
1132
1133lemma getMRs_len[simplified]:
1134  "\<lbrace>\<top>\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. length args > unat (scast n_msgRegisters :: word32) \<longrightarrow> buffer \<noteq> None\<rbrace>"
1135  apply (simp add: getMRs_def)
1136  apply (cases buffer, simp_all add:hoare_TrueI)
1137  apply (wp asUser_const_rv | simp)+
1138  apply (simp add: length_msgRegisters)
1139  done
1140
1141lemma getMRs_sysargs_rel:
1142  "\<lbrace>(\<lambda>s. thread = ksCurThread s) and cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer and K (msgLength mi \<le> msgMaxLength)\<rbrace>
1143  getMRs thread buffer mi \<lbrace>\<lambda>args. sysargs_rel args buffer\<rbrace>"
1144  apply (simp add: sysargs_rel_def)
1145  apply (wp getMRs_rel getMRs_len|simp)+
1146  done
1147
1148lemma ccorres_assume_pre:
1149  assumes "\<And>s. P s \<Longrightarrow> ccorres r xf (P and (\<lambda>s'. s' = s)) P' hs H C"
1150  shows "ccorres r xf P P' hs H C"
1151  apply (clarsimp simp: ccorres_underlying_def)
1152  apply (frule assms)
1153  apply (simp add: ccorres_underlying_def)
1154  apply blast
1155  done
1156
1157lemma getMRs_length:
1158  "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength\<rbrace> getMRs thread buffer mi
1159  \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat (scast n_msgRegisters :: word32)) (unat (msgLength mi))
1160            else length args = unat (msgLength mi)\<rbrace>"
1161  apply (cases buffer)
1162   apply (simp add: getMRs_def)
1163   apply (rule hoare_pre, wp)
1164    apply (rule asUser_const_rv)
1165    apply simp
1166    apply (wp mapM_length)
1167   apply (simp add: min_def length_msgRegisters)
1168  apply clarsimp
1169  apply (simp add: getMRs_def)
1170  apply (rule hoare_pre, wp)
1171    apply simp
1172    apply (wp mapM_length asUser_const_rv mapM_length)+
1173  apply (clarsimp simp: length_msgRegisters)
1174  apply (simp add: min_def split: if_splits)
1175  apply (clarsimp simp: word_le_nat_alt)
1176  apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
1177  done
1178
1179lemma index_msgRegisters_less':
1180  "n < 4 \<Longrightarrow> index msgRegistersC n < 0x14"
1181  by (simp add: msgRegistersC_def fupdate_def Arrays.update_def
1182                fcp_beta "StrictC'_register_defs")
1183
1184lemma index_msgRegisters_less:
1185  "n < 4 \<Longrightarrow> index msgRegistersC n <s 0x14"
1186  "n < 4 \<Longrightarrow> index msgRegistersC n < 0x14"
1187  using index_msgRegisters_less'
1188  by (simp_all add: word_sless_msb_less)
1189
1190lemma valid_ipc_buffer_ptr_array:
1191  "valid_ipc_buffer_ptr' (ptr_val p) s \<Longrightarrow> (s, s') \<in> rf_sr
1192    \<Longrightarrow> n \<le> 2 ^ (msg_align_bits - 2)
1193    \<Longrightarrow> n \<noteq> 0
1194    \<Longrightarrow> array_assertion (p :: word32 ptr) n (hrs_htd (t_hrs_' (globals s')))"
1195  apply (clarsimp simp: valid_ipc_buffer_ptr'_def typ_at_to_obj_at_arches)
1196  apply (drule obj_at_ko_at', clarsimp)
1197  apply (drule rf_sr_heap_user_data_relation)
1198  apply (erule cmap_relationE1)
1199   apply (clarsimp simp: heap_to_user_data_def Let_def)
1200   apply (rule conjI, rule exI, erule ko_at_projectKO_opt)
1201   apply (rule refl)
1202  apply (drule clift_field, rule user_data_C_words_C_fl_ti, simp)
1203  apply (erule clift_array_assertion_imp, simp+)
1204  apply (simp add: field_lvalue_def msg_align_bits)
1205  apply (rule_tac x="unat (ptr_val p && mask pageBits >> 2)" in exI,
1206    simp add: word_shift_by_2 shiftr_shiftl1
1207              is_aligned_andI1[OF is_aligned_weaken])
1208  apply (simp add: add.commute word_plus_and_or_coroll2)
1209  apply (cut_tac a="(ptr_val p && mask pageBits ) >> 2"
1210        and b="2 ^ (pageBits - 2) - 2 ^ (msg_align_bits - 2)" in unat_le_helper)
1211   apply (simp add: pageBits_def msg_align_bits mask_def is_aligned_mask)
1212   apply word_bitwise
1213   apply simp
1214  apply (simp add: msg_align_bits pageBits_def multiple_mask_trivia)
1215  done
1216
1217lemma array_assertion_valid_ipc_buffer_ptr_abs:
1218  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (valid_ipc_buffer_ptr' (ptr_val (p s)) s)
1219        \<and> (n s' \<le> 2 ^ (msg_align_bits - 2) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
1220    \<longrightarrow> (x s' = 0 \<or> array_assertion (p s :: word32 ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))"
1221  apply (intro allI impI disjCI2, clarsimp)
1222  apply (erule(1) valid_ipc_buffer_ptr_array, simp_all)
1223  done
1224
1225lemmas ccorres_move_array_assertion_ipc_buffer
1226    = ccorres_move_array_assertions [OF array_assertion_valid_ipc_buffer_ptr_abs]
1227
1228lemma getSyscallArg_ccorres_foo:
1229  "ccorres (\<lambda>a rv. rv = args ! n) ret__unsigned_long_'
1230         (sysargs_rel args buffer and sysargs_rel_n args buffer n)
1231         (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) []
1232    (return ()) (Call getSyscallArg_'proc)"
1233  apply (rule ccorres_assume_pre)
1234  apply (subst (asm) sysargs_rel_def)
1235  apply (subst (asm) getMRs_rel_def)
1236  apply (subst (asm) pred_conj_def)+
1237  apply (elim conjE exE)
1238  apply (cinit lift: i_' ipc_buffer_')
1239   apply (fold return_def)
1240   apply (rule_tac H="do thread \<leftarrow> gets ksCurThread; getMRs thread buffer mi od" in ccorres_defer)
1241    prefer 2
1242    apply (rule no_fail_pre, wp no_fail_getMRs)
1243    apply assumption
1244   apply (rule ccorres_cond_seq)
1245   apply (rule_tac R=\<top> and P="\<lambda>_. n < unat (scast n_msgRegisters :: word32)" in ccorres_cond_both)
1246     apply (simp add: word_less_nat_alt split: if_split)
1247    apply (rule ccorres_add_return2)
1248    apply (rule ccorres_symb_exec_l)
1249       apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: word32) \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (ARM_HYP_H.msgRegisters!n) = x!n) (ksCurThread s) s"
1250                   and P' = UNIV
1251         in ccorres_from_vcg_split_throws)
1252        apply vcg
1253       apply (simp add: return_def del: Collect_const)
1254       apply (rule conseqPre, vcg)
1255       apply (clarsimp simp: rf_sr_ksCurThread)
1256       apply (drule (1) obj_at_cslift_tcb)
1257       apply (clarsimp simp: typ_heap_simps' msgRegisters_scast)
1258       apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
1259                             msgRegisters_ccorres atcbContextGet_def
1260                             carch_tcb_relation_def)
1261       apply (subst (asm) msgRegisters_ccorres)
1262        apply (clarsimp simp: n_msgRegisters_def)
1263       apply (simp add: n_msgRegisters_def word_less_nat_alt)
1264       apply (simp add: index_msgRegisters_less unat_less_helper)
1265      apply wp[1]
1266     apply (wp getMRs_tcbContext)
1267    apply simp
1268   apply (rule ccorres_seq_skip [THEN iffD2])
1269   apply (rule ccorres_add_return2)
1270   apply (rule ccorres_symb_exec_l)
1271      apply (rule_tac P="\<lambda>s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s
1272                      \<and> valid_ipc_buffer_ptr' (ptr_val ipc_buffer) s \<and> n < msgMaxLength"
1273                  and P'=UNIV
1274                   in ccorres_from_vcg_throws)
1275      apply (simp add: return_def split del: if_split)
1276      apply (rule allI, rule conseqPre, vcg)
1277      apply (clarsimp split del: if_split)
1278      apply (frule(1) user_word_at_cross_over, rule refl)
1279      apply (clarsimp simp: ptr_add_def mult.commute
1280                            msgMaxLength_def)
1281      apply (safe intro!: disjCI2 elim!: valid_ipc_buffer_ptr_array,
1282        simp_all add: unatSuc2 add.commute msg_align_bits)[1]
1283     apply wp[1]
1284    apply (rule_tac P="\<exists>b. buffer = Some b" in hoare_gen_asm)
1285    apply (clarsimp simp: option_to_ptr_def option_to_0_def)
1286    apply (rule_tac P="\<lambda>s. valid_ipc_buffer_ptr' (ptr_val (Ptr b)) s \<and> i < msgLength mi \<and>
1287                           msgLength mi \<le> msgMaxLength \<and> scast n_msgRegisters \<le> i"
1288                 in hoare_pre(1))
1289     apply (wp getMRs_user_word)
1290    apply (clarsimp simp: msgMaxLength_def unat_less_helper)
1291   apply simp
1292  apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
1293  apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def)
1294   apply (drule equalityD2)
1295   apply clarsimp
1296   apply (drule use_valid, rule getMRs_length, assumption)
1297   apply (simp add: n_msgRegisters_def  split: if_split_asm)
1298  apply (rule conjI)
1299   apply (clarsimp simp: option_to_ptr_def option_to_0_def
1300      word_less_nat_alt word_le_nat_alt unat_of_nat32 word_bits_def
1301      n_msgRegisters_def not_less msgMaxLength_def)
1302   apply (drule equalityD2)
1303   apply clarsimp
1304   apply (drule use_valid, rule getMRs_length)
1305    apply (simp add: word_le_nat_alt msgMaxLength_def)
1306   apply (simp split: if_split_asm)
1307  apply (rule conjI, clarsimp simp: cur_tcb'_def)
1308  apply clarsimp
1309  apply (clarsimp simp: bind_def gets_def return_def split_def get_def)
1310  done
1311
1312end
1313
1314context begin interpretation Arch . (*FIXME: arch_split*)
1315
1316lemma invocation_eq_use_type:
1317  "\<lbrakk> value \<equiv> (value' :: 32 signed word);
1318       unat (scast value' :: word32) < length (enum :: invocation_label list); (scast value' :: word32) \<noteq> 0 \<rbrakk>
1319     \<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: word32))"
1320  apply (fold invocation_type_eq, unfold invocationType_def)
1321  apply (simp add: maxBound_is_length Let_def toEnum_def
1322                   nth_eq_iff_index_eq nat_le_Suc_less_imp
1323            split: if_split)
1324  apply (intro impI conjI)
1325   apply (simp add: enum_invocation_label)
1326  apply (subgoal_tac "InvalidInvocation = enum ! 0")
1327   apply (erule ssubst, subst nth_eq_iff_index_eq, simp+)
1328   apply (clarsimp simp add: unat_eq_0)
1329  apply (simp add: enum_invocation_label)
1330  done
1331
1332lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs sel4_arch_invocation_label_defs
1333
1334lemmas invocation_eq_use_types
1335    = all_invocation_label_defs[THEN invocation_eq_use_type, simplified,
1336                            unfolded enum_invocation_label enum_arch_invocation_label, simplified]
1337
1338lemma ccorres_equals_throwError:
1339  "\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk>
1340     \<Longrightarrow> ccorres_underlying sr Gamm rr xf arr axf P P' hs f c"
1341  by simp
1342
1343end
1344
1345end
1346