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> machine_word \<Rightarrow> errtype \<Rightarrow> bool"
30where
31 "cintr a x err \<equiv> x = scast EXCEPTION_PREEMPTED"
32
33definition
34  replyOnRestart :: "machine_word \<Rightarrow> machine_word 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> machine_word) 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> machine_word
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> machine_word) 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
532lemma injection_handler_whenE:
533  "injection_handler injf (whenE P f)
534    = whenE P (injection_handler injf f)"
535  by (simp add: whenE_def injection_handler_returnOk split: if_split)
536
537lemmas injection_handler_bindE = injection_bindE [OF refl refl]
538lemmas injection_handler_wp = injection_wp [OF refl]
539
540lemma ccorres_injection_handler_csum1:
541  "ccorres (f \<currency> r) xf P P' hs a c
542    \<Longrightarrow> ccorres
543           ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r) xf P P' hs
544           (injection_handler injector a) c"
545  apply (simp add: injection_handler_liftM)
546  apply (erule ccorres_rel_imp)
547  apply (auto split: sum.split)
548  done
549
550lemma ccorres_injection_handler_csum2:
551  "ccorres ((f o injector) \<currency> r) xf P P' hs a c
552    \<Longrightarrow> ccorres (f \<currency> r) xf P P' hs
553            (injection_handler injector a) c"
554  apply (simp add: injection_handler_liftM)
555  apply (erule ccorres_rel_imp)
556  apply (auto split: sum.split)
557  done
558
559definition
560  is_nondet_refinement :: "('a, 's) nondet_monad
561                              \<Rightarrow> ('a, 's) nondet_monad \<Rightarrow> bool"
562where
563 "is_nondet_refinement f g \<equiv> \<forall>s. (snd (f s) \<longrightarrow> snd (g s)) \<and> fst (f s) \<subseteq> fst (g s)"
564
565lemma is_nondet_refinement_refl[simp]:
566  "is_nondet_refinement a a"
567  by (simp add: is_nondet_refinement_def)
568
569lemma is_nondet_refinement_bind:
570  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
571     \<Longrightarrow> is_nondet_refinement (a >>= b) (c >>= d)"
572  apply (clarsimp simp: is_nondet_refinement_def bind_def split_def)
573  apply fast
574  done
575
576lemma is_nondet_refinement_bindE:
577  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
578     \<Longrightarrow> is_nondet_refinement (a >>=E b) (c >>=E d)"
579  apply (simp add: bindE_def)
580  apply (erule is_nondet_refinement_bind)
581  apply (simp add: lift_def split: sum.split)
582  done
583
584lemma ccorres_nondet_refinement:
585  "\<lbrakk> is_nondet_refinement a b;
586       ccorres_underlying sr Gamm rvr xf arrel axf G G' hs a c \<rbrakk>
587     \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G G' hs b c"
588  apply (simp add: ccorres_underlying_def is_nondet_refinement_def
589                   split_def)
590  apply (rule ballI, drule(1) bspec)
591  apply (intro impI)
592  apply (drule mp, blast)
593  apply (elim allEI)
594  apply (clarsimp split: xstate.split_asm)
595  apply blast
596  done
597
598lemma is_nondet_refinement_alternative1:
599  "is_nondet_refinement a (a \<sqinter> b)"
600  by (clarsimp simp add: is_nondet_refinement_def alternative_def)
601
602lemma ccorres_defer:
603  assumes c: "ccorres r xf P P' hs H C"
604  assumes f: "no_fail Q H"
605  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"
606  using c
607  apply (clarsimp simp: ccorres_underlying_def split: xstate.splits)
608  apply (drule (1) bspec)
609  apply clarsimp
610  apply (erule impE)
611   apply (insert f)[1]
612   apply (clarsimp simp: no_fail_def)
613  apply (clarsimp simp: return_def)
614  apply (rule conjI)
615   apply clarsimp
616   apply (rename_tac s)
617   apply (erule_tac x=n in allE)
618   apply (erule_tac x="Normal s" in allE)
619   apply (clarsimp simp: unif_rrel_def)
620  apply fastforce
621  done
622
623lemma no_fail_loadWordUser:
624  "no_fail (pointerInUserData x and K (is_aligned x 3)) (loadWordUser x)"
625  apply (simp add: loadWordUser_def)
626  apply (rule no_fail_pre, wp no_fail_stateAssert)
627  apply simp
628  done
629
630lemma no_fail_getMRs:
631  "no_fail (tcb_at' thread and case_option \<top> valid_ipc_buffer_ptr' buffer)
632           (getMRs thread buffer info)"
633  apply (rule det_wp_no_fail)
634  apply (rule det_wp_getMRs)
635  done
636
637lemma nat_less_4_cases:
638  "(x::nat) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
639  by clarsimp
640
641lemma msgRegisters_scast:
642  "n < unat (scast n_msgRegisters :: machine_word) \<Longrightarrow>
643  unat (scast (index msgRegistersC n)::machine_word) = unat (index msgRegistersC n)"
644  apply (simp add: kernel_all_global_addresses.msgRegisters_def fupdate_def update_def n_msgRegisters_def fcp_beta
645                   Kernel_C.R10_def Kernel_C.R8_def Kernel_C.R9_def Kernel_C.R15_def)
646  by (auto dest!: nat_less_4_cases)
647
648lemma asUser_cur_obj_at':
649  assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
650  shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace>
651          asUser t f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (atcbContextGet (tcbArch tcb))) (ksCurThread s) s\<rbrace>"
652  apply (simp add: asUser_def split_def)
653  apply (wp)
654     apply (rule hoare_lift_Pf2 [where f=ksCurThread])
655      apply (wp threadSet_obj_at'_really_strongest)+
656   apply (clarsimp simp: threadGet_def)
657   apply (wp getObject_tcb_wp)
658  apply clarsimp
659  apply (drule obj_at_ko_at')
660  apply clarsimp
661  apply (rename_tac tcb)
662  apply (rule_tac x=tcb in exI)
663  apply clarsimp
664  apply (drule use_valid, rule f, assumption)
665  apply clarsimp
666  done
667
668lemma asUser_const_rv:
669  assumes f: "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
670  shows "\<lbrace>\<lambda>s. P\<rbrace> asUser t f \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
671  apply (simp add: asUser_def split_def)
672  apply (wp)
673  apply (clarsimp simp: threadGet_def)
674  apply (wp getObject_tcb_wp)
675  apply clarsimp
676  apply (drule obj_at_ko_at')
677  apply clarsimp
678  apply (rename_tac tcb)
679  apply (rule_tac x=tcb in exI)
680  apply clarsimp
681  apply (drule use_valid, rule f, assumption)
682  apply clarsimp
683  done
684
685lemma getMRs_tcbContext:
686  "\<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace>
687  getMRs thread buffer info
688  \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. user_regs (atcbContextGet (tcbArch tcb)) (X64_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace>"
689  apply (rule hoare_assume_pre)
690  apply (elim conjE)
691  apply (thin_tac "thread = t" for t)
692  apply (clarsimp simp add: getMRs_def)
693  apply (wp|wpc)+
694    apply (rule_tac P="n < length x" in hoare_gen_asm)
695    apply (clarsimp simp: nth_append)
696    apply (wp mapM_wp' static_imp_wp)+
697    apply simp
698    apply (rule asUser_cur_obj_at')
699    apply (simp add: getRegister_def msgRegisters_unfold)
700    apply (simp add: mapM_Cons bind_assoc mapM_empty)
701    apply wp
702   apply (wp hoare_drop_imps hoare_vcg_all_lift)
703   apply (wp asUser_cur_obj_at')
704    apply (simp add: getRegister_def msgRegisters_unfold)
705    apply (simp add: mapM_Cons bind_assoc mapM_empty)
706    apply (wp asUser_const_rv)
707   apply clarsimp
708   apply (wp asUser_const_rv)
709  apply (clarsimp simp: n_msgRegisters_def msgRegisters_unfold)
710  apply (simp add: nth_Cons' cur_tcb'_def split: if_split)
711  done
712
713lemma threadGet_tcbIpcBuffer_ccorres [corres]:
714  "ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs
715           (threadGet tcbIPCBuffer tptr)
716           (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr tptr\<rbrace>
717               (\<acute>w_bufferPtr :==
718                  h_val (hrs_mem \<acute>t_hrs)
719                   (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::machine_word ptr)))"
720  apply (rule ccorres_guard_imp2)
721   apply (rule ccorres_add_return2)
722   apply (rule ccorres_pre_threadGet)
723   apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and
724                   P'="{s'. \<exists>ctcb.
725          cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and>
726                 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg)
727   apply (rule allI, rule conseqPre, vcg)
728   apply clarsimp
729   apply (clarsimp simp: return_def typ_heap_simps')
730  apply (clarsimp simp: obj_at'_def ctcb_relation_def)
731  done
732
733(* FIXME: move *)
734lemma ccorres_case_bools:
735  assumes P: "ccorres r xf P P' hs (a True) (c True)"
736  assumes Q: "ccorres r xf Q Q' hs (a False) (c False)"
737  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
738                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'})
739                      hs (a b) (c b)"
740  apply (cases b)
741   apply (auto simp: P Q)
742  done
743
744lemma ccorres_cond_both':
745  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
746  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
747  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
748  shows  "ccorres_underlying sr G r xf arrel axf
749          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
750          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
751          hs
752          (if P then a else b) (Cond P' c d)"
753  apply (rule ccorres_guard_imp2)
754   apply (rule ccorres_if_lhs)
755    apply (rule ccorres_cond_true)
756    apply (erule ac)
757   apply (rule ccorres_cond_false)
758   apply (erule bd)
759  apply clarsimp
760  apply (frule abs[rule_format, OF conjI], simp+)
761  done
762
763lemma pageBitsForSize_32 [simp]:
764  "pageBitsForSize sz < 64"
765  by (cases sz, auto simp: bit_simps)
766
767lemma ccap_relation_frame_tags:
768  "ccap_relation (ArchObjectCap (PageCap v0 v1 mt v2 dev  v3)) cap \<Longrightarrow>
769  cap_get_tag cap = scast cap_frame_cap"
770  by (auto simp: cap_get_tag_isCap_unfolded_H_cap)
771
772(* FIXME: move *)
773lemma ccorres_case_bools':
774  assumes P: "b \<Longrightarrow> ccorres r xf P P' hs (a True) (c True)"
775  assumes Q: "\<not> b \<Longrightarrow> ccorres r xf Q Q' hs (a False) (c False)"
776  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
777                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'})
778                      hs (a b) (c b)"
779  apply (cases b)
780   apply (auto simp: P Q)
781  done
782
783(* FIXME x64: does this need vmrights \<noteq> 0 *)
784lemma capFVMRights_range:
785  "\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow>
786   cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) \<le> 3"
787  by (simp add: cap_frame_cap_lift_def
788                cap_lift_def cap_tag_defs word_and_le1 mask_def)+
789
790lemma dumb_bool_for_all: "(\<forall>x. x) = False"
791  by auto
792
793lemma dumb_bool_split_for_vcg:
794  "\<lbrace>d \<longrightarrow> \<acute>ret__unsigned_long \<noteq> 0\<rbrace> \<inter> \<lbrace>\<not> d \<longrightarrow> \<acute>ret__unsigned_long = 0\<rbrace>
795  = \<lbrace>d = to_bool \<acute>ret__unsigned_long \<rbrace>"
796  by (auto simp: to_bool_def)
797
798lemma ccap_relation_page_is_device:
799  "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v0a v1 mt v2 d v3)) c
800   \<Longrightarrow> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift c) \<noteq> 0) = d"
801   apply (clarsimp simp: ccap_relation_def Let_def map_option_Some_eq2 cap_to_H_def)
802   apply (case_tac z)
803    apply (auto split: if_splits simp: to_bool_def Let_def cap_frame_cap_lift_def)
804   done
805
806lemma lookupIPCBuffer_ccorres[corres]:
807  "ccorres ((=) \<circ> option_to_ptr) ret__ptr_to_unsigned_long_'
808           (tcb_at' t)
809           (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}
810                  \<inter> {s. isReceiver_' s = from_bool isReceiver}) []
811      (lookupIPCBuffer isReceiver t) (Call lookupIPCBuffer_'proc)"
812  apply (cinit lift: thread_' isReceiver_')
813   apply (rule ccorres_split_nothrow)
814       apply simp
815       apply (rule threadGet_tcbIpcBuffer_ccorres)
816      apply ceqv
817     apply (simp add: getThreadBufferSlot_def locateSlot_conv
818                      cte_C_size word_sle_def Collect_True
819                 del: Collect_const)
820     apply ccorres_remove_UNIV_guard
821     apply (rule ccorres_getSlotCap_cte_at)
822     apply (rule ccorres_move_array_assertion_tcb_ctes)
823     apply (ctac (no_vcg))
824       apply csymbr
825       apply (rule_tac b="isArchObjectCap rva \<and> isPageCap (capCap rva)" in ccorres_case_bools')
826        apply simp
827        apply (rule ccorres_cond_false_seq)
828        apply (simp(no_asm))
829        apply csymbr
830        apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools')
831         apply (rule ccorres_cond_true_seq)
832         apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
833          apply vcg
834         apply (rule conseqPre, vcg,
835                clarsimp simp: isCap_simps return_def option_to_ptr_def option_to_0_def)
836        apply (rule ccorres_cond_false_seq)
837        apply simp
838        apply csymbr
839        apply csymbr
840        apply (clarsimp simp: isCap_simps)
841        apply (rule ccorres_guard_imp[where A=\<top> and A'=UNIV],
842                rule ccorres_cond [where R=\<top>])
843            apply (clarsimp simp: from_bool_0 isCap_simps)
844            apply (frule cap_get_tag_isCap_unfolded_H_cap)
845            apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def elim!: ccap_relationE)
846            apply (clarsimp simp: vmrights_to_H_def)
847            apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def
848                             Kernel_C.VMReadWrite_def
849                      split: if_split)
850           apply (frule cap_get_tag_isCap_unfolded_H_cap(18),simp)
851           apply (frule capFVMRights_range) thm pageBitsForSize_spec
852           apply (simp add: cap_frame_cap_lift)
853           apply (clarsimp simp: cap_to_H_def vmrights_to_H_def to_bool_def
854                                 word_le_make_less
855                                 Kernel_C.VMReadWrite_def Kernel_C.VMReadOnly_def
856                                 Kernel_C.VMKernelOnly_def
857                           dest: word_less_cases)
858           apply (rule ccorres_rhs_assoc)+
859           apply csymbr
860           apply csymbr
861           apply csymbr
862           apply csymbr
863           apply csymbr
864           apply csymbr
865           apply (rule ccorres_Guard)
866           apply simp
867           apply (rule ccorres_assert)+
868           apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
869           apply (rule allI, rule conseqPre, vcg)
870           apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps)
871           apply (frule cap_get_tag_isCap_unfolded_H_cap)
872           apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def mask_def elim!: ccap_relationE)
873          apply (ctac add: ccorres_return_C)
874         apply clarsimp
875        apply (frule cap_get_tag_isCap_unfolded_H_cap)
876        apply (clarsimp simp: if_1_0_0 Collect_const_mem isCap_simps word_less_nat_alt
877                              option_to_ptr_def from_bool_0 option_to_0_def ccap_relation_def
878                              c_valid_cap_def cl_valid_cap_def cap_frame_cap_lift)
879       apply (rule ccorres_cond_true_seq)
880       apply simp
881       apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
882       apply (rule allI, rule conseqPre, vcg)
883       apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps
884                             dumb_bool_for_all
885                      split: capability.splits arch_capability.splits bool.splits)
886      apply wpsimp
887     apply (clarsimp simp: if_1_0_0 Collect_const_mem)
888     apply (rule conjI)
889      apply (clarsimp simp: isCap_simps word_less_nat_alt )
890      apply (frule ccap_relation_page_is_device)
891      apply (frule ccap_relation_frame_tags)
892      apply clarsimp
893     apply (rule ccontr)
894     apply clarsimp
895     apply (fastforce simp: cap_get_tag_PageCap_frame
896                            isCap_simps)
897    apply wp
898   apply vcg
899  apply (simp add: word_sle_def Collect_const_mem
900                   tcb_cnode_index_defs tcbSlots cte_level_bits_def
901                   size_of_def)
902  done
903
904
905lemma doMachineOp_pointerInUserData:
906  "\<lbrace>pointerInUserData p\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. pointerInUserData p\<rbrace>"
907  by (simp add: pointerInUserData_def) wp
908
909lemma loadWordUser_wp:
910  "\<lbrace>\<lambda>s. is_aligned p 3 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace>
911    loadWordUser p
912   \<lbrace>P\<rbrace>"
913  apply (simp add: loadWordUser_def loadWord_def stateAssert_def
914                   user_word_at_def valid_def upto0_7_def)
915  apply (clarsimp simp: in_monad in_doMachineOp)
916  done
917
918lemma ccorres_pre_loadWordUser:
919  "(\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow>
920   ccorres r xf (valid_pspace' and K (is_aligned ptr 3) and
921                 (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s))
922     {s. \<forall>v. cslift s (Ptr ptr :: machine_word ptr) = Some v \<longrightarrow>
923               s \<in> Q v} hs
924     (loadWordUser ptr >>= a) c"
925  apply (rule ccorres_guard_imp)
926    apply (rule_tac Q="\<lambda>rv. P rv and user_word_at rv ptr" and Q'=Q in
927          ccorres_symb_exec_l [OF _ loadWordUser_inv loadWordUser_wp])
928     apply (fastforce intro: ccorres_guard_imp)
929    apply simp
930   apply simp
931  apply clarsimp
932  apply (drule(1) user_word_at_cross_over, simp)
933  apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff)
934  done
935
936lemma loadWordUser_user_word_at:
937  "\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>"
938  apply (simp add: loadWordUser_def user_word_at_def
939                   doMachineOp_def split_def)
940  apply wp
941  apply (clarsimp simp: pointerInUserData_def
942                        loadWord_def in_monad
943                        is_aligned_mask upto0_7_def)
944  done
945
946lemma mapM_loadWordUser_user_words_at:
947  "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s)
948              \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace>
949    mapM loadWordUser xs \<lbrace>Q\<rbrace>"
950  apply (induct xs arbitrary: Q)
951   apply (simp add: mapM_def sequence_def)
952   apply wp
953  apply (simp add: mapM_Cons)
954  apply wp
955   apply assumption
956  apply (wp loadWordUser_user_word_at)
957  apply clarsimp
958  apply (drule spec, erule mp)
959  apply clarsimp
960  apply (case_tac x)
961   apply simp
962  apply simp
963  done
964
965
966lemma getMRs_user_word:
967  "\<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info
968      \<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace>
969  getMRs thread (Some buffer) info
970  \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 8 + 8))\<rbrace>"
971  apply (rule hoare_assume_pre)
972  apply (elim conjE)
973  apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y)
974  apply (simp add: getMRs_def)
975  apply wp
976   apply (rule_tac P="length hardwareMRValues = unat n_msgRegisters" in hoare_gen_asm)
977   apply (clarsimp simp: nth_append word_le_nat_alt
978                         word_less_nat_alt word_size
979                         linorder_not_less [symmetric])
980   apply (wp mapM_loadWordUser_user_words_at)
981   apply (wp hoare_vcg_all_lift)
982    apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post)
983     apply wp
984    apply clarsimp
985    defer
986    apply simp
987    apply (wp asUser_const_rv)
988   apply (simp add: msgRegisters_unfold n_msgRegisters_def)
989  apply (erule_tac x="unat i - unat n_msgRegisters" in allE)
990  apply (erule impE)
991   apply (simp add: msgRegisters_unfold
992                    msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
993   apply (drule (1) order_less_le_trans)
994   apply (simp add: word_less_nat_alt word_le_nat_alt)
995  apply (simp add: msgRegisters_unfold
996                   msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
997  apply (simp add: upto_enum_word del: upt_rec_numeral)
998  apply (subst (asm) nth_map)
999   apply (simp del: upt_rec_numeral)
1000   apply (drule (1) order_less_le_trans)
1001   apply (simp add: word_less_nat_alt word_le_nat_alt)
1002  apply (subst (asm) nth_upt)
1003   apply simp
1004   apply (drule (1) order_less_le_trans)
1005   apply (simp add: word_less_nat_alt word_le_nat_alt)
1006  apply (simp add: word_le_nat_alt add.commute add.left_commute mult.commute mult.left_commute
1007                   wordSize_def')
1008  done
1009
1010declare if_split [split]
1011
1012definition
1013  "getMRs_rel args buffer \<equiv> \<lambda>s. \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}"
1014
1015definition
1016  "sysargs_rel args buffer \<equiv>
1017          cur_tcb'
1018          and case_option \<top> valid_ipc_buffer_ptr' buffer
1019          and getMRs_rel args buffer
1020          and (\<lambda>_. length args > unat (scast n_msgRegisters :: machine_word) \<longrightarrow> buffer \<noteq> None)"
1021
1022definition
1023  "sysargs_rel_n args buffer n \<equiv> \<lambda>s. n < length args \<and> (unat (scast n_msgRegisters :: machine_word) \<le> n \<longrightarrow> buffer \<noteq> None)"
1024
1025lemma sysargs_rel_to_n:
1026  "sysargs_rel args buffer s \<Longrightarrow> sysargs_rel_n args buffer n s = (n < length args)"
1027  by (auto simp add: sysargs_rel_def sysargs_rel_n_def)
1028
1029lemma getMRs_rel:
1030  "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and>
1031        case_option \<top> valid_ipc_buffer_ptr' buffer s \<and>
1032        cur_tcb' s\<rbrace>
1033  getMRs thread buffer mi \<lbrace>\<lambda>args. getMRs_rel args buffer\<rbrace>"
1034  apply (simp add: getMRs_rel_def)
1035  apply (rule hoare_pre)
1036   apply (rule_tac x=mi in hoare_vcg_exI)
1037   apply wp
1038   apply (rule_tac Q="\<lambda>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv,s)}" in hoare_strengthen_post)
1039    apply (wp det_result det_wp_getMRs)
1040   apply clarsimp
1041  apply (clarsimp simp: cur_tcb'_def)
1042  done
1043
1044lemma length_msgRegisters:
1045  "length X64_H.msgRegisters = unat (scast n_msgRegisters :: machine_word)"
1046  by (simp add: msgRegisters_unfold n_msgRegisters_def)
1047
1048lemma getMRs_len[simplified]:
1049  "\<lbrace>\<top>\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. length args > unat (scast n_msgRegisters :: machine_word) \<longrightarrow> buffer \<noteq> None\<rbrace>"
1050  apply (simp add: getMRs_def)
1051  apply (cases buffer, simp_all add:hoare_TrueI)
1052  apply (wp asUser_const_rv | simp)+
1053  apply (simp add: length_msgRegisters)
1054  done
1055
1056lemma getMRs_sysargs_rel:
1057  "\<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>
1058  getMRs thread buffer mi \<lbrace>\<lambda>args. sysargs_rel args buffer\<rbrace>"
1059  apply (simp add: sysargs_rel_def)
1060  apply (wp getMRs_rel getMRs_len|simp)+
1061  done
1062
1063lemma ccorres_assume_pre:
1064  assumes "\<And>s. P s \<Longrightarrow> ccorres r xf (P and (\<lambda>s'. s' = s)) P' hs H C"
1065  shows "ccorres r xf P P' hs H C"
1066  apply (clarsimp simp: ccorres_underlying_def)
1067  apply (frule assms)
1068  apply (simp add: ccorres_underlying_def)
1069  apply blast
1070  done
1071
1072lemma getMRs_length:
1073  "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength\<rbrace> getMRs thread buffer mi
1074  \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat (scast n_msgRegisters :: machine_word)) (unat (msgLength mi))
1075            else length args = unat (msgLength mi)\<rbrace>"
1076  apply (cases buffer)
1077   apply (simp add: getMRs_def)
1078   apply (rule hoare_pre, wp)
1079    apply (rule asUser_const_rv)
1080    apply simp
1081    apply (wp mapM_length)
1082   apply (simp add: min_def length_msgRegisters)
1083  apply clarsimp
1084  apply (simp add: getMRs_def)
1085  apply (rule hoare_pre, wp)
1086    apply simp
1087    apply (wp mapM_length asUser_const_rv mapM_length)+
1088  apply (clarsimp simp: length_msgRegisters)
1089  apply (simp add: min_def split: if_splits)
1090  apply (clarsimp simp: word_le_nat_alt)
1091  apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
1092  done
1093
1094lemma index_msgRegisters_less':
1095  "n < 4 \<Longrightarrow> index msgRegistersC n < 0x17"
1096  by (simp add: msgRegistersC_def fupdate_def Arrays.update_def
1097                fcp_beta "StrictC'_register_defs")
1098
1099lemma index_msgRegisters_less:
1100  "n < 4 \<Longrightarrow> index msgRegistersC n <s 0x17"
1101  "n < 4 \<Longrightarrow> index msgRegistersC n < 0x17"
1102  using index_msgRegisters_less'
1103  by (simp_all add: word_sless_msb_less)
1104
1105lemma valid_ipc_buffer_ptr_array:
1106  "valid_ipc_buffer_ptr' (ptr_val p) s \<Longrightarrow> (s, s') \<in> rf_sr
1107    \<Longrightarrow> n \<le> 2 ^ (msg_align_bits - 3)
1108    \<Longrightarrow> n \<noteq> 0
1109    \<Longrightarrow> array_assertion (p :: machine_word ptr) n (hrs_htd (t_hrs_' (globals s')))"
1110  apply (clarsimp simp: valid_ipc_buffer_ptr'_def typ_at_to_obj_at_arches)
1111  apply (drule obj_at_ko_at', clarsimp)
1112  apply (drule rf_sr_heap_user_data_relation)
1113  apply (erule cmap_relationE1)
1114   apply (clarsimp simp: heap_to_user_data_def Let_def)
1115   apply (rule conjI, rule exI, erule ko_at_projectKO_opt)
1116   apply (rule refl)
1117  apply (drule clift_field, rule user_data_C_words_C_fl_ti, simp)
1118  apply (erule clift_array_assertion_imp, simp+)
1119  apply (simp add: field_lvalue_def msg_align_bits)
1120  apply (rule_tac x="unat (ptr_val p && mask pageBits >> 3)" in exI,
1121    simp add: word_shift_by_3 shiftr_shiftl1
1122              is_aligned_andI1[OF is_aligned_weaken])
1123  apply (simp add: add.commute word_plus_and_or_coroll2)
1124  apply (cut_tac a="(ptr_val p && mask pageBits ) >> 3"
1125        and b="2 ^ (pageBits - 3) - 2 ^ (msg_align_bits - 3)" in unat_le_helper)
1126   apply (simp add: pageBits_def msg_align_bits mask_def is_aligned_mask)
1127   apply word_bitwise
1128   apply simp
1129  apply (simp add: msg_align_bits pageBits_def)
1130  done
1131
1132lemma array_assertion_valid_ipc_buffer_ptr_abs:
1133  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (valid_ipc_buffer_ptr' (ptr_val (p s)) s)
1134        \<and> (n s' \<le> 2 ^ (msg_align_bits - 3) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
1135    \<longrightarrow> (x s' = 0 \<or> array_assertion (p s :: machine_word ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))"
1136  apply (intro allI impI disjCI2, clarsimp)
1137  apply (erule(1) valid_ipc_buffer_ptr_array, simp_all)
1138  done
1139
1140lemmas ccorres_move_array_assertion_ipc_buffer
1141    = ccorres_move_array_assertions [OF array_assertion_valid_ipc_buffer_ptr_abs]
1142
1143lemma getSyscallArg_ccorres_foo:
1144  "ccorres (\<lambda>a rv. rv = args ! n) ret__unsigned_long_'
1145         (sysargs_rel args buffer and sysargs_rel_n args buffer n)
1146         (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) []
1147    (return ()) (Call getSyscallArg_'proc)"
1148  apply (rule ccorres_assume_pre)
1149  apply (subst (asm) sysargs_rel_def)
1150  apply (subst (asm) getMRs_rel_def)
1151  apply (subst (asm) pred_conj_def)+
1152  apply (elim conjE exE)
1153  apply (cinit lift: i_' ipc_buffer_')
1154   apply (fold return_def)
1155   apply (rule_tac H="do thread \<leftarrow> gets ksCurThread; getMRs thread buffer mi od" in ccorres_defer)
1156    prefer 2
1157    apply (rule no_fail_pre, wp no_fail_getMRs)
1158    apply assumption
1159   apply (rule ccorres_cond_seq)
1160   apply (rule_tac R=\<top> and P="\<lambda>_. n < unat (scast n_msgRegisters :: machine_word)" in ccorres_cond_both)
1161     apply (simp add: word_less_nat_alt split: if_split)
1162    apply (rule ccorres_add_return2)
1163    apply (rule ccorres_symb_exec_l)
1164       apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: machine_word) \<and>
1165                              obj_at' (\<lambda>tcb. user_regs (atcbContextGet (tcbArch tcb))
1166                                               (X64_H.msgRegisters!n) = x!n) (ksCurThread s) s"
1167                   and P' = UNIV
1168         in ccorres_from_vcg_split_throws)
1169        apply vcg
1170       apply (simp add: return_def del: Collect_const)
1171       apply (rule conseqPre, vcg)
1172       apply (clarsimp simp: rf_sr_ksCurThread)
1173       apply (drule (1) obj_at_cslift_tcb)
1174       apply (clarsimp simp: typ_heap_simps' msgRegisters_scast)
1175       apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
1176                             msgRegisters_ccorres atcbContextGet_def
1177                             carch_tcb_relation_def cregs_relation_def)
1178       apply (subst (asm) msgRegisters_ccorres)
1179        apply (clarsimp simp: n_msgRegisters_def)
1180       apply (simp add: n_msgRegisters_def word_less_nat_alt)
1181       apply (simp add: index_msgRegisters_less unat_less_helper)
1182      apply wp[1]
1183     apply (wp getMRs_tcbContext)
1184    apply simp
1185   apply (rule ccorres_seq_skip [THEN iffD2])
1186   apply (rule ccorres_add_return2)
1187   apply (rule ccorres_symb_exec_l)
1188      apply (rule_tac P="\<lambda>s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s
1189                      \<and> valid_ipc_buffer_ptr' (ptr_val ipc_buffer) s \<and> n < msgMaxLength"
1190                  and P'=UNIV
1191                   in ccorres_from_vcg_throws)
1192      apply (simp add: return_def split del: if_split)
1193      apply (rule allI, rule conseqPre, vcg)
1194      apply (clarsimp split del: if_split)
1195      apply (frule(1) user_word_at_cross_over, rule refl)
1196      apply (clarsimp simp: ptr_add_def mult.commute
1197                            msgMaxLength_def)
1198      apply (safe intro!: disjCI2 elim!: valid_ipc_buffer_ptr_array,
1199        simp_all add: unatSuc2 add.commute msg_align_bits)[1]
1200     apply wp[1]
1201    apply (rule_tac P="\<exists>b. buffer = Some b" in hoare_gen_asm)
1202    apply (clarsimp simp: option_to_ptr_def option_to_0_def)
1203    apply (rule_tac P="\<lambda>s. valid_ipc_buffer_ptr' (ptr_val (Ptr b)) s \<and> i < msgLength mi \<and>
1204                           msgLength mi \<le> msgMaxLength \<and> scast n_msgRegisters \<le> i"
1205                 in hoare_pre(1))
1206     apply (wp getMRs_user_word)
1207    apply (clarsimp simp: msgMaxLength_def unat_less_helper)
1208   apply simp
1209  apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
1210  apply (rule conjI, clarsimp simp: unat_of_nat64 word_bits_def)
1211   apply (drule equalityD2)
1212   apply clarsimp
1213   apply (drule use_valid, rule getMRs_length, assumption)
1214   apply (simp add: n_msgRegisters_def  split: if_split_asm)
1215  apply (rule conjI)
1216   apply (clarsimp simp: option_to_ptr_def option_to_0_def
1217      word_less_nat_alt word_le_nat_alt unat_of_nat64 word_bits_def
1218      n_msgRegisters_def not_less msgMaxLength_def)
1219   apply (drule equalityD2)
1220   apply clarsimp
1221   apply (drule use_valid, rule getMRs_length)
1222    apply (simp add: word_le_nat_alt msgMaxLength_def)
1223   apply (simp split: if_split_asm)
1224  apply (rule conjI, clarsimp simp: cur_tcb'_def)
1225  apply clarsimp
1226  apply (clarsimp simp: bind_def gets_def return_def split_def get_def)
1227  done
1228
1229end
1230
1231context begin interpretation Arch . (*FIXME: arch_split*)
1232
1233lemma invocation_eq_use_type:
1234  "\<lbrakk> value \<equiv> (value' :: 32 signed word);
1235       unat (scast value' :: machine_word) < length (enum :: invocation_label list); (scast value' :: machine_word) \<noteq> 0 \<rbrakk>
1236     \<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: machine_word))"
1237  apply (fold invocation_type_eq, unfold invocationType_def)
1238  apply (simp add: maxBound_is_length Let_def toEnum_def
1239                   nth_eq_iff_index_eq nat_le_Suc_less_imp
1240            split: if_split)
1241  apply (intro impI conjI)
1242   apply (simp add: enum_invocation_label)
1243  apply (subgoal_tac "InvalidInvocation = enum ! 0")
1244   apply (erule ssubst, subst nth_eq_iff_index_eq, simp+)
1245   apply (clarsimp simp add: unat_eq_0)
1246  apply (simp add: enum_invocation_label)
1247  done
1248
1249lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs sel4_arch_invocation_label_defs
1250
1251lemmas invocation_eq_use_types
1252    = all_invocation_label_defs[THEN invocation_eq_use_type, simplified,
1253                            unfolded enum_invocation_label enum_arch_invocation_label, simplified]
1254
1255lemma ccorres_equals_throwError:
1256  "\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk>
1257     \<Longrightarrow> ccorres_underlying sr Gamm rr xf arr axf P P' hs f c"
1258  by simp
1259
1260end
1261
1262end
1263