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 TcbAcc_C
12imports Ctac_lemmas_C
13begin
14
15context kernel
16begin
17
18lemma ccorres_pre_threadGet:
19  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (g rv) c"
20  shows   "ccorres r xf
21           (\<lambda>s. \<forall>tcb. ko_at' tcb p s \<longrightarrow> P (f tcb) s)
22           ({s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr p) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> P' (f tcb)})
23           hs (threadGet f p >>= (\<lambda>rv. g rv)) c"
24  apply (rule ccorres_guard_imp)
25    apply (rule ccorres_symb_exec_l)
26       defer
27       apply wp[1]
28      apply (rule tg_sp')
29     apply simp
30    apply assumption
31   defer
32   apply (rule ccorres_guard_imp)
33     apply (rule cc)
34    apply clarsimp
35    apply (frule obj_at_ko_at')
36    apply clarsimp
37  apply assumption
38  apply clarsimp
39  apply (frule (1) obj_at_cslift_tcb)
40  apply clarsimp
41  done
42
43
44(* FIXME MOVE *)
45crunch inv'[wp]: archThreadGet P
46  (ignore: getObject)
47
48(* FIXME MOVE near thm tg_sp' *)
49lemma atg_sp':
50  "\<lbrace>P\<rbrace> archThreadGet f p \<lbrace>\<lambda>t. obj_at' (\<lambda>t'. f (tcbArch t') = t) p and P\<rbrace>"
51  including no_pre
52  apply (simp add: archThreadGet_def)
53  apply wp
54  apply (rule hoare_strengthen_post)
55   apply (rule getObject_tcb_sp)
56  apply clarsimp
57  apply (erule obj_at'_weakenE)
58  apply simp
59  done
60
61(* FIXME: MOVE to EmptyFail *)
62lemma empty_fail_archThreadGet [intro!, wp, simp]:
63  "empty_fail (archThreadGet f p)"
64  by (simp add: archThreadGet_def getObject_def split_def)
65
66lemma ccorres_pre_archThreadGet:
67  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (g rv) c"
68  shows   "ccorres r xf
69           (\<lambda>s. \<forall>tcb. ko_at' tcb p s \<longrightarrow> P (f (tcbArch tcb)) s)
70           ({s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr p) = Some ctcb
71                            \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> P' (f (tcbArch tcb))})
72           hs (archThreadGet f p >>= (\<lambda>rv. g rv)) c"
73  apply (rule ccorres_guard_imp)
74    apply (rule ccorres_symb_exec_l)
75       defer
76       apply wp[1]
77      apply (rule atg_sp')
78     apply simp
79    apply assumption
80   defer
81   apply (rule ccorres_guard_imp)
82     apply (rule cc)
83    apply clarsimp
84    apply (frule obj_at_ko_at')
85    apply clarsimp
86  apply assumption
87  apply clarsimp
88  apply (frule (1) obj_at_cslift_tcb)
89  apply clarsimp
90  done
91
92lemma threadGet_eq:
93  "ko_at' tcb thread s \<Longrightarrow> (f tcb, s) \<in> fst (threadGet f thread s)"
94  unfolding threadGet_def
95  apply (simp add: liftM_def in_monad)
96  apply (rule exI [where x = tcb])
97  apply simp
98  apply (subst getObject_eq)
99     apply simp
100    apply (simp add: objBits_simps')
101   apply assumption
102  apply simp
103  done
104
105lemma archThreadGet_eq:
106  "ko_at' tcb thread s \<Longrightarrow> (f (tcbArch tcb), s) \<in> fst (archThreadGet f thread s)"
107  unfolding archThreadGet_def
108  apply (simp add: liftM_def in_monad)
109  apply (rule exI [where x = tcb])
110  apply simp
111  apply (subst getObject_eq)
112     apply simp
113    apply (simp add: objBits_simps')
114   apply assumption
115  apply simp
116  done
117
118lemma get_tsType_ccorres [corres]:
119  "ccorres (\<lambda>r r'. r' = thread_state_to_tsType r) ret__unsigned_' (tcb_at' thread)
120           (UNIV \<inter> {s. thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])}) []
121  (getThreadState thread) (Call thread_state_ptr_get_tsType_'proc)"
122  unfolding getThreadState_def
123  apply (rule ccorres_from_spec_modifies)
124      apply (rule thread_state_ptr_get_tsType_spec)
125     apply (rule thread_state_ptr_get_tsType_modifies)
126    apply simp
127   apply (frule (1) obj_at_cslift_tcb)
128   apply (clarsimp simp: typ_heap_simps)
129  apply (frule (1) obj_at_cslift_tcb)
130  apply (clarsimp simp: typ_heap_simps)
131  apply (rule bexI [rotated, OF threadGet_eq], assumption)
132  apply simp
133  apply (erule ctcb_relation_thread_state_to_tsType)
134  done
135
136lemma threadGet_obj_at2:
137  "\<lbrace>\<top>\<rbrace> threadGet f thread \<lbrace>\<lambda>v. obj_at' (\<lambda>t. f t = v) thread\<rbrace>"
138  apply (rule hoare_post_imp)
139   prefer 2
140   apply (rule tg_sp')
141  apply simp
142  done
143
144lemma register_from_H_less:
145  "register_from_H hr < 20"
146  by (cases hr, simp_all add: "StrictC'_register_defs")
147
148lemma register_from_H_sless:
149  "register_from_H hr <s 20"
150  by (cases hr, simp_all add: "StrictC'_register_defs" word_sless_def word_sle_def)
151
152lemma register_from_H_0_sle[simp]:
153  "0 <=s register_from_H hr"
154  using word_0_sle_from_less[OF order_less_le_trans] register_from_H_less
155  by fastforce
156
157lemma getRegister_ccorres [corres]:
158  "ccorres (=) ret__unsigned_long_' \<top>
159             ({s. thread_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. reg_' s = register_from_H reg}) []
160             (asUser thread (getRegister reg)) (Call getRegister_'proc)"
161  apply (unfold asUser_def)
162  apply (rule ccorres_guard_imp)
163    apply (rule ccorres_symb_exec_l [where Q="\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet o tcbArch) t = u) thread" and
164      Q'="\<lambda>rv. {s. thread_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. reg_' s = register_from_H reg}"])
165       apply (rule ccorres_from_vcg)
166       apply (rule allI, rule conseqPre)
167        apply vcg
168       apply clarsimp
169       apply (drule (1) obj_at_cslift_tcb)
170       apply (clarsimp simp: typ_heap_simps register_from_H_less register_from_H_sless)
171       apply (clarsimp simp: getRegister_def typ_heap_simps)
172       apply (rule_tac x = "((atcbContextGet o tcbArch) ko reg, \<sigma>)" in bexI [rotated])
173        apply (simp add: in_monad' asUser_def select_f_def split_def)
174        apply (subst arg_cong2 [where f = "(\<in>)"])
175          defer
176          apply (rule refl)
177         apply (erule threadSet_eq)
178        apply (clarsimp simp: ctcb_relation_def ccontext_relation_def carch_tcb_relation_def)
179       apply (wp threadGet_obj_at2)+
180   apply simp
181  apply simp
182  apply (erule obj_atE')
183  apply (clarsimp simp: projectKOs )
184  apply (subst fun_upd_idem)
185   apply (case_tac ko)
186   apply clarsimp
187  apply simp
188  done
189
190lemma getRestartPC_ccorres [corres]:
191  "ccorres (=) ret__unsigned_long_' \<top> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> []
192           (asUser thread getRestartPC) (Call getRestartPC_'proc)"
193  unfolding getRestartPC_def
194  apply (cinit')
195   apply (rule ccorres_add_return2, ctac)
196     apply (rule ccorres_return_C, simp+)[1]
197    apply wp
198   apply vcg
199  apply (simp add: scast_id)
200  done
201
202lemma threadSet_corres_lemma:
203  assumes spec: "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. P s\<rbrace> Call f {t. Q s t}"
204  and      mod: "modifies_heap_spec f"
205  and  rl: "\<And>\<sigma> x t ko. \<lbrakk>(\<sigma>, x) \<in> rf_sr; Q x t; x \<in> P'; ko_at' ko thread \<sigma>\<rbrakk>
206             \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := ksPSpace \<sigma>(thread \<mapsto> KOTCB (g ko))\<rparr>,
207                  t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr"
208  and  g:  "\<And>s x. \<lbrakk>tcb_at' thread s; x \<in> P'; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> P x"
209  shows "ccorres dc xfdc (tcb_at' thread) P' [] (threadSet g thread) (Call f)"
210  apply (rule ccorres_Call_call_for_vcg)
211   apply (rule ccorres_from_vcg)
212   apply (rule allI, rule conseqPre)
213   apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. t\<lparr> globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t) \<rparr>\<rparr>"])
214     apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec])
215      apply (rule subset_refl)
216     apply vcg
217    prefer 2
218    apply (rule mod)
219   apply (clarsimp simp: mex_def meq_def)
220  apply clarsimp
221  apply (rule conjI)
222   apply (erule (2) g)
223  apply clarsimp
224   apply (frule obj_at_ko_at')
225   apply clarsimp
226   apply (rule bexI [rotated])
227   apply (erule threadSet_eq)
228   apply simp
229  apply (rule_tac x1 = "t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>" in iffD1 [OF rf_sr_upd], simp_all)[1]
230  apply (erule (3) rl)
231  done
232
233
234lemma threadSet_ccorres_lemma4:
235  "\<lbrakk> \<And>s tcb. \<Gamma> \<turnstile> (Q s tcb) c {s'. (s \<lparr>ksPSpace := ksPSpace s(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr};
236          \<And>s s' tcb tcb'. \<lbrakk> (s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s;
237                             cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb';
238                             ctcb_relation tcb tcb'; P' s ; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb \<rbrakk>
239         \<Longrightarrow> ccorres dc xfdc (obj_at' (P :: tcb \<Rightarrow> bool) thread and P') R hs (threadSet F thread) c"
240  apply (rule ccorres_from_vcg)
241  apply (rule allI)
242  apply (case_tac "obj_at' P thread \<sigma>")
243   apply (drule obj_at_ko_at', clarsimp)
244   apply (rule conseqPre, rule conseqPost)
245      apply assumption
246     apply clarsimp
247     apply (rule rev_bexI, rule threadSet_eq)
248      apply assumption
249     apply simp
250    apply simp
251   apply clarsimp
252   apply (drule(1) obj_at_cslift_tcb, clarsimp)
253  apply simp
254  apply (rule hoare_complete')
255  apply (simp add: cnvalid_def nvalid_def) (* pretty *)
256  done
257
258lemmas threadSet_ccorres_lemma3 = threadSet_ccorres_lemma4[where R=UNIV]
259
260lemmas threadSet_ccorres_lemma2
261    = threadSet_ccorres_lemma3[where P'=\<top>]
262
263lemma ctcb_relation_tcbVCPU:
264  "ctcb_relation t ko' \<Longrightarrow> tcbVCPU_C (tcbArch_C ko') = option_to_ptr (atcbVCPUPtr (tcbArch t))"
265  unfolding ctcb_relation_def carch_tcb_relation_def ccontext_relation_def
266  by clarsimp
267
268lemma is_aligned_tcb_ptr_to_ctcb_ptr:
269  "obj_at' (P :: tcb \<Rightarrow> bool) p s
270     \<Longrightarrow> is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr p)) ctcb_size_bits"
271  apply (clarsimp simp: obj_at'_def objBits_simps' projectKOs
272                        tcb_ptr_to_ctcb_ptr_def ctcb_offset_defs)
273  apply (erule aligned_add_aligned, simp_all add: word_bits_conv)
274  apply (simp add: is_aligned_def)
275  done
276
277lemma valid_tcb'_vcpuE [elim_format]:
278    "valid_tcb' t s \<Longrightarrow> atcbVCPUPtr (tcbArch t) = Some v \<Longrightarrow> vcpu_at' v s"
279    unfolding valid_tcb'_def valid_arch_tcb'_def
280    by auto
281
282lemma sanitiseRegister_spec:
283  "\<forall>s t v r. \<Gamma> \<turnstile> ({s} \<inter> \<lbrace>\<acute>v = v\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H r\<rbrace> \<inter> \<lbrace>\<acute>archInfo = from_bool t\<rbrace>)
284                   Call sanitiseRegister_'proc
285                 \<lbrace>\<acute>ret__unsigned_long = sanitiseRegister t r v\<rbrace>"
286  apply vcg
287  apply (auto simp: C_register_defs sanitiseRegister_def word_0_sle_from_less
288             split: register.split)
289  done
290
291lemma rf_sr_ksArchState_armHSCurVCPU:
292  "(s, s') \<in> rf_sr \<Longrightarrow> cur_vcpu_relation (armHSCurVCPU (ksArchState s)) (armHSCurVCPU_' (globals s')) (armHSVCPUActive_' (globals s'))"
293  by (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def)
294
295lemma ccorres_pre_getCurVCPU:
296  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
297  shows   "ccorres r xf
298                  (\<lambda>s. (\<forall>rv. (armHSCurVCPU \<circ> ksArchState) s = rv \<longrightarrow> P rv s))
299                  {s. \<forall>rv vcpu' act'. armHSCurVCPU_' (globals s) = vcpu' \<and>
300                                      armHSVCPUActive_' (globals s) = act' \<and>
301                                      cur_vcpu_relation rv vcpu' act'
302                                 \<longrightarrow> s \<in> P' rv }
303                          hs (gets (armHSCurVCPU \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
304  apply (rule ccorres_guard_imp)
305    apply (rule ccorres_symb_exec_l)
306       defer
307       apply wp
308      apply (rule hoare_gets_sp)
309     apply (clarsimp simp: empty_fail_def getCurThread_def simpler_gets_def)
310    apply assumption
311   apply clarsimp
312   defer
313   apply (rule ccorres_guard_imp)
314     apply (rule cc)
315    apply clarsimp
316   apply assumption
317  apply (clarsimp simp: rf_sr_ksArchState_armHSCurVCPU)
318  done
319
320lemma getObject_tcb_wp':
321  "\<lbrace>\<lambda>s. \<forall>t. ko_at' (t :: tcb) p s \<longrightarrow> Q t s\<rbrace> getObject p \<lbrace>Q\<rbrace>"
322  by (clarsimp simp: getObject_def valid_def in_monad
323                     split_def objBits_simps' loadObject_default_def
324                     projectKOs obj_at'_def in_magnitude_check)
325
326lemma ccorres_pre_getObject_tcb:
327  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
328  shows   "ccorres r xf
329                  (\<lambda>s. (\<forall>tcb. ko_at' tcb p s \<longrightarrow> P tcb s))
330                  {s. \<forall> tcb tcb'. cslift s (tcb_ptr_to_ctcb_ptr p) = Some tcb' \<and> ctcb_relation tcb tcb'
331                           \<longrightarrow> s \<in> P' tcb}
332                          hs (getObject p >>= (\<lambda>rv :: tcb. f rv)) c"
333  apply (rule ccorres_guard_imp2)
334   apply (rule ccorres_symb_exec_l)
335      apply (rule ccorres_guard_imp2)
336       apply (rule cc)
337      apply (rule conjI)
338       apply (rule_tac Q="ko_at' rv p s" in conjunct1)
339       apply assumption
340      apply assumption
341     apply (wpsimp wp: empty_fail_getObject getObject_tcb_wp')+
342    apply (erule cmap_relationE1[OF cmap_relation_tcb],
343           erule ko_at_projectKO_opt)
344  apply simp
345  done
346
347lemma ccorres_pre_getObject_vcpu:
348  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
349  shows   "ccorres r xf
350                  (\<lambda>s. (\<forall>vcpu. ko_at' vcpu p s \<longrightarrow> P vcpu s))
351                  {s. \<forall> vcpu vcpu'. cslift s (vcpu_Ptr p) = Some vcpu' \<and> cvcpu_relation vcpu vcpu'
352                           \<longrightarrow> s \<in> P' vcpu}
353                          hs (getObject p >>= (\<lambda>rv :: vcpu. f rv)) c"
354  apply (rule ccorres_guard_imp2)
355   apply (rule ccorres_symb_exec_l)
356      apply (rule ccorres_guard_imp2)
357       apply (rule cc)
358      apply (rule conjI)
359       apply (rule_tac Q="ko_at' rv p s" in conjunct1)
360       apply assumption
361      apply assumption
362     apply (wpsimp wp: getVCPU_wp empty_fail_getObject)+
363    apply (erule cmap_relationE1 [OF cmap_relation_vcpu],
364         erule ko_at_projectKO_opt)
365  apply simp
366  done
367
368lemma armHSCurVCPU_update_active_ccorres:
369  "b' = from_bool b \<Longrightarrow> v' = fst v \<Longrightarrow>
370   ccorres dc xfdc (\<lambda>s. armHSCurVCPU (ksArchState s) = Some v) UNIV hs
371      (modifyArchState (armHSCurVCPU_update (\<lambda>_. Some (v', b))))
372      (Basic (\<lambda>s. globals_update (armHSVCPUActive_'_update (\<lambda>_. b')) s))"
373  apply (clarsimp simp: modifyArchState_def)
374  apply (rule ccorres_from_vcg)
375  apply (rule allI, rule conseqPre, vcg)
376  apply (clarsimp simp: bind_def simpler_gets_def from_bool_def simpler_modify_def)
377  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
378  by (clarsimp simp: carch_state_relation_def carch_globals_def cur_vcpu_relation_def
379                     cmachine_state_relation_def from_bool_def
380               split: bool.split)
381
382lemma armHSCurVCPU_update_curv_ccorres:
383  "ccorres dc xfdc (\<lambda>s. ((armHSCurVCPU (ksArchState s)) = Some (v, a)) \<and> v \<noteq> 0 \<and> new \<noteq> 0) UNIV hs
384    (modifyArchState (armHSCurVCPU_update (\<lambda>_. Some (new, a))))
385    (Basic (\<lambda>s. globals_update (armHSCurVCPU_'_update (\<lambda>_. Ptr new)) s))"
386  apply (clarsimp simp: modifyArchState_def)
387  apply (rule ccorres_from_vcg)
388  apply (rule allI, rule conseqPre, vcg)
389  apply (clarsimp simp: bind_def simpler_gets_def simpler_modify_def)
390  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
391  by (clarsimp simp: carch_state_relation_def carch_globals_def cur_vcpu_relation_def
392                     cmachine_state_relation_def from_bool_def true_def false_def
393               split: bool.split)
394
395lemma armHSCurVCPU_update_ccorres:
396  "ccorres dc xfdc (\<lambda>_. cur_vcpu_relation curv vcpu act) UNIV hs
397     (modifyArchState (armHSCurVCPU_update (\<lambda>_. curv)))
398     (Basic (\<lambda>s. globals_update (armHSCurVCPU_'_update (\<lambda>_. vcpu)) s);;
399        Basic (\<lambda>s. globals_update (armHSVCPUActive_'_update (\<lambda>_. act)) s))"
400  apply (clarsimp simp: modifyArchState_def)
401  apply (rule ccorres_from_vcg)
402  apply (rule allI, rule conseqPre, vcg)
403  apply (clarsimp simp: bind_def simpler_gets_def simpler_modify_def)
404  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
405  by (clarsimp simp: carch_state_relation_def carch_globals_def cur_vcpu_relation_def
406                     cmachine_state_relation_def from_bool_def true_def false_def
407               split: bool.split)
408
409lemmas armHSCurVCPU_update_active_ccorres2 = armHSCurVCPU_update_ccorres[where curv="Some (v, b)" for v b]
410
411lemma invs'_HScurVCPU_vcpu_at':
412  "\<lbrakk>invs' s; armHSCurVCPU (ksArchState s) = Some (a, b) \<rbrakk> \<Longrightarrow> vcpu_at' a s"
413by (fastforce dest: invs_arch_state' simp: valid_arch_state'_def vcpu_at_is_vcpu' ko_wp_at'_def split: option.splits)
414
415crunch ksArch[wp]: vcpuDisable, vcpuRestore, vcpuSave, vcpuEnable "\<lambda>s. P (ksArchState s)"
416  (ignore: getObject setObject wp: crunch_wps)
417
418(* FIXME move to Invariants_H *)
419lemma invs_cicd_arch_state' [elim!]:
420  "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_arch_state' s"
421  by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def)
422
423(* FIXME move to Invariants_H *)
424lemma invs_cicd_no_0_obj'[elim!]:
425  "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> no_0_obj' s"
426  by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def)
427
428(* FIXME: move *)
429lemma vcpu_at_ko:
430  "vcpu_at' p s \<Longrightarrow> \<exists>vcpu. ko_at' (vcpu::vcpu) p s"
431  apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs)
432  apply (case_tac ko; simp)
433  apply (rename_tac arch_kernel_object)
434  apply (case_tac arch_kernel_object, auto)[1]
435  done
436
437(* FIXME: move *)
438lemma vcpu_at_c_guard:
439  "\<lbrakk>vcpu_at' p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> c_guard (vcpu_Ptr p)"
440  by (fastforce intro: typ_heap_simps dest!: vcpu_at_ko vcpu_at_rf_sr)
441
442(* FIXME: MOVE, probably to CSpace_RAB  *)
443lemma ccorres_gen_asm2_state:
444  assumes rl: "\<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c"
445  shows "ccorres r xf G (G' \<inter> {s. P s}) hs a c"
446proof (rule ccorres_guard_imp2)
447  show "ccorres r xf G (G' \<inter> {_. \<exists>s. P s}) hs a c"
448    apply (rule ccorres_gen_asm2)
449    apply (erule exE)
450    apply (erule rl)
451    done
452next
453  fix s s'
454  assume "(s, s') \<in> rf_sr" and "G s" and "s' \<in> G' \<inter> {s. P s}"
455  thus "G s \<and> s' \<in> (G' \<inter> {_. \<exists>s. P s})"
456    by (clarsimp elim!: exI simp: Collect_const_mem)
457qed
458
459lemma cap_case_TCBCap2:
460  "(case cap of ThreadCap pd
461                   \<Rightarrow> f pd | _ \<Rightarrow> g)
462   = (if isThreadCap cap
463      then f (capTCBPtr cap)
464      else g)"
465  by (simp add: isCap_simps
466         split: capability.split arch_capability.split)
467
468(* FIXME move *)
469lemma ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState:
470  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
471  shows   "ccorres r xf
472                  (\<lambda>s. (\<forall>rv. (armKSGICVCPUNumListRegs \<circ> ksArchState) s = rv \<longrightarrow> P rv s))
473                  {s. \<forall>rv vcpu' act'. of_nat rv = gic_vcpu_num_list_regs_' (globals s)
474                                 \<longrightarrow> s \<in> P' rv }
475                          hs (gets (armKSGICVCPUNumListRegs \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
476  apply (rule ccorres_guard_imp)
477    apply (rule ccorres_symb_exec_l)
478       defer
479       apply wp[1]
480      apply (rule gets_sp)
481     apply (clarsimp simp: empty_fail_def simpler_gets_def)
482    apply assumption
483   apply clarsimp
484   defer
485   apply (rule ccorres_guard_imp)
486     apply (rule cc)
487    apply clarsimp
488   apply assumption
489  apply (simp add: rf_sr_armKSGICVCPUNumListRegs)
490  done
491
492
493lemma length_of_msgRegisters:
494  "length ARM_HYP_H.msgRegisters = 4"
495  by (auto simp: msgRegisters_unfold)
496
497lemma setMRs_single:
498  "setMRs thread buffer [val] = do y \<leftarrow> asUser thread (setRegister register.R2 val);
499       return 1
500    od"
501  apply (clarsimp simp: setMRs_def length_of_msgRegisters zipWithM_x_def zipWith_def split: option.splits)
502  apply (subst zip_commute, subst zip_singleton)
503   apply (simp add: length_of_msgRegisters length_0_conv[symmetric])
504  apply (clarsimp simp: msgRegisters_unfold sequence_x_def)
505  done
506
507end
508end
509