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 IpcCancel_C
12imports SyscallArgs_C
13begin
14
15context kernel_m
16begin
17
18lemma cready_queues_index_to_C_in_range':
19  assumes prems: "qdom \<le> ucast maxDom" "prio \<le> ucast maxPrio"
20  shows "cready_queues_index_to_C qdom prio < numDomains * numPriorities"
21proof -
22  have P: "unat prio < numPriorities"
23    using prems
24    by (simp add: numPriorities_def seL4_MaxPrio_def Suc_le_lessD unat_le_helper)
25  have Q: "unat qdom < numDomains"
26    using prems
27    by (simp add: numDomains_def maxDom_def Suc_le_lessD unat_le_helper)
28  show ?thesis
29    using mod_lemma[OF _ P, where q="unat qdom" and c=numDomains] Q
30    by (clarsimp simp: cready_queues_index_to_C_def field_simps numDomains_def)
31qed
32
33lemmas cready_queues_index_to_C_in_range
34            = cready_queues_index_to_C_in_range'[unfolded numPriorities_def numDomains_def, simplified]
35
36lemma cready_queues_index_to_C_inj:
37  "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';
38     prio \<le> ucast maxPrio; prio' \<le> ucast maxPrio \<rbrakk> \<Longrightarrow> prio = prio' \<and> qdom = qdom'"
39  apply (rule context_conjI)
40  apply (auto simp: cready_queues_index_to_C_def numPriorities_def
41                    seL4_MaxPrio_def word_le_nat_alt dest: arg_cong[where f="\<lambda>x. x mod 256"])
42  done
43
44lemma cready_queues_index_to_C_distinct:
45  "\<lbrakk> qdom = qdom' \<longrightarrow> prio \<noteq> prio'; prio \<le> ucast maxPrio; prio' \<le> ucast maxPrio \<rbrakk>
46   \<Longrightarrow> cready_queues_index_to_C qdom prio \<noteq> cready_queues_index_to_C qdom' prio'"
47  apply (auto simp: cready_queues_index_to_C_inj)
48  done
49
50lemma cstate_relation_ksReadyQueues_update:
51  "\<lbrakk> cstate_relation hs cs; arr = ksReadyQueues_' cs;
52     sched_queue_relation' (clift (t_hrs_' cs)) v (head_C v') (end_C v');
53     qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk>
54    \<Longrightarrow> cstate_relation (ksReadyQueues_update (\<lambda>qs. qs ((qdom, prio) := v)) hs)
55                        (ksReadyQueues_'_update (\<lambda>_. Arrays.update arr
56                                                        (cready_queues_index_to_C qdom prio) v') cs)"
57  apply (clarsimp simp: cstate_relation_def Let_def
58                        cmachine_state_relation_def
59                        carch_state_relation_def carch_globals_def
60                        cready_queues_relation_def seL4_MinPrio_def minDom_def)
61  apply (frule cready_queues_index_to_C_in_range, assumption)
62  apply clarsimp
63  apply (frule_tac qdom=qdoma and prio=prioa in cready_queues_index_to_C_in_range, assumption)
64  apply (frule cready_queues_index_to_C_distinct, assumption+)
65  apply clarsimp
66  done
67
68lemma cmap_relation_drop_fun_upd:
69  "\<lbrakk> cm x = Some v; \<And>v''. rel v'' v = rel v'' v' \<rbrakk>
70      \<Longrightarrow> cmap_relation am (cm (x \<mapsto> v')) f rel
71            = cmap_relation am cm f rel"
72  apply (simp add: cmap_relation_def)
73  apply (rule conj_cong[OF refl])
74  apply (rule ball_cong[OF refl])
75  apply (auto split: if_split)
76  done
77
78lemma valid_queuesD':
79  "\<lbrakk> obj_at' (inQ d p) t s; valid_queues' s \<rbrakk>
80        \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p))"
81  by (simp add: valid_queues'_def)
82
83lemma invs_valid_queues'[elim!]:
84  "invs' s \<Longrightarrow> valid_queues' s"
85  by (simp add: invs'_def valid_state'_def)
86
87
88lemma ntfn_ptr_get_queue_spec:
89  "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> \<sigma> \<Turnstile>\<^sub>c \<^bsup>\<sigma>\<^esup>ntfnPtr} \<acute>ret__struct_tcb_queue_C :== PROC ntfn_ptr_get_queue(\<acute>ntfnPtr)
90       \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr)))) \<and>
91        end_C \<acute>ret__struct_tcb_queue_C = Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr))))\<rbrace>"
92  apply vcg
93  apply clarsimp
94  done
95
96(* Although tcb_C contains an user_fpu_state_C field,
97   none of the uses of this abbreviation involve modifying
98   any user_fpu_state_C within a tcb_C.
99   It is therefore convenient to include user_fpu_state_C here
100   to cover preservation of the global FPU null state. *)
101abbreviation
102  "cslift_all_but_tcb_C s t \<equiv> (cslift s :: cte_C typ_heap) = cslift t
103          \<and> (cslift s :: endpoint_C typ_heap) = cslift t
104          \<and> (cslift s :: notification_C typ_heap) = cslift t
105          \<and> (cslift s :: asid_pool_C typ_heap) = cslift t
106          \<and> (cslift s :: pte_C typ_heap) = cslift t
107          \<and> (cslift s :: pde_C typ_heap) = cslift t
108          \<and> (cslift s :: pdpte_C typ_heap) = cslift t
109          \<and> (cslift s :: pml4e_C typ_heap) = cslift t
110          \<and> (cslift s :: user_data_C typ_heap) = cslift t
111          \<and> (cslift s :: user_data_device_C typ_heap) = cslift t
112          \<and> (cslift s :: ioport_table_C typ_heap) = cslift t
113          \<and> (cslift s :: user_fpu_state_C typ_heap) = cslift t"
114
115lemma tcbEPDequeue_spec:
116  "\<forall>s queue. \<Gamma> \<turnstile> \<lbrace>s. \<exists>t. (t, s) \<in> rf_sr
117               \<and> (\<forall>tcb\<in>set queue. tcb_at' tcb t) \<and> distinct queue
118               \<and> (ctcb_ptr_to_tcb_ptr \<acute>tcb \<in> set queue)
119               \<and> ep_queue_relation' (cslift s) queue (head_C \<acute>queue) (end_C \<acute>queue) \<rbrace>
120            Call tcbEPDequeue_'proc
121            {t. (head_C (ret__struct_tcb_queue_C_' t) =
122                 (if (tcbEPPrev_C (the (cslift s (\<^bsup>s\<^esup>tcb)))) = NULL then
123                    (tcbEPNext_C (the (cslift s (\<^bsup>s\<^esup>tcb))))
124                 else
125                    (head_C \<^bsup>s\<^esup>queue)))
126              \<and> (end_C (ret__struct_tcb_queue_C_' t) =
127                 (if (tcbEPNext_C (the (cslift s (\<^bsup>s\<^esup>tcb)))) = NULL then
128                    (tcbEPPrev_C (the (cslift s (\<^bsup>s\<^esup>tcb))))
129                 else
130                    (end_C \<^bsup>s\<^esup>queue)))
131              \<and> (ep_queue_relation' (cslift t)
132                                    (Lib.delete (ctcb_ptr_to_tcb_ptr \<^bsup>s\<^esup>tcb) queue)
133                                    (head_C (ret__struct_tcb_queue_C_' t))
134                                    (end_C (ret__struct_tcb_queue_C_' t))
135                \<and> (cslift t |` (- tcb_ptr_to_ctcb_ptr ` set queue)) =
136                  (cslift s |` (- tcb_ptr_to_ctcb_ptr ` set queue))
137                \<and> option_map tcb_null_ep_ptrs \<circ> (cslift t) =
138                  option_map tcb_null_ep_ptrs \<circ> (cslift s))
139                \<and> cslift_all_but_tcb_C t s
140                \<and> (\<forall>rs. zero_ranges_are_zero rs (\<^bsup>t\<^esup>t_hrs)
141                    = zero_ranges_are_zero rs (\<^bsup>s\<^esup>t_hrs))
142                \<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}"
143  apply (intro allI)
144  apply (rule conseqPre)
145  apply vcg
146  apply (clarsimp split del: if_split)
147  apply (frule (4) tcb_queue_valid_ptrsD [OF _ _ _ _ tcb_queue_relation'_queue_rel])
148  apply (elim conjE exE)
149  apply (frule (3) tcbEPDequeue_update)
150   apply simp
151  apply (unfold upd_unless_null_def)
152  apply (frule (2) tcb_queue_relation_ptr_rel' [OF tcb_queue_relation'_queue_rel])
153    prefer 2
154    apply assumption
155   apply simp
156  apply (frule c_guard_clift)
157  apply (simp add: typ_heap_simps')
158  apply (intro allI conjI impI)
159            apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff)
160           apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff
161                           cong: if_weak_cong)
162          apply (rule ext)
163          apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def)
164         apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff c_guard_clift)
165        apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff)
166       apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def
167                       cong: if_weak_cong)
168      apply (rule ext)
169      apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def)
170     apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff c_guard_clift)
171    apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff
172                    cong: if_weak_cong)
173   apply (rule ext)
174   apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def)
175  apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff c_guard_clift)
176  done
177
178lemma ntfn_ptr_set_queue_spec:
179  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>ntfnPtr\<rbrace> Call ntfn_ptr_set_queue_'proc
180           {t. (\<exists>ntfn'. notification_lift ntfn' =
181  (notification_lift (the (cslift s (\<^bsup>s\<^esup>ntfnPtr))))\<lparr>
182    ntfnQueue_head_CL := sign_extend 47 (ptr_val (head_C \<^bsup>s\<^esup>ntfn_queue)),
183    ntfnQueue_tail_CL := sign_extend 47 (ptr_val (end_C \<^bsup>s\<^esup>ntfn_queue)) \<rparr>
184            \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>ntfnPtr) ntfn')
185                (t_hrs_' (globals s)))}"
186  apply (rule allI, rule conseqPre, vcg)
187  apply (clarsimp simp: packed_heap_update_collapse_hrs typ_heap_simps')
188  done
189
190
191lemma cancelSignal_ccorres_helper:
192  "ccorres dc xfdc (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn)
193        UNIV
194        []
195        (setNotification ntfn (ntfnObj_update
196          (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfn')) = []
197           then ntfn.IdleNtfn
198           else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfn'))) (ntfnObj ntfn')) ntfn'))
199        (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue(Ptr ntfn);;
200         \<acute>ntfn_queue :== CALL tcbEPDequeue(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);;
201         CALL ntfn_ptr_set_queue(Ptr ntfn,\<acute>ntfn_queue);;
202         IF head_C \<acute>ntfn_queue = NULL THEN
203           CALL notification_ptr_set_state(Ptr ntfn,
204           scast NtfnState_Idle)
205         FI)"
206  apply (rule ccorres_from_vcg)
207  apply (rule allI, rule conseqPre, vcg)
208  apply (clarsimp split del: if_split)
209  apply (frule (2) ntfn_blocked_in_queueD)
210  apply (frule (1) ko_at_valid_ntfn' [OF _ invs_valid_objs'])
211  apply (elim conjE)
212  apply (frule (1) valid_ntfn_isWaitingNtfnD)
213  apply (elim conjE)
214  apply (frule cmap_relation_ntfn)
215  apply (erule (1) cmap_relation_ko_atE)
216  apply (rule conjI)
217   apply (erule h_t_valid_clift)
218  apply (rule impI)
219  apply (rule exI)
220  apply (rule conjI)
221   apply (rule_tac x = \<sigma> in exI)
222   apply (intro conjI, assumption+)
223   apply (drule (2) ntfn_to_ep_queue)
224   apply (simp add: tcb_queue_relation'_def)
225  apply (clarsimp simp: typ_heap_simps cong: imp_cong split del: if_split)
226  apply (frule null_ep_queue [simplified Fun.comp_def])
227  apply (intro impI conjI allI)
228   \<comment> \<open>empty case\<close>
229   apply clarsimp
230   apply (frule iffD1 [OF tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel]])
231     apply (rule ballI, erule bspec)
232     apply (erule subsetD [rotated])
233     apply clarsimp
234    apply simp
235   apply (simp add: setNotification_def split_def)
236   apply (rule bexI [OF _ setObject_eq])
237       apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
238                        cpspace_relation_def update_ntfn_map_tos
239                        typ_heap_simps')
240       apply (elim conjE)
241       apply (intro conjI)
242            \<comment> \<open>tcb relation\<close>
243            apply (erule ctcb_relation_null_queue_ptrs)
244            apply (clarsimp simp: comp_def)
245           \<comment> \<open>ep relation\<close>
246           apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
247           apply simp
248           apply (rule cendpoint_relation_ntfn_queue [OF invs_sym'], assumption+)
249           apply simp
250           apply (erule (1) map_to_ko_atI')
251          \<comment> \<open>ntfn relation\<close>
252          apply (rule cpspace_relation_ntfn_update_ntfn, assumption+)
253          apply (simp add: cnotification_relation_def Let_def NtfnState_Idle_def)
254          apply (simp add: carch_state_relation_def carch_globals_def)
255         \<comment> \<open>queue relation\<close>
256         apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
257         apply (clarsimp simp: comp_def)
258        apply (clarsimp simp: carch_state_relation_def carch_globals_def
259                              typ_heap_simps' packed_heap_update_collapse_hrs
260                              fpu_null_state_heap_update_tag_disj_simps
261                       elim!: fpu_null_state_typ_heap_preservation)
262       apply (simp add: cmachine_state_relation_def)
263      apply (simp add: h_t_valid_clift_Some_iff)
264     apply (simp add: objBits_simps')
265    apply (simp add: objBits_simps)
266   apply assumption
267  \<comment> \<open>non empty case\<close>
268  apply (frule tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel])
269   apply (rule ballI, erule bspec)
270   apply (erule subsetD [rotated])
271   apply clarsimp
272  apply (simp add: setNotification_def split_def)
273  apply (rule bexI [OF _ setObject_eq])
274      apply (frule (1) st_tcb_at_h_t_valid)
275      apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
276                       cpspace_relation_def update_ntfn_map_tos
277                       typ_heap_simps')
278      apply (elim conjE)
279      apply (intro conjI)
280           \<comment> \<open>tcb relation\<close>
281           apply (erule ctcb_relation_null_queue_ptrs)
282           apply (clarsimp simp: comp_def)
283          \<comment> \<open>ep relation\<close>
284          apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
285          apply simp
286          apply (rule cendpoint_relation_ntfn_queue)
287              apply fastforce
288             apply assumption+
289          apply simp
290          apply (erule (1) map_to_ko_atI')
291         \<comment> \<open>ntfn relation\<close>
292         apply (rule cpspace_relation_ntfn_update_ntfn, assumption+)
293          apply (simp add: cnotification_relation_def Let_def isWaitingNtfn_def
294                    split: ntfn.splits split del: if_split)
295          apply (erule iffD1 [OF tcb_queue_relation'_cong [OF refl _ _ refl], rotated -1])
296           apply (clarsimp simp add: h_t_valid_clift_Some_iff)
297           apply (subst tcb_queue_relation'_next_sign; assumption?)
298            apply fastforce
299           apply (simp add: notification_lift_def sign_extend_sign_extend_eq)
300          apply (clarsimp simp: h_t_valid_clift_Some_iff notification_lift_def sign_extend_sign_extend_eq)
301          apply (subst tcb_queue_relation'_prev_sign; assumption?)
302           apply fastforce
303          apply simp
304         apply simp
305        \<comment> \<open>queue relation\<close>
306        apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
307        apply (clarsimp simp: comp_def)
308       subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def
309                                  fpu_null_state_heap_update_tag_disj_simps
310                                  global_ioport_bitmap_heap_update_tag_disj_simps
311                           elim!: fpu_null_state_typ_heap_preservation)
312      subgoal by (simp add: cmachine_state_relation_def)
313     subgoal by (simp add: h_t_valid_clift_Some_iff)
314    subgoal by (simp add: objBits_simps')
315   subgoal by (simp add: objBits_simps)
316  by assumption
317
318lemmas rf_sr_tcb_update_no_queue_gen
319    = rf_sr_tcb_update_no_queue[where t="t''\<lparr> globals := gs \<lparr> t_hrs_' := th \<rparr>\<rparr>" for th, simplified]
320
321lemma threadSet_tcbState_simple_corres:
322  "ccorres dc xfdc (tcb_at' thread)
323        {s. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := v64_' s && mask 4\<rparr>, fl)) \<and>
324           thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} []
325        (threadSet (tcbState_update (\<lambda>_. st)) thread)  (Call thread_state_ptr_set_tsType_'proc)"
326  apply (rule threadSet_corres_lemma)
327  apply (rule thread_state_ptr_set_tsType_spec)
328  apply (rule thread_state_ptr_set_tsType_modifies)
329   apply clarsimp
330   apply (frule (1) obj_at_cslift_tcb)
331   apply (clarsimp simp: typ_heap_simps')
332   apply (rule rf_sr_tcb_update_no_queue_gen, assumption+, simp, simp_all)
333    apply (rule ball_tcb_cte_casesI, simp_all)
334    apply (frule cmap_relation_tcb)
335    apply (frule (1) cmap_relation_ko_atD)
336    apply clarsimp
337    apply (simp add: ctcb_relation_def cthread_state_relation_def)
338  apply (frule (1) obj_at_cslift_tcb)
339  apply (clarsimp simp: typ_heap_simps)
340  done
341
342lemma ko_at_obj_congD':
343  "\<lbrakk>ko_at' k p s; ko_at' k' p s\<rbrakk> \<Longrightarrow> k = k'"
344  apply (erule obj_atE')+
345  apply simp
346  done
347
348lemma threadGet_vcg_corres_P:
349  assumes c: "\<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr
350                       \<and> tcb_at' thread \<sigma> \<and> P \<sigma>
351                       \<and> (\<forall>tcb. ko_at' tcb thread \<sigma> \<longrightarrow> (\<exists>tcb'.
352                       x = f tcb \<and> cslift s (tcb_ptr_to_ctcb_ptr thread) = Some tcb'
353                       \<and> ctcb_relation tcb tcb'))} c {s. (\<sigma>, s) \<in> rf_sr \<and> r x (xf s)}"
354  shows "ccorres r xf P UNIV hs (threadGet f thread) c"
355  apply (rule ccorres_add_return2)
356  apply (rule ccorres_guard_imp2)
357  apply (rule ccorres_pre_threadGet)
358  apply (rule_tac P = "\<lambda>\<sigma>. \<exists>tcb. ko_at' tcb thread \<sigma> \<and> x = f tcb \<and> P \<sigma>"
359    and P' = UNIV in ccorres_from_vcg)
360   apply (simp add: return_def)
361   apply (rule allI, rule conseqPre)
362   apply (rule spec [OF c])
363   apply clarsimp
364   apply (frule cmap_relation_tcb)
365   apply (frule (1) cmap_relation_ko_atD)
366   apply clarsimp
367   apply (rule conjI)
368    apply (erule obj_at'_weakenE)
369    apply simp
370   apply clarsimp
371   apply (drule (1) ko_at_obj_congD')
372   apply simp
373  apply fastforce
374  done
375
376lemmas threadGet_vcg_corres = threadGet_vcg_corres_P[where P=\<top>]
377
378lemma threadGet_specs_corres:
379  assumes spec: "\<forall>s. \<Gamma> \<turnstile> {s} Call g {t. xf t = f' s}"
380  and      mod: "modifies_spec g"
381  and       xf: "\<And>f s. xf (globals_update f s) = xf s"
382  shows "ccorres r xf (ko_at' ko thread) {s'. r (f ko) (f' s')} hs (threadGet f thread) (Call g)"
383  apply (rule ccorres_Call_call_for_vcg)
384  apply (rule ccorres_guard_imp2)
385   apply (rule ccorres_add_return2)
386   apply (rule ccorres_pre_threadGet)
387   apply (rule_tac P = "\<lambda>s. ko_at' ko thread s \<and> x = f ko" in ccorres_from_vcg [where P' = "{s'. r (f ko) (f' s')}"])
388   apply (rule allI)
389    apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. t\<lparr> globals := globals s \<rparr>"])
390      apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec])
391      defer
392      apply vcg
393     prefer 2
394     apply (rule mod)
395    apply (clarsimp simp: mex_def meq_def)
396    apply (frule obj_at'_weakenE [OF _ TrueI])
397   apply clarsimp
398   apply (drule (1) ko_at_obj_congD')
399   apply simp
400  apply (clarsimp simp: return_def)
401  apply (rule conjI)
402   apply (erule iffD1 [OF rf_sr_upd, rotated -1], simp_all)[1]
403  apply (simp add: xf)
404  done
405
406lemma ccorres_exI1:
407  assumes rl: "\<And>x. ccorres r xf (Q x) (P' x) hs a c"
408  shows   "ccorres r xf (\<lambda>s. (\<exists>x. P x s) \<and> (\<forall>x. P x s \<longrightarrow> Q x s))
409                        {s'. \<forall>x s. (s, s') \<in> rf_sr \<and> P x s \<longrightarrow> s' \<in> P' x} hs a c"
410  apply (rule ccorresI')
411  apply clarsimp
412  apply (drule spec, drule (1) mp)
413  apply (rule ccorresE [OF rl], assumption+)
414    apply fastforce
415   apply assumption
416   apply assumption
417  apply fastforce
418  done
419
420lemma isBlocked_ccorres [corres]:
421  "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
422  (tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread})  []
423  (isBlocked thread) (Call isBlocked_'proc)"
424  apply (cinit lift: thread_' simp: getThreadState_def)
425  apply (rule ccorres_pre_threadGet)
426   apply (rule ccorres_move_c_guard_tcb)
427   apply (rule ccorres_symb_exec_r)
428     apply (rule ccorres_cond_weak)
429      apply (rule ccorres_return_C)
430        apply simp
431       apply simp
432      apply simp
433     apply (simp add: ccorres_cond_iffs)
434     apply (rule ccorres_return_C)
435       apply simp
436      apply simp
437     apply simp
438    apply vcg
439   apply (rule conseqPre)
440   apply vcg
441   apply clarsimp
442  apply clarsimp
443  apply (clarsimp simp: to_bool_def true_def false_def typ_heap_simps
444    ctcb_relation_thread_state_to_tsType split: thread_state.splits)
445  apply (simp add: "StrictC'_thread_state_defs")+
446  done
447
448lemma isRunnable_ccorres [corres]:
449  "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
450  (tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread})  []
451  (isRunnable thread) (Call isRunnable_'proc)"
452  apply (cinit lift: thread_' simp: getThreadState_def)
453   apply (rule ccorres_move_c_guard_tcb)
454   apply (rule ccorres_pre_threadGet)
455   apply (rule ccorres_symb_exec_r)
456     apply (rule ccorres_cond_weak)
457     apply (rule ccorres_return_C)
458        apply (simp)
459       apply (simp)
460      apply (simp)
461     apply (simp add: ccorres_cond_iffs)
462     apply (rule ccorres_return_C)
463       apply (simp)
464      apply (simp)
465     apply (simp)
466    apply (vcg)
467   apply (rule conseqPre)
468    apply (vcg)
469   apply (clarsimp)
470  apply (clarsimp)
471  apply (clarsimp simp: to_bool_def true_def false_def typ_heap_simps
472    ctcb_relation_thread_state_to_tsType split: thread_state.splits)
473  apply (simp add: "StrictC'_thread_state_defs")+
474done
475
476
477
478lemma tcb_queue_relation_update_head:
479  fixes getNext_update :: "(tcb_C ptr \<Rightarrow> tcb_C ptr) \<Rightarrow> tcb_C \<Rightarrow> tcb_C" and
480  getPrev_update :: "(tcb_C ptr \<Rightarrow> tcb_C ptr) \<Rightarrow> tcb_C \<Rightarrow> tcb_C"
481  assumes qr: "tcb_queue_relation getNext getPrev mp queue NULL qhead"
482  and     qh': "qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue"
483  and  cs_tcb: "mp qhead' = Some tcb"
484  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
485  and     qhN: "qhead' \<noteq> NULL"
486  and     fgN: "fg_cons getNext (getNext_update \<circ> (\<lambda>x _. x))"
487  and     fgP: "fg_cons getPrev (getPrev_update \<circ> (\<lambda>x _. x))"
488  and     npu: "\<And>f t. getNext (getPrev_update f t) = getNext t"
489  and     pnu: "\<And>f t. getPrev (getNext_update f t) = getPrev t"
490  shows   "tcb_queue_relation getNext getPrev
491                 (upd_unless_null qhead (getPrev_update (\<lambda>_. qhead') (the (mp qhead)))
492                       (mp(qhead' := Some (getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead)  tcb)))))
493                 (ctcb_ptr_to_tcb_ptr qhead' # queue) NULL qhead'"
494  using qr qh' cs_tcb valid_ep qhN
495  apply (subgoal_tac "qhead \<noteq> qhead'")
496  apply (clarsimp simp: pnu upd_unless_null_def fg_consD1 [OF fgN] fg_consD1 [OF fgP] npu)
497  apply (cases queue)
498    apply simp
499   apply (frule (2) tcb_queue_relation_next_not_NULL)
500    apply simp
501   apply (clarsimp simp: fg_consD1 [OF fgN] fg_consD1 [OF fgP] pnu npu)
502   apply (subst tcb_queue_relation_cong [OF refl refl refl, where mp' = mp])
503    apply (clarsimp simp: inj_eq)
504    apply (intro impI conjI)
505     apply (frule_tac x = x in imageI [where f = tcb_ptr_to_ctcb_ptr])
506     apply simp
507    apply simp
508   apply simp
509  apply clarsimp
510  apply (cases queue)
511   apply simp
512  apply simp
513  done
514
515lemma tcbSchedEnqueue_update:
516  assumes sr: "sched_queue_relation' mp queue qhead qend"
517  and     qh': "qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue"
518  and  cs_tcb: "mp qhead' = Some tcb"
519  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
520  and     qhN: "qhead' \<noteq> NULL"
521  shows
522  "sched_queue_relation'
523                   (upd_unless_null qhead (tcbSchedPrev_C_update (\<lambda>_. qhead') (the (mp qhead)))
524                (mp(qhead' \<mapsto> tcb\<lparr>tcbSchedNext_C := qhead, tcbSchedPrev_C := NULL\<rparr>)))
525            (ctcb_ptr_to_tcb_ptr qhead' # queue) qhead' (if qend = NULL then qhead' else qend)"
526  using sr qh' cs_tcb valid_ep qhN
527  apply -
528  apply (erule tcb_queue_relationE')
529  apply (rule tcb_queue_relationI')
530   apply (erule (5) tcb_queue_relation_update_head
531        [where getNext_update = tcbSchedNext_C_update and getPrev_update = tcbSchedPrev_C_update], simp_all)[1]
532  apply simp
533  apply (intro impI)
534  apply (erule (1) tcb_queue_relation_not_NULL')
535  apply simp
536  done
537
538lemma tcb_ptr_to_ctcb_ptr_imageD:
539  "x \<in> tcb_ptr_to_ctcb_ptr ` S \<Longrightarrow> ctcb_ptr_to_tcb_ptr x \<in> S"
540  apply (erule imageE)
541  apply simp
542  done
543
544lemma ctcb_ptr_to_tcb_ptr_imageI:
545  "ctcb_ptr_to_tcb_ptr x \<in> S \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` S"
546  apply (drule imageI [where f = tcb_ptr_to_ctcb_ptr])
547  apply simp
548  done
549
550lemma tcb_queue'_head_end_NULL:
551  assumes qr: "tcb_queue_relation' getNext getPrev mp queue qhead qend"
552  and   tat: "\<forall>t\<in>set queue. tcb_at' t s"
553  shows "(qend = NULL) = (qhead = NULL)"
554  using qr tat
555  apply -
556  apply (erule tcb_queue_relationE')
557  apply (simp add: tcb_queue_head_empty_iff)
558  apply (rule impI)
559  apply (rule tcb_at_not_NULL)
560  apply (erule bspec)
561  apply simp
562  done
563
564lemma tcb_queue_relation_qhead_mem:
565  "\<lbrakk> tcb_queue_relation getNext getPrev mp queue NULL qhead;
566  (\<forall>tcb\<in>set queue. tcb_at' tcb t) \<rbrakk>
567  \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qhead \<in> set queue"
568  by (clarsimp simp: tcb_queue_head_empty_iff tcb_queue_relation_head_hd)
569
570lemma tcb_queue_relation_qhead_valid:
571  "\<lbrakk> tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead;
572  (s, s') \<in> rf_sr; (\<forall>tcb\<in>set queue. tcb_at' tcb s) \<rbrakk>
573  \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qhead"
574  apply (frule (1) tcb_queue_relation_qhead_mem)
575  apply clarsimp
576  apply(drule (3) tcb_queue_memberD)
577  apply (simp add: h_t_valid_clift_Some_iff)
578  done
579
580lemmas tcb_queue_relation_qhead_mem' = tcb_queue_relation_qhead_mem [OF tcb_queue_relation'_queue_rel]
581lemmas tcb_queue_relation_qhead_valid' = tcb_queue_relation_qhead_valid [OF tcb_queue_relation'_queue_rel]
582
583
584lemma valid_queues_valid_q:
585  "valid_queues s \<Longrightarrow> (\<forall>tcb\<in>set (ksReadyQueues s (qdom, prio)). tcb_at' tcb s) \<and> distinct (ksReadyQueues s (qdom, prio))"
586  apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def)
587  apply (drule spec [where x = qdom])
588  apply (drule spec [where x = prio])
589  apply clarsimp
590  apply (drule (1) bspec, erule obj_at'_weakenE)
591  apply simp
592  done
593
594lemma invs_valid_q:
595  "invs' s \<Longrightarrow> (\<forall>tcb\<in>set (ksReadyQueues s (qdom, prio)). tcb_at' tcb s) \<and> distinct (ksReadyQueues s (qdom, prio))"
596  apply (rule valid_queues_valid_q)
597  apply (clarsimp simp: invs'_def valid_state'_def)
598  done
599
600lemma tcbQueued_not_in_queues:
601  assumes vq: "valid_queues s"
602  and    objat: "obj_at' (Not \<circ> tcbQueued) thread s"
603  shows   "thread \<notin> set (ksReadyQueues s (d, p))"
604  using vq objat
605  apply -
606  apply clarsimp
607  apply (drule (1) valid_queues_obj_at'D)
608  apply (erule obj_atE')+
609  apply (clarsimp simp: inQ_def)
610  done
611
612declare unat_ucast_8_64[simp]
613
614lemma rf_sr_sched_queue_relation:
615  "\<lbrakk> (s, s') \<in> rf_sr; d \<le> ucast maxDom; p \<le> ucast maxPrio \<rbrakk>
616  \<Longrightarrow> sched_queue_relation' (cslift s') (ksReadyQueues s (d, p))
617                                        (head_C (index (ksReadyQueues_' (globals s'))
618                                                       (cready_queues_index_to_C d p)))
619                                        (end_C (index (ksReadyQueues_' (globals s'))
620                                                      (cready_queues_index_to_C d p)))"
621  unfolding rf_sr_def cstate_relation_def cready_queues_relation_def
622  apply (clarsimp simp: Let_def seL4_MinPrio_def minDom_def)
623  done
624
625lemma ready_queue_not_in:
626  assumes  vq: "valid_queues s"
627  and     inq: "t \<in> set (ksReadyQueues s (d, p))"
628  and     neq: "d \<noteq> d' \<or> p \<noteq> p'"
629  shows   "t \<notin> set (ksReadyQueues s (d', p'))"
630proof
631  assume "t \<in> set (ksReadyQueues s (d', p'))"
632  hence "obj_at' (inQ d' p') t s" using vq by (rule valid_queues_obj_at'D)
633  moreover have "obj_at' (inQ d p) t s" using inq vq by (rule valid_queues_obj_at'D)
634  ultimately show False using neq
635    by (clarsimp elim!: obj_atE' simp: inQ_def)
636qed
637
638lemma ctcb_relation_unat_prio_eq:
639  "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority tcb) = unat (tcbPriority_C tcb')"
640  apply (clarsimp simp: ctcb_relation_def)
641  apply (erule_tac t = "tcbPriority_C tcb'" in subst)
642  apply simp
643  done
644
645lemma ctcb_relation_unat_dom_eq:
646  "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain tcb) = unat (tcbDomain_C tcb')"
647  apply (clarsimp simp: ctcb_relation_def)
648  apply (erule_tac t = "tcbDomain_C tcb'" in subst)
649  apply simp
650  done
651
652lemma threadSet_queued_ccorres [corres]:
653  shows "ccorres dc xfdc (tcb_at' thread)
654        {s. v64_' s = from_bool v \<and> thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} []
655        (threadSet (tcbQueued_update (\<lambda>_. v)) thread)
656        (Call thread_state_ptr_set_tcbQueued_'proc)"
657  apply (rule threadSet_corres_lemma)
658     apply (rule thread_state_ptr_set_tcbQueued_spec)
659    apply (rule thread_state_ptr_set_tcbQueued_modifies)
660   apply clarsimp
661   apply (frule (1) obj_at_cslift_tcb)
662   apply clarsimp
663   apply (rule rf_sr_tcb_update_no_queue_gen, assumption+, simp, simp_all)
664   apply (rule ball_tcb_cte_casesI, simp_all)
665   apply (simp add: ctcb_relation_def cthread_state_relation_def)
666   apply (case_tac "tcbState ko", simp_all add: Word_Lemmas.from_bool_mask_simp)[1]
667  apply (frule (1) obj_at_cslift_tcb)
668  apply (clarsimp simp: typ_heap_simps)
669  done
670
671lemma ccorres_pre_getQueue:
672  assumes cc: "\<And>queue. ccorres r xf (P queue) (P' queue) hs (f queue) c"
673  shows   "ccorres r xf (\<lambda>s. P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority)
674                        {s'. \<forall>queue. (let cqueue = index (ksReadyQueues_' (globals s'))
675                                                         (cready_queues_index_to_C d p) in
676                                      sched_queue_relation' (cslift s') queue (head_C cqueue) (end_C cqueue)) \<longrightarrow> s' \<in> P' queue}
677           hs (getQueue d p >>= (\<lambda>queue. f queue)) c"
678  apply (rule ccorres_guard_imp2)
679  apply (rule ccorres_symb_exec_l2)
680     defer
681     defer
682     apply (rule gq_sp)
683    defer
684    apply (rule ccorres_guard_imp)
685    apply (rule cc)
686     apply clarsimp
687     apply assumption
688    apply assumption
689   apply (clarsimp simp: getQueue_def gets_exs_valid)
690  apply clarsimp
691  apply (drule spec, erule mp)
692  apply (simp add: Let_def)
693  apply (erule rf_sr_sched_queue_relation)
694   apply (simp add: maxDom_to_H maxPrio_to_H)+
695  done
696
697(* FIXME: move *)
698lemma threadGet_wp:
699  "\<lbrace>\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>"
700  apply (rule hoare_post_imp [OF _ tg_sp'])
701  apply clarsimp
702  apply (frule obj_at_ko_at')
703  apply (clarsimp elim: obj_atE')
704  done
705
706lemma state_relation_queue_update_helper':
707  "\<lbrakk> (s, s') \<in> rf_sr;
708     (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s)
709                                       \<and> distinct (ksReadyQueues s (d, p)));
710          globals t = ksReadyQueues_'_update
711             (\<lambda>_. Arrays.update (ksReadyQueues_' (globals s')) prio' q')
712             (t_hrs_'_update f (globals s'));
713          sched_queue_relation' (cslift t) q (head_C q') (end_C q');
714          cslift t |` ( - tcb_ptr_to_ctcb_ptr ` S )
715             = cslift s' |` ( - tcb_ptr_to_ctcb_ptr ` S );
716          option_map tcb_null_sched_ptrs \<circ> cslift t
717            = option_map tcb_null_sched_ptrs \<circ> cslift s';
718          cslift_all_but_tcb_C t s';
719          zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s')))
720              = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s'));
721          hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s'));
722          prio' = cready_queues_index_to_C qdom prio;
723          \<forall>x \<in> S. obj_at' (inQ qdom prio) x s
724                   \<or> (obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s
725                       \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s)
726                   \<or> (tcb_at' x s \<and> (\<forall>d' p'. (d' \<noteq> qdom \<or> p' \<noteq> prio)
727                                         \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))));
728          S \<noteq> {}; qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk>
729      \<Longrightarrow> (s \<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr"
730  apply (subst(asm) disj_imp_rhs)
731   apply (subst obj_at'_and[symmetric])
732   apply (rule disjI1, erule obj_at'_weakenE, simp add: inQ_def)
733  apply (subst(asm) disj_imp_rhs)
734   apply (subst(asm) obj_at'_and[symmetric])
735   apply (rule conjI, erule obj_at'_weakenE, simp)
736   apply (rule allI, rule allI)
737   apply (drule_tac x=d' in spec)
738   apply (drule_tac x=p' in spec)
739   apply clarsimp
740   apply (drule(1) bspec)
741   apply (clarsimp simp: inQ_def obj_at'_def)
742  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
743  apply (intro conjI)
744      \<comment> \<open>cpspace_relation\<close>
745     apply (erule nonemptyE, drule(1) bspec)
746     apply (clarsimp simp: cpspace_relation_def)
747     apply (drule obj_at_ko_at', clarsimp)
748     apply (rule cmap_relationE1, assumption,
749            erule ko_at_projectKO_opt)
750     apply (frule null_sched_queue)
751     apply (frule null_sched_epD)
752     apply (intro conjI)
753       \<comment> \<open>tcb relation\<close>
754       apply (drule ctcb_relation_null_queue_ptrs,
755              simp_all)[1]
756      \<comment> \<open>endpoint relation\<close>
757      apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
758      apply simp
759      apply (erule cendpoint_relation_upd_tcb_no_queues, simp+)
760     \<comment> \<open>ntfn relation\<close>
761     apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
762     apply simp
763     apply (erule cnotification_relation_upd_tcb_no_queues, simp+)
764    \<comment> \<open>ready queues\<close>
765    apply (simp add: cready_queues_relation_def Let_def
766                     cready_queues_index_to_C_in_range
767                     seL4_MinPrio_def minDom_def)
768    apply clarsimp
769    apply (frule cready_queues_index_to_C_distinct, assumption+)
770    apply (clarsimp simp: cready_queues_index_to_C_in_range all_conj_distrib)
771    apply (rule iffD1 [OF tcb_queue_relation'_cong[OF refl], rotated -1],
772           drule spec, drule spec, erule mp, simp+)
773    apply clarsimp
774    apply (drule_tac x="tcb_ptr_to_ctcb_ptr x" in fun_cong)+
775    apply (clarsimp simp: restrict_map_def
776                   split: if_split_asm)
777   by (auto simp: carch_state_relation_def cmachine_state_relation_def
778           elim!: fpu_null_state_typ_heap_preservation)
779
780lemma state_relation_queue_update_helper:
781  "\<lbrakk> (s, s') \<in> rf_sr; valid_queues s;
782          globals t = ksReadyQueues_'_update
783             (\<lambda>_. Arrays.update (ksReadyQueues_' (globals s')) prio' q')
784             (t_hrs_'_update f (globals s'));
785          sched_queue_relation' (cslift t) q (head_C q') (end_C q');
786          cslift t |` ( - tcb_ptr_to_ctcb_ptr ` S )
787             = cslift s' |` ( - tcb_ptr_to_ctcb_ptr ` S );
788          option_map tcb_null_sched_ptrs \<circ> cslift t
789            = option_map tcb_null_sched_ptrs \<circ> cslift s';
790          cslift_all_but_tcb_C t s';
791          zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s')))
792              = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s'));
793          hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s'));
794          prio' = cready_queues_index_to_C qdom prio;
795          \<forall>x \<in> S. obj_at' (inQ qdom prio) x s
796                   \<or> (obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s
797                       \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s)
798                   \<or> (tcb_at' x s \<and> (\<forall>d' p'. (d' \<noteq> qdom \<or> p' \<noteq> prio)
799                                         \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))));
800          S \<noteq> {}; qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk>
801      \<Longrightarrow> (s \<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr"
802  apply (subgoal_tac "\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s)
803                           \<and> distinct(ksReadyQueues s (d, p))")
804   apply (erule(5) state_relation_queue_update_helper', simp_all)
805  apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def)
806  apply (drule_tac x=d in spec)
807  apply (drule_tac x=p in spec)
808  apply (clarsimp)
809  apply (drule(1) bspec)
810  apply (erule obj_at'_weakenE, clarsimp)
811  done
812
813(* FIXME: move *)
814lemma from_bool_vals [simp]:
815  "from_bool True = scast true"
816  "from_bool False = scast false"
817  "scast true \<noteq> scast false"
818  by (auto simp add: from_bool_def true_def false_def)
819
820(* FIXME: move *)
821lemma cmap_relation_no_upd:
822  "\<lbrakk> cmap_relation a c f rel; a p = Some ko; rel ko v; inj f \<rbrakk> \<Longrightarrow> cmap_relation a (c(f p \<mapsto> v)) f rel"
823  apply (clarsimp simp: cmap_relation_def)
824  apply (subgoal_tac "f p \<in> dom c")
825   prefer 2
826   apply (drule_tac t="dom c" in sym)
827   apply fastforce
828  apply clarsimp
829  apply (drule (1) injD)
830  apply simp
831  done
832
833(* FIXME: move *)
834lemma cmap_relation_rel_upd:
835  "\<lbrakk> cmap_relation a c f rel; \<And>v v'. rel v v' \<Longrightarrow> rel' v v' \<rbrakk> \<Longrightarrow> cmap_relation a c f rel'"
836  by (simp add: cmap_relation_def)
837
838declare fun_upd_restrict_conv[simp del]
839
840lemmas queue_in_range = of_nat_mono_maybe[OF _ cready_queues_index_to_C_in_range,
841        where 'a=32, unfolded cready_queues_index_to_C_def numPriorities_def,
842        simplified, unfolded ucast_nat_def]
843    of_nat_mono_maybe[OF _ cready_queues_index_to_C_in_range,
844        where 'a="32 signed", unfolded cready_queues_index_to_C_def numPriorities_def,
845        simplified, unfolded ucast_nat_def]
846    of_nat_mono_maybe[OF _ cready_queues_index_to_C_in_range,
847        where 'a=64, unfolded cready_queues_index_to_C_def numPriorities_def,
848        simplified, unfolded ucast_nat_def]
849
850lemma cready_queues_index_to_C_def2':
851  "\<lbrakk> qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk>
852   \<Longrightarrow> cready_queues_index_to_C qdom prio
853             = unat (ucast qdom * of_nat numPriorities + ucast prio :: machine_word)"
854  apply (simp add: cready_queues_index_to_C_def numPriorities_def)
855  apply (subst unat_add_lem[THEN iffD1])
856   apply (frule cready_queues_index_to_C_in_range, simp)
857   apply (simp add: cready_queues_index_to_C_def numPriorities_def)
858   apply (subst unat_mult_simple)
859    apply (simp add: word_bits_def maxDom_def)
860   apply simp
861  apply (subst unat_mult_simple)
862   apply (simp add: word_bits_def maxDom_def)
863   apply (subst (asm) word_le_nat_alt)
864   apply simp
865  apply simp
866  done
867
868lemmas cready_queues_index_to_C_def2
869           = cready_queues_index_to_C_def2'[simplified maxDom_to_H maxPrio_to_H]
870
871lemma ready_queues_index_spec:
872  "\<forall>s. \<Gamma> \<turnstile> {s} Call ready_queues_index_'proc
873       \<lbrace>\<acute>ret__unsigned_long = (dom_' s) * 0x100 + (prio_' s)\<rbrace>"
874  by vcg (simp add: word_sless_alt)
875
876lemma prio_to_l1index_spec:
877  "\<forall>s. \<Gamma> \<turnstile> {s} Call prio_to_l1index_'proc
878       \<lbrace>\<acute>ret__unsigned_long = prio_' s >> wordRadix \<rbrace>"
879  by vcg (simp add: word_sle_def wordRadix_def')
880
881lemma invert_l1index_spec:
882  "\<forall>s. \<Gamma> \<turnstile> {s} Call invert_l1index_'proc
883       \<lbrace>\<acute>ret__unsigned_long = of_nat l2BitmapSize - 1 - l1index_' s \<rbrace>"
884  unfolding l2BitmapSize_def'
885  by vcg
886     (simp add: word_sle_def sdiv_int_def sdiv_word_def smod_word_def smod_int_def)
887
888lemma cbitmap_L1_relation_update:
889  "\<lbrakk> (\<sigma>, s) \<in> rf_sr ; cbitmap_L1_relation cupd aupd \<rbrakk>
890   \<Longrightarrow> (\<sigma>\<lparr>ksReadyQueuesL1Bitmap := aupd \<rparr>,
891       globals_update (ksReadyQueuesL1Bitmap_'_update (\<lambda>_. cupd)) s)
892      \<in> rf_sr"
893  by (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
894                cmachine_state_relation_def)
895
896lemma cbitmap_L2_relation_update:
897  "\<lbrakk> (\<sigma>, s) \<in> rf_sr ; cbitmap_L2_relation cupd aupd \<rbrakk>
898   \<Longrightarrow> (\<sigma>\<lparr>ksReadyQueuesL2Bitmap := aupd \<rparr>,
899       globals_update (ksReadyQueuesL2Bitmap_'_update (\<lambda>_. cupd)) s)
900      \<in> rf_sr"
901  by (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
902                cmachine_state_relation_def)
903
904lemma unat_ucast_prio_shiftr_simp[simp]:
905  "unat (ucast (p::priority) >> n :: machine_word) = unat (p >> n)"
906  by (simp add: shiftr_div_2n')+
907
908lemma unat_ucast_prio_mask_simp[simp]:
909  "unat (ucast (p::priority) && mask m :: machine_word) = unat (p && mask m)"
910  by (metis ucast_and_mask unat_ucast_8_64)
911
912lemma unat_ucast_prio_L1_cmask_simp:
913  "unat (ucast (p::priority) && 0x3F :: machine_word) = unat (p && 0x3F)"
914  using unat_ucast_prio_mask_simp[where m=6]
915  by (simp add: mask_def)
916
917lemma machine_word_and_3F_less_40:
918  "(w :: machine_word) && 0x3F < 0x40"
919  by (rule word_and_less', simp)
920
921lemma prio_ucast_shiftr_wordRadix_helper: (* FIXME generalise *)
922  "(ucast (p::priority) >> wordRadix :: machine_word) < 4"
923  unfolding maxPriority_def numPriorities_def wordRadix_def
924  using unat_lt2p[where x=p]
925  apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt)
926  apply arith
927  done
928
929lemma prio_ucast_shiftr_wordRadix_helper': (* FIXME generalise *)
930  "(ucast (p::priority) >> wordRadix :: machine_word) \<le> 3"
931  unfolding maxPriority_def numPriorities_def wordRadix_def
932  using unat_lt2p[where x=p]
933  apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt)
934  apply arith
935  done
936
937lemma prio_unat_shiftr_wordRadix_helper': (* FIXME generalise *)
938  "unat ((p::priority) >> wordRadix) \<le> 3"
939  unfolding maxPriority_def numPriorities_def wordRadix_def
940  using unat_lt2p[where x=p]
941  apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt)
942  apply arith
943  done
944
945lemma prio_ucast_shiftr_wordRadix_helper2: (* FIXME possibly unused *)
946  "(ucast (p::priority) >> wordRadix :: machine_word) < 0x20"
947  by (rule order_less_trans[OF prio_ucast_shiftr_wordRadix_helper]; simp)
948
949lemma prio_ucast_shiftr_wordRadix_helper3:
950  "(ucast (p::priority) >> wordRadix :: machine_word) < 0x40"
951  by (rule order_less_trans[OF prio_ucast_shiftr_wordRadix_helper]; simp)
952
953lemma dom_less_0x10_helper:
954  "d \<le> maxDomain \<Longrightarrow> (ucast d :: machine_word) < 0x10"
955  unfolding maxDomain_def numDomains_def
956  by (clarsimp simp add: word_less_nat_alt unat_ucast_upcast is_up word_le_nat_alt)
957
958lemma cready_queues_index_to_C_ucast_helper:
959  fixes p :: priority
960  fixes d :: domain
961  shows "unat (ucast d * 0x100 + ucast p :: machine_word) = unat d * 256 + unat p"
962  unfolding tcb_queue_relation'_def maxPriority_def maxDomain_def numDomains_def numPriorities_def
963  using unat_lt2p[where x=p] unat_lt2p[where x=d]
964  by (clarsimp simp: cready_queues_index_to_C_def word_le_nat_alt unat_word_ariths)
965
966lemmas prio_and_dom_limit_helpers =
967  prio_ucast_shiftr_wordRadix_helper
968  prio_ucast_shiftr_wordRadix_helper'
969  prio_ucast_shiftr_wordRadix_helper2
970  prio_ucast_shiftr_wordRadix_helper3
971  prio_unat_shiftr_wordRadix_helper'
972  dom_less_0x10_helper
973  cready_queues_index_to_C_ucast_helper
974  unat_ucast_prio_L1_cmask_simp
975  machine_word_and_3F_less_40
976
977(* FIXME MOVE *)
978lemma rf_sr_cbitmap_L1_relation[intro]:
979  "(\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>)"
980  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
981
982(* FIXME MOVE *)
983lemma rf_sr_cbitmap_L2_relation[intro]:
984  "(\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>)"
985  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
986
987lemma cbitmap_L1_relation_bit_set:
988  fixes p :: priority
989  shows
990  "\<lbrakk> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) ;
991     d \<le> maxDomain \<rbrakk> \<Longrightarrow>
992   cbitmap_L1_relation
993           (Arrays.update (ksReadyQueuesL1Bitmap_' (globals x)) (unat d)
994             (ksReadyQueuesL1Bitmap_' (globals x).[unat d] || 2 ^ unat (p >> wordRadix)))
995           ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d || 2 ^ prioToL1Index p))"
996  apply (unfold cbitmap_L1_relation_def)
997  apply (clarsimp simp: prioToL1Index_def wordRadix_def' maxDomain_def numDomains_def word_le_nat_alt)
998  done
999
1000lemma cbitmap_L2_relation_bit_set:
1001  fixes p :: priority
1002  fixes d :: domain
1003  shows "\<lbrakk> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>) ;
1004           d \<le> maxDomain ; b = b' \<rbrakk>
1005         \<Longrightarrow>
1006         cbitmap_L2_relation
1007          (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d)
1008            (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d])
1009              (invertL1Index (prioToL1Index p))
1010              (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] ||
1011               2 ^ unat (p && b))))
1012          ((ksReadyQueuesL2Bitmap \<sigma>)
1013           ((d, invertL1Index (prioToL1Index p)) :=
1014              ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) ||
1015               2 ^ unat (p && b')))"
1016  unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def'
1017  apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def
1018                        invertL1Index_def l2BitmapSize_def'
1019                        maxDomain_def numDomains_def word_le_nat_alt)
1020  apply (case_tac "da = d" ; clarsimp)
1021  done
1022
1023lemma carch_state_relation_enqueue_simp:
1024  "carch_state_relation (ksArchState \<sigma>)
1025    (t_hrs_'_update f
1026      (globals \<sigma>' \<lparr>ksReadyQueuesL1Bitmap_' := l1upd, ksReadyQueuesL2Bitmap_' := l2upd \<rparr>)
1027      \<lparr>ksReadyQueues_' := rqupd \<rparr>) =
1028   carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update f (globals \<sigma>'))"
1029  unfolding carch_state_relation_def
1030  by clarsimp
1031
1032(* FIXME move to lib/Eisbach_Methods *)
1033(* FIXME consider printing error on solve goal apply *)
1034context
1035begin
1036
1037private definition "bool_protect (b::bool) \<equiv> b"
1038
1039lemma bool_protectD:
1040  "bool_protect P \<Longrightarrow> P"
1041  unfolding bool_protect_def by simp
1042
1043lemma bool_protectI:
1044  "P \<Longrightarrow> bool_protect P"
1045  unfolding bool_protect_def by simp
1046
1047(*
1048  When you want to apply a rule/tactic to transform a potentially complex goal into another
1049  one manually, but want to indicate that any fresh emerging goals are solved by a more
1050  brutal method.
1051  E.g. apply (solves_emerging \<open>frule x=... in my_rule\<close>\<open>fastforce simp: ... intro!: ... \<close>  *)
1052method solves_emerging methods m1 m2 = (rule bool_protectD, (m1 ; (rule bool_protectI | (m2; fail))))
1053
1054end
1055
1056lemma t_hrs_ksReadyQueues_upd_absorb:
1057  "t_hrs_'_update f (g s) \<lparr>ksReadyQueues_' := rqupd \<rparr> =
1058   t_hrs_'_update f (g s \<lparr>ksReadyQueues_' := rqupd\<rparr>)"
1059  by simp
1060
1061lemma rf_sr_drop_bitmaps_enqueue_helper:
1062  "\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ;
1063     cbitmap_L1_relation ksqL1upd' ksqL1upd ; cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk>
1064   \<Longrightarrow>
1065   ((\<sigma>\<lparr>ksReadyQueues := ksqupd, ksReadyQueuesL1Bitmap := ksqL1upd, ksReadyQueuesL2Bitmap := ksqL2upd\<rparr>,
1066     \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd',
1067        globals := t_hrs_'_update f
1068          (globals \<sigma>'
1069             \<lparr>ksReadyQueuesL1Bitmap_' := ksqL1upd',
1070              ksReadyQueuesL2Bitmap_' := ksqL2upd',
1071              ksReadyQueues_' := ksqupd'\<rparr>)\<rparr>) \<in> rf_sr) =
1072   ((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>,
1073     \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd',
1074        globals := t_hrs_'_update f
1075          (globals \<sigma>' \<lparr>ksReadyQueues_' := ksqupd'\<rparr>)\<rparr>) \<in> rf_sr)"
1076  unfolding rf_sr_def cstate_relation_def Let_def
1077             carch_state_relation_def cmachine_state_relation_def
1078  by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation)
1079
1080lemma cmachine_state_relation_enqueue_simp:
1081  "cmachine_state_relation (ksMachineState \<sigma>)
1082    (t_hrs_'_update f
1083      (globals \<sigma>' \<lparr>ksReadyQueuesL1Bitmap_' := l1upd, ksReadyQueuesL2Bitmap_' := l2upd \<rparr>)
1084      \<lparr>ksReadyQueues_' := rqupd \<rparr>) =
1085   cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update f (globals \<sigma>'))"
1086  unfolding cmachine_state_relation_def
1087  by clarsimp
1088
1089lemma tcb_queue_relation'_empty_ksReadyQueues:
1090  "\<lbrakk> sched_queue_relation' (cslift x) (q s) NULL NULL ; \<forall>t\<in> set (q s). tcb_at' t s  \<rbrakk> \<Longrightarrow> q s = []"
1091  apply (clarsimp simp add: tcb_queue_relation'_def)
1092  apply (subst (asm) eq_commute)
1093  apply (cases "q s" rule: rev_cases, simp)
1094  apply (clarsimp simp: tcb_at_not_NULL)
1095  done
1096
1097lemma invert_prioToL1Index_c_simp:
1098  "p \<le> maxPriority
1099   \<Longrightarrow>
1100   unat ((of_nat l2BitmapSize :: machine_word) - 1 - (ucast p >> wordRadix))
1101   = invertL1Index (prioToL1Index p)"
1102   unfolding maxPriority_def l2BitmapSize_def' invertL1Index_def prioToL1Index_def
1103     numPriorities_def
1104   by (simp add: unat_sub prio_and_dom_limit_helpers)
1105
1106lemma c_invert_assist: "3 - (ucast (p :: priority) >> 6 :: machine_word) < 4"
1107  using prio_ucast_shiftr_wordRadix_helper'[simplified wordRadix_def]
1108  by - (rule word_less_imp_diff_less, simp_all)
1109
1110lemma tcbSchedEnqueue_ccorres:
1111  "ccorres dc xfdc
1112           (valid_queues and tcb_at' t and valid_objs')
1113           (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>)
1114           hs
1115           (tcbSchedEnqueue t)
1116           (Call tcbSchedEnqueue_'proc)"
1117proof -
1118  note prio_and_dom_limit_helpers[simp] word_sle_def[simp] maxDom_to_H[simp] maxPrio_to_H[simp]
1119  note invert_prioToL1Index_c_simp[simp]
1120
1121  show ?thesis
1122    apply (cinit lift: tcb_')
1123     apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'"
1124              in ccorres_split_nothrow)
1125         apply (rule threadGet_vcg_corres)
1126         apply (rule allI, rule conseqPre, vcg)
1127         apply clarsimp
1128         apply (drule obj_at_ko_at', clarsimp)
1129         apply (drule spec, drule(1) mp, clarsimp)
1130         apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1131        apply ceqv
1132       apply (simp add: when_def unless_def del: Collect_const split del: if_split)
1133       apply (rule ccorres_cond[where R=\<top>])
1134         apply (simp add: to_bool_def)
1135        apply (rule ccorres_rhs_assoc)+
1136        apply csymbr
1137        apply csymbr
1138        apply csymbr
1139        apply csymbr
1140        apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="dom_'" in ccorres_split_nothrow)
1141            apply (rule threadGet_vcg_corres)
1142            apply (rule allI, rule conseqPre, vcg)
1143            apply clarsimp
1144            apply (drule obj_at_ko_at', clarsimp)
1145            apply (drule spec, drule(1) mp, clarsimp)
1146            apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1147           apply ceqv
1148          apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="prio_'" in ccorres_split_nothrow)
1149              apply (rule threadGet_vcg_corres)
1150              apply (rule allI, rule conseqPre, vcg)
1151              apply clarsimp
1152              apply (drule obj_at_ko_at', clarsimp)
1153              apply (drule spec, drule(1) mp, clarsimp)
1154              apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1155             apply ceqv
1156            apply (rule ccorres_rhs_assoc2)+
1157            apply (simp only: bind_assoc[symmetric])
1158            apply (rule ccorres_split_nothrow_novcg_dc)
1159               prefer 2
1160               apply (rule ccorres_move_c_guard_tcb)
1161               apply (simp only: dc_def[symmetric])
1162               apply ctac
1163              prefer 2
1164              apply (wp, clarsimp, wp+)
1165             apply (rule_tac P="\<lambda>s. valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p))
1166                                  \<and> (\<exists>tcb. ko_at' tcb t s \<and> tcbDomain tcb =rva
1167                                  \<and> tcbPriority tcb = rvb \<and> valid_tcb' tcb s)"
1168                         and P'=UNIV in ccorres_from_vcg)
1169             apply (rule allI, rule conseqPre, vcg)
1170             apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def
1171                                   put_def bind_def return_def bitmap_fun_defs null_def)
1172             apply (clarsimp simp: queue_in_range valid_tcb'_def)
1173             apply (rule conjI; clarsimp simp: queue_in_range)
1174              (* queue is empty, set t to be new queue *)
1175              apply (drule (1) obj_at_cslift_tcb)
1176              apply clarsimp
1177              apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb"
1178                       in rf_sr_sched_queue_relation)
1179                apply clarsimp
1180               apply clarsimp
1181              apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL)
1182               apply (simp add: valid_queues_valid_q)
1183              apply (subgoal_tac
1184                      "head_C (ksReadyQueues_' (globals x)
1185                         .[cready_queues_index_to_C (tcbDomain tcb) (tcbPriority tcb)]) = NULL")
1186               prefer 2
1187               apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL; simp add: valid_queues_valid_q)
1188              apply (subgoal_tac
1189                       "end_C (ksReadyQueues_' (globals x)
1190                          .[cready_queues_index_to_C (tcbDomain tcb) (tcbPriority tcb)]) = NULL")
1191               prefer 2
1192               apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL[symmetric]; simp add: valid_queues_valid_q)
1193              apply (clarsimp simp: cready_queues_index_to_C_def numPriorities_def)
1194              apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1195              apply (simp add: t_hrs_ksReadyQueues_upd_absorb)
1196
1197              apply (rule conjI)
1198               apply (clarsimp simp: l2BitmapSize_def' wordRadix_def c_invert_assist)
1199              apply (subst rf_sr_drop_bitmaps_enqueue_helper, assumption)
1200                apply (fastforce intro: cbitmap_L1_relation_bit_set)
1201               apply (fastforce intro: cbitmap_L2_relation_bit_set simp: wordRadix_def mask_def)
1202
1203              apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" in rf_sr_sched_queue_relation)
1204                apply clarsimp
1205               apply clarsimp
1206              apply (drule_tac qhead'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedEnqueue_update,
1207                     simp_all add: valid_queues_valid_q)[1]
1208               apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
1209              apply (erule(1) state_relation_queue_update_helper[where S="{t}"],
1210                     (simp | rule globals.equality)+,
1211                     simp_all add: cready_queues_index_to_C_def2 numPriorities_def
1212                                   t_hrs_ksReadyQueues_upd_absorb upd_unless_null_def
1213                                   typ_heap_simps)[1]
1214               apply (fastforce simp: tcb_null_sched_ptrs_def typ_heap_simps c_guard_clift
1215                                elim: obj_at'_weaken)+
1216
1217             apply (rule conjI; clarsimp simp: queue_in_range)
1218              (* invalid, disagreement between C and Haskell on emptiness of queue *)
1219              apply (drule (1) obj_at_cslift_tcb)
1220              apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1221              apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" in rf_sr_sched_queue_relation)
1222                apply clarsimp
1223               apply clarsimp
1224              apply (clarsimp simp: cready_queues_index_to_C_def numPriorities_def)
1225              apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL)
1226               apply (simp add: valid_queues_valid_q)
1227              apply clarsimp
1228              apply (drule tcb_queue_relation'_empty_ksReadyQueues; simp add: valid_queues_valid_q)
1229             (* queue was not empty, add t to queue and leave bitmaps alone *)
1230             apply (drule (1) obj_at_cslift_tcb)
1231             apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1232             apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" in rf_sr_sched_queue_relation)
1233               apply clarsimp
1234              apply clarsimp
1235             apply (clarsimp simp: cready_queues_index_to_C_def numPriorities_def)
1236             apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL)
1237              apply (simp add: valid_queues_valid_q)
1238             apply clarsimp
1239             apply (frule_tac t=\<sigma> in tcb_queue_relation_qhead_mem')
1240              apply (simp add: valid_queues_valid_q)
1241             apply (frule(1) tcb_queue_relation_qhead_valid')
1242              apply (simp add: valid_queues_valid_q)
1243             apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff numPriorities_def
1244                                   cready_queues_index_to_C_def2)
1245             apply (drule_tac qhead'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedEnqueue_update,
1246                    simp_all add: valid_queues_valid_q)[1]
1247               apply clarsimp
1248
1249              apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
1250             apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D])
1251             apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1252             apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper,
1253                    (simp | rule globals.equality)+,
1254                    simp_all add: typ_heap_simps if_Some_helper numPriorities_def
1255                                  cready_queues_index_to_C_def2 upd_unless_null_def
1256                             del: fun_upd_restrict_conv
1257                             cong: if_cong
1258                             split del: if_split)[1]
1259                 apply simp
1260                 apply (rule conjI)
1261                  apply clarsimp
1262                  apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp)
1263                 apply (clarsimp simp add: fun_upd_twist)
1264                prefer 4
1265                apply (simp add: obj_at'_weakenE[OF _ TrueI])
1266                apply (rule disjI1, erule (1) valid_queues_obj_at'D)
1267               apply clarsimp
1268              apply (fastforce simp: tcb_null_sched_ptrs_def)
1269             apply (simp add: fpu_state_preservation[OF _ h_t_valid_clift] typ_heap_simps')
1270            apply (simp add: typ_heap_simps c_guard_clift)
1271            apply (simp add: guard_is_UNIV_def)
1272           apply simp
1273           apply (wp threadGet_wp)
1274          apply vcg
1275         apply simp
1276         apply (wp threadGet_wp)
1277        apply vcg
1278       apply (rule ccorres_return_Skip[unfolded dc_def])
1279      apply simp
1280      apply (wp threadGet_wp)
1281     apply vcg
1282    apply (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def
1283                           valid_obj'_def inQ_def
1284                    dest!: valid_queues_obj_at'D)
1285  done
1286qed
1287
1288lemmas tcbSchedDequeue_update
1289    = tcbDequeue_update[where tn=tcbSchedNext_C and tn_update=tcbSchedNext_C_update
1290                          and tp=tcbSchedPrev_C and tp_update=tcbSchedPrev_C_update,
1291                        simplified]
1292
1293lemma tcb_queue_relation_prev_next:
1294  "\<lbrakk> tcb_queue_relation tn tp mp queue qprev qhead;
1295     tcbp \<in> set queue; distinct (ctcb_ptr_to_tcb_ptr qprev # queue);
1296     \<forall>t \<in> set queue. tcb_at' t s; qprev \<noteq> tcb_Ptr 0 \<longrightarrow> mp qprev \<noteq> None;
1297     mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<rbrakk>
1298      \<Longrightarrow> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue
1299                       \<and> mp (tn tcb) \<noteq> None \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp)
1300        \<and> (tp tcb \<noteq> tcb_Ptr 0 \<longrightarrow> (tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue
1301                                         \<or> tp tcb = qprev)
1302                       \<and> mp (tp tcb) \<noteq> None \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp)
1303        \<and> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<noteq> tp tcb)"
1304  apply (induct queue arbitrary: qprev qhead)
1305   apply simp
1306  apply simp
1307  apply (erule disjE)
1308   apply clarsimp
1309   apply (case_tac "queue")
1310    apply clarsimp
1311   apply clarsimp
1312   apply (rule conjI)
1313    apply clarsimp
1314   apply clarsimp
1315   apply (drule_tac f=ctcb_ptr_to_tcb_ptr in arg_cong[where y="tp tcb"], simp)
1316  apply clarsimp
1317  apply fastforce
1318  done
1319
1320lemma tcb_queue_relation_prev_next':
1321  "\<lbrakk> tcb_queue_relation' tn tp mp queue qhead qend; tcbp \<in> set queue; distinct queue;
1322       \<forall>t \<in> set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<rbrakk>
1323      \<Longrightarrow> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue
1324                       \<and> mp (tn tcb) \<noteq> None \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp)
1325        \<and> (tp tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue
1326                       \<and> mp (tp tcb) \<noteq> None \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp)
1327        \<and> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<noteq> tp tcb)"
1328  apply (clarsimp simp: tcb_queue_relation'_def split: if_split_asm)
1329  apply (drule(1) tcb_queue_relation_prev_next, simp_all)
1330   apply (fastforce dest: tcb_at_not_NULL)
1331  apply clarsimp
1332  done
1333
1334(* L1 bitmap only updated if L2 entry bits end up all zero *)
1335lemma rf_sr_drop_bitmaps_dequeue_helper_L2:
1336  "\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ;
1337     cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk>
1338   \<Longrightarrow>
1339((\<sigma>\<lparr>ksReadyQueues := ksqupd,
1340   ksReadyQueuesL2Bitmap := ksqL2upd\<rparr>,
1341 \<sigma>'\<lparr>idx_' := i',
1342   queue_' := queue_upd',
1343   globals := globals \<sigma>'
1344     \<lparr>ksReadyQueuesL2Bitmap_' := ksqL2upd',
1345      ksReadyQueues_' := ksqupd'\<rparr>\<rparr>)
1346         \<in> rf_sr)
1347 =
1348((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>,
1349 \<sigma>'\<lparr>idx_' := i',
1350   queue_' := queue_upd',
1351   globals := globals \<sigma>'
1352     \<lparr>ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> rf_sr)
1353"
1354  unfolding rf_sr_def cstate_relation_def Let_def
1355             carch_state_relation_def cmachine_state_relation_def
1356  by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation)
1357
1358lemma rf_sr_drop_bitmaps_dequeue_helper:
1359  "\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ;
1360     cbitmap_L1_relation ksqL1upd' ksqL1upd ; cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk>
1361   \<Longrightarrow>
1362((\<sigma>\<lparr>ksReadyQueues := ksqupd,
1363   ksReadyQueuesL2Bitmap := ksqL2upd,
1364   ksReadyQueuesL1Bitmap := ksqL1upd\<rparr>,
1365 \<sigma>'\<lparr>idx_' := i',
1366   queue_' := queue_upd',
1367   globals := globals \<sigma>'
1368     \<lparr>ksReadyQueuesL2Bitmap_' := ksqL2upd',
1369      ksReadyQueuesL1Bitmap_' := ksqL1upd',
1370      ksReadyQueues_' := ksqupd'\<rparr>\<rparr>)
1371         \<in> rf_sr)
1372 =
1373((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>,
1374 \<sigma>'\<lparr>idx_' := i',
1375   queue_' := queue_upd',
1376   globals := globals \<sigma>'
1377     \<lparr>ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> rf_sr)
1378"
1379  unfolding rf_sr_def cstate_relation_def Let_def
1380             carch_state_relation_def cmachine_state_relation_def
1381  by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation)
1382
1383lemma filter_empty_unfiltered_contr:
1384  "\<lbrakk> [x\<leftarrow>xs . x \<noteq> y] = [] ; x' \<in> set xs ; x' \<noteq> y \<rbrakk> \<Longrightarrow> False"
1385  by (induct xs, auto split: if_split_asm)
1386
1387(* FIXME same proofs as bit_set, maybe can generalise? *)
1388lemma cbitmap_L1_relation_bit_clear:
1389  fixes p :: priority
1390  shows
1391  "\<lbrakk> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) ;
1392     d \<le> maxDomain \<rbrakk> \<Longrightarrow>
1393   cbitmap_L1_relation
1394           (Arrays.update (ksReadyQueuesL1Bitmap_' (globals x)) (unat d)
1395             (ksReadyQueuesL1Bitmap_' (globals x).[unat d] && ~~ 2 ^ unat (p >> wordRadix)))
1396           ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d && ~~ 2 ^ prioToL1Index p))"
1397  apply (unfold cbitmap_L1_relation_def)
1398  apply (clarsimp simp: prioToL1Index_def wordRadix_def' maxDomain_def numDomains_def word_le_nat_alt)
1399  done
1400
1401lemma cready_queues_relation_empty_queue_helper:
1402  "\<lbrakk> tcbDomain ko \<le> maxDomain ; tcbPriority ko \<le> maxPriority ;
1403     cready_queues_relation (cslift \<sigma>') (ksReadyQueues_' (globals \<sigma>')) (ksReadyQueues \<sigma>)\<rbrakk>
1404   \<Longrightarrow>
1405   cready_queues_relation (cslift \<sigma>')
1406          (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko))
1407            (tcb_queue_C.end_C_update (\<lambda>_. NULL)
1408              (head_C_update (\<lambda>_. NULL)
1409                (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))))
1410          ((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := []))"
1411  unfolding cready_queues_relation_def Let_def
1412  using maxPrio_to_H[simp] maxDom_to_H[simp]
1413  apply clarsimp
1414  apply (frule (1) cready_queues_index_to_C_in_range[simplified maxDom_to_H maxPrio_to_H])
1415  apply (fold cready_queues_index_to_C_def[simplified numPriorities_def])
1416  apply (case_tac "qdom = tcbDomain ko",
1417          simp_all add: prio_and_dom_limit_helpers seL4_MinPrio_def
1418                        minDom_def)
1419   apply (fastforce simp: cready_queues_index_to_C_in_range simp: cready_queues_index_to_C_distinct)+
1420  done
1421
1422lemma cbitmap_L2_relationD:
1423  "\<lbrakk> cbitmap_L2_relation cbitmap2 abitmap2 ; d \<le> maxDomain ; i < l2BitmapSize \<rbrakk> \<Longrightarrow>
1424    cbitmap2.[unat d].[i] = abitmap2 (d, i)"
1425  unfolding cbitmap_L2_relation_def l2BitmapSize_def'
1426  by clarsimp
1427
1428(* FIXME move *)
1429lemma filter_noteq_op:
1430  "[x \<leftarrow> xs . x \<noteq> y] = filter ((\<noteq>) y) xs"
1431  by (induct xs) auto
1432
1433(* FIXME move *)
1434lemma all_filter_propI:
1435  "\<forall>x\<in>set lst. P x \<Longrightarrow> \<forall>x\<in>set (filter Q lst). P x"
1436  by (induct lst, auto)
1437
1438lemma cbitmap_L2_relation_bit_clear:
1439  fixes p :: priority
1440  fixes d :: domain
1441  shows "\<lbrakk> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>) ;
1442           d \<le> maxDomain \<rbrakk>
1443         \<Longrightarrow>
1444         cbitmap_L2_relation
1445          (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d)
1446            (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d])
1447              (invertL1Index (prioToL1Index p))
1448              (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] &&
1449                ~~ 2 ^ unat (p && 0x3F))))
1450          ((ksReadyQueuesL2Bitmap \<sigma>)
1451           ((d, invertL1Index (prioToL1Index p)) :=
1452              ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) &&
1453                ~~ 2 ^ unat (p && mask wordRadix)))"
1454  unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def'
1455  apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def
1456                        invertL1Index_def l2BitmapSize_def'
1457                        maxDomain_def numDomains_def word_le_nat_alt)
1458  apply (case_tac "da = d" ; clarsimp)
1459  done
1460
1461lemma tcbSchedDequeue_ccorres':
1462  "ccorres dc xfdc
1463           ((\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s)
1464                     \<and> distinct (ksReadyQueues s (d, p)))
1465             and valid_queues' and tcb_at' t and valid_objs')
1466           (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>)
1467           []
1468           (tcbSchedDequeue t)
1469           (Call tcbSchedDequeue_'proc)"
1470proof -
1471
1472  note prio_and_dom_limit_helpers[simp] word_sle_def[simp]
1473
1474  have ksQ_tcb_at': "\<And>s ko d p.
1475    \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s)
1476                                          \<and> distinct (ksReadyQueues s (d, p)) \<Longrightarrow>
1477    \<forall>t\<in>set (ksReadyQueues s (d, p)). tcb_at' t s"
1478    by (fastforce dest: spec elim: obj_at'_weakenE)
1479
1480  have invert_l1_index_limit: "\<And>p. invertL1Index (prioToL1Index p) < 4"
1481    unfolding invertL1Index_def l2BitmapSize_def' prioToL1Index_def
1482    by simp
1483
1484  show ?thesis
1485  apply (cinit lift: tcb_')
1486   apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'"
1487            in ccorres_split_nothrow)
1488       apply (rule threadGet_vcg_corres)
1489       apply (rule allI, rule conseqPre, vcg)
1490       apply clarsimp
1491       apply (drule obj_at_ko_at', clarsimp)
1492       apply (drule spec, drule(1) mp, clarsimp)
1493       apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1494      apply ceqv
1495     apply (simp add: when_def del: Collect_const split del: if_split)
1496     apply (rule ccorres_cond[where R=\<top>])
1497       apply (simp add: to_bool_def)
1498      apply (rule ccorres_rhs_assoc)+
1499      apply csymbr
1500      apply csymbr
1501      apply csymbr
1502      apply csymbr
1503      apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="dom_'" in ccorres_split_nothrow)
1504          apply (rule threadGet_vcg_corres)
1505          apply (rule allI, rule conseqPre, vcg)
1506          apply clarsimp
1507          apply (drule obj_at_ko_at', clarsimp)
1508          apply (drule spec, drule(1) mp, clarsimp)
1509          apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1510         apply ceqv
1511        apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="prio_'" in ccorres_split_nothrow)
1512            apply (rule threadGet_vcg_corres)
1513            apply (rule allI, rule conseqPre, vcg)
1514            apply clarsimp
1515            apply (drule obj_at_ko_at', clarsimp)
1516            apply (drule spec, drule(1) mp, clarsimp)
1517            apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1518           apply ceqv
1519          apply (rule ccorres_rhs_assoc2)+
1520          apply (simp only: bind_assoc[symmetric])
1521          apply (rule ccorres_split_nothrow_novcg_dc)
1522             prefer 2
1523             apply (rule ccorres_move_c_guard_tcb)
1524             apply (simp only: dc_def[symmetric])
1525             apply ctac
1526            prefer 2
1527            apply (wp, clarsimp, wp+)
1528           apply (rule_tac P="(\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s)
1529                                         \<and> distinct(ksReadyQueues s (d, p)))
1530                                and valid_queues' and obj_at' (inQ rva rvb) t
1531                                and (\<lambda>s. rva \<le> maxDomain \<and> rvb \<le> maxPriority)"
1532                       and P'=UNIV in ccorres_from_vcg)
1533           apply (rule allI, rule conseqPre, vcg)
1534           apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def
1535                                 put_def bind_def return_def bitmap_fun_defs when_def
1536                                 null_def)
1537
1538           apply (rule conjI; clarsimp simp: queue_in_range[simplified maxDom_to_H maxPrio_to_H])
1539            apply (rule conjI; clarsimp simp: queue_in_range[simplified maxDom_to_H maxPrio_to_H])
1540             apply (frule(1) valid_queuesD')
1541             apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def)
1542             apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" in rf_sr_sched_queue_relation)
1543               apply (fastforce simp: maxDom_to_H maxPrio_to_H)+
1544             apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next'; (fastforce simp: ksQ_tcb_at')?)
1545             apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption,
1546                    simp_all add: remove1_filter ksQ_tcb_at')[1]
1547             apply (intro conjI;
1548                    clarsimp simp: h_val_field_clift'
1549                                   h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)+
1550               apply (drule(2) filter_empty_unfiltered_contr, simp)+
1551             apply (rule conjI; clarsimp)
1552              apply (rule conjI)
1553               apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
1554              apply (rule conjI; clarsimp)
1555               apply (subst rf_sr_drop_bitmaps_dequeue_helper, assumption)
1556                 apply (fastforce intro: cbitmap_L1_relation_bit_clear)
1557                apply (simp add: invert_prioToL1Index_c_simp)
1558                apply (frule rf_sr_cbitmap_L2_relation)
1559                apply (clarsimp simp: cbitmap_L2_relation_def
1560                                      word_size prioToL1Index_def wordRadix_def mask_def
1561                                      maxDomain_def numDomains_def word_le_nat_alt
1562                                      numPriorities_def wordBits_def l2BitmapSize_def'
1563                                      invertL1Index_def)
1564                apply (case_tac "d = tcbDomain ko" ; fastforce)
1565
1566               apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def)
1567               apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko"
1568                        in rf_sr_sched_queue_relation)
1569                 apply (fold_subgoals (prefix))[2]
1570                subgoal premises prems using prems by (fastforce simp: maxDom_to_H maxPrio_to_H)+
1571
1572               apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next', assumption)
1573                  prefer 3
1574                  apply fastforce
1575                 apply (fold_subgoals (prefix))[2]
1576                subgoal premises prems using prems by ((fastforce simp: ksQ_tcb_at')+)
1577               apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption,
1578                      simp_all add: remove1_filter ksQ_tcb_at')[1]
1579               (* trivial case, setting queue to empty *)
1580               apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
1581                                     cmachine_state_relation_def)
1582               apply (erule (2) cready_queues_relation_empty_queue_helper)
1583              (* impossible case, C L2 update disagrees with Haskell update *)
1584              apply (simp add: invert_prioToL1Index_c_simp)
1585              apply (subst (asm) Arrays.index_update)
1586               subgoal by (simp add: maxDomain_def numDomains_def word_le_nat_alt)
1587              apply (subst (asm) Arrays.index_update)
1588               apply (simp add: invert_l1_index_limit)
1589
1590              apply (frule rf_sr_cbitmap_L2_relation)
1591              apply (drule_tac i="invertL1Index (prioToL1Index (tcbPriority ko))"
1592                       in cbitmap_L2_relationD, assumption)
1593               apply (fastforce simp: l2BitmapSize_def' invert_l1_index_limit)
1594              apply (fastforce simp: prioToL1Index_def invertL1Index_def mask_def wordRadix_def)
1595             (* impossible case *)
1596             apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1597             apply (drule(2) filter_empty_unfiltered_contr, fastforce)
1598
1599            apply (frule (1) valid_queuesD')
1600            apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def)
1601            apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko"
1602                     in rf_sr_sched_queue_relation)
1603              apply fold_subgoals[2]
1604              apply (fastforce simp: maxDom_to_H maxPrio_to_H)+
1605            apply (clarsimp simp: h_val_field_clift'
1606                                  h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
1607            apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next', assumption)
1608               prefer 3
1609               apply fastforce
1610              apply (fold_subgoals (prefix))[2]
1611             subgoal premises prems using prems by (fastforce simp: ksQ_tcb_at')+
1612            apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption,
1613                   simp_all add: remove1_filter ksQ_tcb_at')[1]
1614            apply (clarsimp simp:  filter_noteq_op upd_unless_null_def)
1615            apply (rule conjI, clarsimp)
1616             apply (clarsimp simp: h_val_field_clift'
1617                                   h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
1618             apply (rule conjI; clarsimp)
1619              apply (simp add: typ_heap_simps)
1620              apply (clarsimp simp: h_t_valid_c_guard [OF h_t_valid_field, OF h_t_valid_clift]
1621                                    h_t_valid_field[OF h_t_valid_clift] h_t_valid_clift)
1622              apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
1623                       in state_relation_queue_update_helper',
1624                     (simp | rule globals.equality)+,
1625                     simp_all add: clift_field_update if_Some_helper numPriorities_def
1626                                   cready_queues_index_to_C_def2 typ_heap_simps
1627                                   maxDom_to_H maxPrio_to_H
1628                             cong: if_cong split del: if_split)[1]
1629
1630               apply (fastforce simp: tcb_null_sched_ptrs_def typ_heap_simps c_guard_clift
1631                                elim: obj_at'_weaken)+
1632             apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
1633                      in state_relation_queue_update_helper',
1634                    (simp | rule globals.equality)+,
1635                    simp_all add: clift_field_update if_Some_helper numPriorities_def
1636                                  cready_queues_index_to_C_def2
1637                                  maxDom_to_H maxPrio_to_H
1638                            cong: if_cong split del: if_split,
1639                    simp_all add: typ_heap_simps')[1]
1640               subgoal by (fastforce simp: tcb_null_sched_ptrs_def)
1641              subgoal by (simp add: fpu_state_preservation[OF _ h_t_valid_clift] typ_heap_simps')
1642             subgoal by fastforce
1643            apply clarsimp
1644            apply (rule conjI; clarsimp)
1645             apply (rule conjI)
1646              apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
1647             apply (rule conjI; clarsimp)
1648              (* invalid, missing bitmap updates on haskell side *)
1649              apply (fold_subgoals (prefix))[2]
1650             subgoal premises prems using prems
1651               by (fastforce dest!: tcb_queue_relation'_empty_ksReadyQueues
1652                              elim: obj_at'_weaken)+
1653            apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1654            apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
1655                     in state_relation_queue_update_helper',
1656                   (simp | rule globals.equality)+,
1657                   simp_all add: clift_field_update if_Some_helper numPriorities_def
1658                                 cready_queues_index_to_C_def2
1659                                 maxDom_to_H maxPrio_to_H
1660                           cong: if_cong split del: if_split)[1]
1661               apply (fold_subgoals (prefix))[4]
1662            subgoal premises prems using prems
1663              by - (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def
1664                                    clift_heap_update_same[OF h_t_valid_clift]
1665                                    fpu_state_preservation[OF _ h_t_valid_clift])+
1666           apply (rule conjI; clarsimp simp: queue_in_range[simplified maxDom_to_H maxPrio_to_H])
1667            apply (frule (1) valid_queuesD')
1668            apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def)
1669            apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko"
1670                     in rf_sr_sched_queue_relation)
1671              apply (fold_subgoals (prefix))[2]
1672             subgoal premises prems using prems by (fastforce simp: maxDom_to_H maxPrio_to_H)+
1673            apply (clarsimp simp: h_val_field_clift'
1674                                  h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
1675            apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next')
1676                apply fastforce
1677               prefer 3
1678               apply fastforce
1679              apply (fold_subgoals (prefix))[2]
1680             subgoal premises prems using prems by (fastforce simp: ksQ_tcb_at')+
1681            apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption,
1682                   simp_all add: remove1_filter ksQ_tcb_at')[1]
1683            apply (clarsimp simp:  filter_noteq_op upd_unless_null_def)
1684            apply (rule conjI; clarsimp)
1685             apply (clarsimp simp: h_val_field_clift'
1686                                   h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
1687             apply (clarsimp simp: typ_heap_simps)
1688             apply (rule conjI; clarsimp simp: typ_heap_simps)
1689             apply (drule(2) filter_empty_unfiltered_contr[simplified filter_noteq_op], simp)
1690            apply (rule conjI)
1691             apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
1692            apply (rule conjI; clarsimp)
1693             (* impossible case, C L2 update disagrees with Haskell update *)
1694             apply (subst (asm) Arrays.index_update)
1695              apply (simp add: maxDomain_def numDomains_def word_le_nat_alt)
1696             apply (subst (asm) Arrays.index_update)
1697              subgoal using invert_l1_index_limit
1698                by (fastforce simp add: invert_prioToL1Index_c_simp intro: nat_Suc_less_le_imp)
1699             apply (frule rf_sr_cbitmap_L2_relation)
1700             apply (simp add: invert_prioToL1Index_c_simp)
1701             apply (drule_tac i="invertL1Index (prioToL1Index (tcbPriority ko))"
1702                      in cbitmap_L2_relationD, assumption)
1703              subgoal by (simp add: invert_l1_index_limit l2BitmapSize_def')
1704             apply (fastforce simp: prioToL1Index_def invertL1Index_def mask_def wordRadix_def)
1705
1706            apply (simp add: invert_prioToL1Index_c_simp)
1707            apply (subst rf_sr_drop_bitmaps_dequeue_helper_L2, assumption)
1708             subgoal by (fastforce dest: rf_sr_cbitmap_L2_relation elim!: cbitmap_L2_relation_bit_clear)
1709
1710            (* trivial case, setting queue to empty *)
1711            apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
1712                                  cmachine_state_relation_def)
1713            apply (erule (2) cready_queues_relation_empty_queue_helper)
1714
1715           apply (frule (1) valid_queuesD')
1716           apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def)
1717           apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko"
1718                    in rf_sr_sched_queue_relation)
1719             apply (fold_subgoals (prefix))[2]
1720            subgoal premises prems using prems by (fastforce simp: maxDom_to_H maxPrio_to_H)+
1721           apply (clarsimp simp: h_val_field_clift'
1722                                 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
1723           apply (simp add: invert_prioToL1Index_c_simp)
1724           apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next')
1725               apply (fastforce simp add: ksQ_tcb_at')+
1726           apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption,
1727                  simp_all add: remove1_filter ksQ_tcb_at')[1]
1728           apply (clarsimp simp: filter_noteq_op upd_unless_null_def)
1729           apply (rule conjI, clarsimp)
1730            apply (clarsimp simp: h_val_field_clift'
1731                                  h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
1732            apply (clarsimp simp: typ_heap_simps)
1733            apply (rule conjI; clarsimp simp: typ_heap_simps)
1734             apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
1735                      in state_relation_queue_update_helper',
1736                    (simp | rule globals.equality)+,
1737                    simp_all add: clift_field_update if_Some_helper numPriorities_def
1738                                  cready_queues_index_to_C_def2
1739                                  maxDom_to_H maxPrio_to_H
1740                            cong: if_cong split del: if_split)[1]
1741                apply (fastforce simp: tcb_null_sched_ptrs_def)
1742               apply (clarsimp simp: typ_heap_simps)
1743              apply (fastforce simp: typ_heap_simps)
1744             apply (fastforce simp: tcb_null_sched_ptrs_def)
1745            apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
1746                     in state_relation_queue_update_helper',
1747                   (simp | rule globals.equality)+,
1748                   simp_all add: clift_field_update if_Some_helper numPriorities_def
1749                                 cready_queues_index_to_C_def2
1750                                 maxDom_to_H maxPrio_to_H
1751                           cong: if_cong split del: if_split)[1]
1752               apply (fold_subgoals (prefix))[4]
1753            subgoal premises prems using prems
1754              by - (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def
1755                                    clift_heap_update_same[OF h_t_valid_clift]
1756                                    fpu_state_preservation[OF _ h_t_valid_clift])+
1757           apply (clarsimp)
1758           apply (rule conjI; clarsimp simp: typ_heap_simps)
1759            apply (rule conjI)
1760             apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
1761            apply (rule conjI; clarsimp)
1762             (* invalid, missing bitmap updates on haskell side *)
1763             apply (drule tcb_queue_relation'_empty_ksReadyQueues)
1764              apply (fold_subgoals (prefix))[2]
1765             subgoal premises prems using prems by (fastforce elim: obj_at'_weaken)+
1766            (* invalid, missing bitmap updates on haskell side *)
1767            apply (drule tcb_queue_relation'_empty_ksReadyQueues)
1768             apply (fold_subgoals (prefix))[2]
1769            subgoal premises prems using prems by (fastforce elim: obj_at'_weaken)+
1770           apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
1771                    in state_relation_queue_update_helper',
1772                  (simp | rule globals.equality)+,
1773                  simp_all add: clift_field_update if_Some_helper numPriorities_def
1774                                cready_queues_index_to_C_def2 typ_heap_simps
1775                                maxDom_to_H maxPrio_to_H
1776                          cong: if_cong split del: if_split)[1]
1777            apply (fold_subgoals (prefix))[2]
1778           subgoal premises prems using prems
1779            by (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def)+
1780          apply (simp add: guard_is_UNIV_def)
1781         apply simp
1782         apply (wp threadGet_wp)
1783        apply vcg
1784       apply simp
1785       apply (wp threadGet_wp)
1786      apply vcg
1787     apply (rule ccorres_return_Skip[unfolded dc_def])
1788    apply simp
1789    apply (wp threadGet_wp)
1790   apply vcg
1791  by (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def
1792                      valid_obj'_def valid_tcb'_def inQ_def)
1793qed
1794
1795lemma tcbSchedDequeue_ccorres:
1796  "ccorres dc xfdc
1797           (valid_queues and valid_queues' and tcb_at' t and valid_objs')
1798           (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>)
1799           []
1800           (tcbSchedDequeue t)
1801           (Call tcbSchedDequeue_'proc)"
1802  apply (rule ccorres_guard_imp [OF tcbSchedDequeue_ccorres'])
1803   apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def)
1804   apply (drule_tac x=d in spec)
1805   apply (drule_tac x=p in spec)
1806   apply (clarsimp)
1807   apply (drule(1) bspec)
1808   apply (erule obj_at'_weakenE)
1809   apply (clarsimp)+
1810  done
1811
1812lemma tcb_queue_relation_append:
1813  "\<lbrakk> tcb_queue_relation tn tp mp queue qprev qhead; queue \<noteq> [];
1814     qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb;
1815     queue = queue' @ [ctcb_ptr_to_tcb_ptr qend]; distinct queue;
1816     \<forall>x \<in> set queue. tcb_ptr_to_ctcb_ptr x \<noteq> NULL; qend' \<noteq> NULL;
1817     \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v)
1818                \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v \<rbrakk>
1819    \<Longrightarrow> tcb_queue_relation tn tp
1820          (mp (qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)),
1821               qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb)))
1822          (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev qhead"
1823  using [[hypsubst_thin = true]]
1824  apply clarsimp
1825  apply (induct queue' arbitrary: qprev qhead)
1826   apply clarsimp
1827  apply clarsimp
1828  done
1829
1830lemma tcbSchedAppend_update:
1831  assumes sr: "sched_queue_relation' mp queue qhead qend"
1832  and     qh': "qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue"
1833  and  cs_tcb: "mp qend' = Some tcb"
1834  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
1835  and     qhN: "qend' \<noteq> NULL"
1836  shows
1837  "sched_queue_relation'
1838            (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend)))
1839                (mp(qend' \<mapsto> tcb\<lparr>tcbSchedNext_C := NULL, tcbSchedPrev_C := qend\<rparr>)))
1840            (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend'"
1841  using sr qh' valid_ep cs_tcb qhN
1842  apply -
1843  apply (rule rev_cases[where xs=queue])
1844   apply (simp add: tcb_queue_relation'_def upd_unless_null_def)
1845  apply (clarsimp simp: tcb_queue_relation'_def upd_unless_null_def tcb_at_not_NULL)
1846  apply (drule_tac qend'=qend' and tn_update=tcbSchedNext_C_update
1847             and tp_update=tcbSchedPrev_C_update and qend="tcb_ptr_to_ctcb_ptr y"
1848             in tcb_queue_relation_append, simp_all)
1849   apply (fastforce simp add: tcb_at_not_NULL)
1850  apply (simp add: fun_upd_twist)
1851  done
1852
1853lemma tcb_queue_relation_qend_mems:
1854  "\<lbrakk> tcb_queue_relation' getNext getPrev mp queue qhead qend;
1855     \<forall>x \<in> set queue. tcb_at' x s \<rbrakk>
1856      \<Longrightarrow> (qend = NULL \<longrightarrow> queue = [])
1857       \<and> (qend \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qend \<in> set queue)"
1858  apply (clarsimp simp: tcb_queue_relation'_def)
1859  apply (drule bspec, erule last_in_set)
1860  apply (simp add: tcb_at_not_NULL)
1861  done
1862
1863lemma tcbSchedAppend_ccorres:
1864  "ccorres dc xfdc
1865           (valid_queues and tcb_at' t and valid_objs')
1866           (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>)
1867           []
1868           (tcbSchedAppend t)
1869           (Call tcbSchedAppend_'proc)"
1870proof -
1871  note prio_and_dom_limit_helpers[simp] word_sle_def[simp] maxDom_to_H[simp] maxPrio_to_H[simp]
1872
1873  show ?thesis
1874  apply (cinit lift: tcb_')
1875   apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'"
1876               and xf'="ret__unsigned_longlong_'" in ccorres_split_nothrow)
1877       apply (rule threadGet_vcg_corres)
1878       apply (rule allI, rule conseqPre, vcg)
1879       apply clarsimp
1880       apply (drule obj_at_ko_at', clarsimp)
1881       apply (drule spec, drule(1) mp, clarsimp)
1882       apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1883      apply ceqv
1884     apply (simp add: when_def unless_def del: Collect_const split del: if_split)
1885     apply (rule ccorres_cond[where R=\<top>])
1886       apply (simp add: to_bool_def)
1887      apply (rule ccorres_rhs_assoc)+
1888      apply csymbr
1889      apply csymbr
1890      apply csymbr
1891      apply csymbr
1892      apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv"
1893          and xf'="dom_'" in ccorres_split_nothrow)
1894          apply (rule threadGet_vcg_corres)
1895          apply (rule allI, rule conseqPre, vcg)
1896          apply clarsimp
1897          apply (drule obj_at_ko_at', clarsimp)
1898          apply (drule spec, drule(1) mp, clarsimp)
1899          apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1900         apply ceqv
1901        apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv"
1902            and xf'="prio_'" in ccorres_split_nothrow)
1903            apply (rule threadGet_vcg_corres)
1904            apply (rule allI, rule conseqPre, vcg)
1905            apply clarsimp
1906            apply (drule obj_at_ko_at', clarsimp)
1907            apply (drule spec, drule(1) mp, clarsimp)
1908            apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
1909           apply ceqv
1910          apply (rule ccorres_rhs_assoc2)+
1911          apply (simp only: bind_assoc[symmetric])
1912          apply (rule ccorres_split_nothrow_novcg_dc)
1913             prefer 2
1914             apply (rule ccorres_move_c_guard_tcb)
1915             apply (simp only: dc_def[symmetric])
1916             apply ctac
1917            prefer 2
1918            apply (wp, clarsimp, wp+)
1919           apply (rule_tac P="\<lambda>s. valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p))
1920                                  \<and> (\<exists>tcb. ko_at' tcb t s \<and> tcbDomain tcb =rva
1921                                  \<and> tcbPriority tcb = rvb \<and> valid_tcb' tcb s)"
1922                       and P'=UNIV in ccorres_from_vcg)
1923           apply (rule allI, rule conseqPre, vcg)
1924           apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def
1925                                 put_def bind_def return_def bitmap_fun_defs null_def)
1926           apply (clarsimp simp: queue_in_range valid_tcb'_def)
1927           apply (rule conjI; clarsimp simp: queue_in_range)
1928            apply (drule (1) obj_at_cslift_tcb)
1929            apply clarsimp
1930            apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb"
1931                     in rf_sr_sched_queue_relation)
1932              apply clarsimp
1933             apply clarsimp
1934            apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL)
1935             apply (simp add: valid_queues_valid_q)
1936            apply (frule_tac s=\<sigma> in tcb_queue_relation_qend_mems,  simp add: valid_queues_valid_q)
1937            apply (drule_tac qend'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedAppend_update,
1938                   simp_all add: valid_queues_valid_q)[1]
1939             apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
1940            apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1941            apply (simp add: invert_prioToL1Index_c_simp)
1942            apply (rule conjI; clarsimp)
1943             apply (rule conjI)
1944              apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
1945             apply (simp add: t_hrs_ksReadyQueues_upd_absorb)
1946             apply (subst rf_sr_drop_bitmaps_enqueue_helper, assumption)
1947               apply (fastforce intro: cbitmap_L1_relation_bit_set)
1948              subgoal by (fastforce intro: cbitmap_L2_relation_bit_set simp: wordRadix_def mask_def)
1949             apply (erule(1) state_relation_queue_update_helper[where S="{t}"],
1950                    (simp | rule globals.equality)+,
1951                    simp_all add: cready_queues_index_to_C_def2 numPriorities_def
1952                                  t_hrs_ksReadyQueues_upd_absorb upd_unless_null_def
1953                                  typ_heap_simps)[1]
1954               apply (fastforce simp: tcb_null_sched_ptrs_def elim: obj_at'_weaken)
1955             apply (fastforce simp: tcb_null_sched_ptrs_def elim: obj_at'_weaken)
1956            apply (clarsimp simp: upd_unless_null_def cready_queues_index_to_C_def numPriorities_def)
1957           apply (rule conjI; clarsimp simp: queue_in_range)
1958            apply (drule (1) obj_at_cslift_tcb)
1959            apply clarsimp
1960            apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb"
1961                     in rf_sr_sched_queue_relation)
1962              apply clarsimp
1963             apply clarsimp
1964            apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL)
1965             apply (simp add: valid_queues_valid_q)
1966            apply (frule_tac s=\<sigma> in tcb_queue_relation_qend_mems,
1967                   simp add: valid_queues_valid_q)
1968            apply (drule_tac qend'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedAppend_update,
1969                   simp_all add: valid_queues_valid_q)[1]
1970              apply clarsimp
1971             apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
1972            apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1973            apply (clarsimp simp: upd_unless_null_def cready_queues_index_to_C_def numPriorities_def)
1974           apply (drule (1) obj_at_cslift_tcb)
1975           apply clarsimp
1976           apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb"
1977                    in rf_sr_sched_queue_relation)
1978             apply clarsimp
1979            apply clarsimp
1980           apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL)
1981            apply (simp add: valid_queues_valid_q)
1982           apply (frule_tac s=\<sigma> in tcb_queue_relation_qend_mems,
1983                  simp add: valid_queues_valid_q)
1984           apply (drule_tac qend'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedAppend_update,
1985                  simp_all add: valid_queues_valid_q)[1]
1986             apply clarsimp
1987            apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
1988           apply (clarsimp simp: cready_queues_index_to_C_def2 numPriorities_def)
1989           apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D])
1990           apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
1991           apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper,
1992                  (simp | rule globals.equality)+,
1993                  simp_all add: typ_heap_simps if_Some_helper numPriorities_def
1994                                cready_queues_index_to_C_def2 upd_unless_null_def
1995                           cong: if_cong split del: if_split
1996                           del: fun_upd_restrict_conv)[1]
1997              apply simp
1998              apply (rule conjI)
1999               apply clarsimp
2000               apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp)
2001              apply (clarsimp simp add: fun_upd_twist)
2002             prefer 3
2003             apply (simp add: obj_at'_weakenE[OF _ TrueI])
2004             apply (rule disjI1, erule valid_queues_obj_at'D)
2005             subgoal by simp
2006            subgoal by simp
2007           subgoal by (fastforce simp: tcb_null_sched_ptrs_def)
2008          apply (simp add: guard_is_UNIV_def)
2009         apply simp
2010         apply (wp threadGet_wp)
2011        apply vcg
2012       apply simp
2013       apply (wp threadGet_wp)
2014      apply vcg
2015     apply (rule ccorres_return_Skip[unfolded dc_def])
2016    apply simp
2017    apply (wp threadGet_wp)
2018   apply vcg
2019  by (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def
2020                         valid_obj'_def inQ_def
2021                   dest!: valid_queues_obj_at'D)
2022qed
2023
2024lemma true_eq_from_bool [simp]:
2025  "(scast true = from_bool P) = P"
2026  by (simp add: true_def from_bool_def split: bool.splits)
2027
2028lemma isBlocked_spec:
2029  "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isBlocked_'proc
2030       {s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in>
2031                            {scast ThreadState_BlockedOnReply,
2032                             scast ThreadState_BlockedOnNotification, scast ThreadState_BlockedOnSend,
2033                             scast ThreadState_BlockedOnReceive, scast ThreadState_Inactive}) }"
2034  apply vcg
2035  apply (clarsimp simp: typ_heap_simps)
2036done
2037
2038lemma isRunnable_spec:
2039  "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isRunnable_'proc
2040       {s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in>
2041                            { scast ThreadState_Running, scast ThreadState_Restart })}"
2042  apply vcg
2043  apply (clarsimp simp: typ_heap_simps)
2044done
2045
2046(* FIXME: move *)
2047lemma ccorres_setSchedulerAction:
2048  "cscheduler_action_relation a p \<Longrightarrow>
2049  ccorres dc xfdc \<top> UNIV hs
2050      (setSchedulerAction a)
2051      (Basic (\<lambda>s. globals_update (ksSchedulerAction_'_update (\<lambda>_. p)) s))"
2052  apply (rule ccorres_from_vcg)
2053  apply (rule allI, rule conseqPre, vcg)
2054  apply (clarsimp simp: setSchedulerAction_def modify_def get_def put_def bind_def)
2055  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def cmachine_state_relation_def)
2056  done
2057
2058declare ge_0_from_bool [simp]
2059
2060lemma scheduler_action_case_switch_to_if:
2061  "(case act of SwitchToThread t \<Rightarrow> f t | _ \<Rightarrow> g)
2062      = (if \<exists>t. act = SwitchToThread t
2063            then f (case act of SwitchToThread t \<Rightarrow> t) else g)"
2064  by (simp split: scheduler_action.split)
2065
2066lemma tcb_at_1:
2067  "tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr 1"
2068  apply (drule is_aligned_tcb_ptr_to_ctcb_ptr)
2069  apply (clarsimp simp add: is_aligned_def max_word_def ctcb_size_bits_def)
2070  done
2071
2072lemma rescheduleRequired_ccorres:
2073  "ccorres dc xfdc (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs')
2074           UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)"
2075  apply cinit
2076   apply (rule ccorres_symb_exec_l)
2077      apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc])
2078          apply (simp add: scheduler_action_case_switch_to_if
2079                      cong: if_weak_cong split del: if_split)
2080          apply (rule_tac R="\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s"
2081                     in ccorres_cond)
2082            apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2083                                  cscheduler_action_relation_def)
2084            subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
2085                           split: scheduler_action.split_asm dest!: pred_tcb_at')
2086           apply (ctac add: tcbSchedEnqueue_ccorres)
2087          apply (rule ccorres_return_Skip)
2088         apply ceqv
2089        apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
2090        apply (rule allI, rule conseqPre, vcg)
2091        apply (clarsimp simp: setSchedulerAction_def simpler_modify_def)
2092        subgoal by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2093                              cscheduler_action_relation_def
2094                              carch_state_relation_def cmachine_state_relation_def
2095                              max_word_def)
2096       apply wp
2097      apply (simp add: guard_is_UNIV_def)
2098     apply wp+
2099   apply (simp add: getSchedulerAction_def)
2100  apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
2101                        Let_def cscheduler_action_relation_def)
2102  by (auto simp: tcb_at_not_NULL tcb_at_1
2103                    tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
2104                 split: scheduler_action.split_asm)
2105
2106lemma getReadyQueuesL1Bitmap_sp:
2107  "\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<rbrace>
2108   getReadyQueuesL1Bitmap d
2109   \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d = rv \<and> d \<le> maxDomain \<and> P s\<rbrace>"
2110  unfolding bitmap_fun_defs
2111  by wp simp
2112
2113(* this doesn't actually carry over d \<le> maxDomain to the rest of the ccorres,
2114   use ccorres_cross_over_guard to do that *)
2115lemma ccorres_pre_getReadyQueuesL1Bitmap:
2116  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
2117  shows   "ccorres r xf
2118                  (\<lambda>s. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> P rv s))
2119                  {s. \<forall>rv. (ksReadyQueuesL1Bitmap_' (globals s)).[unat d] = ucast rv
2120                                 \<longrightarrow> s \<in> P' rv }
2121                          hs (getReadyQueuesL1Bitmap d >>= (\<lambda>rv. f rv)) c"
2122  apply (rule ccorres_guard_imp)
2123  apply (rule ccorres_symb_exec_l2)
2124      defer
2125      defer
2126      apply (rule getReadyQueuesL1Bitmap_sp)
2127     apply blast
2128    apply clarsimp
2129    prefer 3
2130    apply (clarsimp simp: bitmap_fun_defs gets_exs_valid)
2131   defer
2132   apply (rule ccorres_guard_imp)
2133     apply (rule cc)
2134    apply blast
2135   apply assumption
2136  apply (drule rf_sr_cbitmap_L1_relation)
2137  apply (clarsimp simp: cbitmap_L1_relation_def)
2138  done
2139
2140lemma getReadyQueuesL2Bitmap_sp:
2141  "\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<rbrace>
2142   getReadyQueuesL2Bitmap d i
2143   \<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> P s\<rbrace>"
2144  unfolding bitmap_fun_defs
2145  by wp simp
2146
2147lemma ccorres_pre_getReadyQueuesL2Bitmap:
2148  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
2149  shows   "ccorres r xf
2150                  (\<lambda>s. d \<le> maxDomain \<and> i < l2BitmapSize
2151                       \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d,i) = rv \<longrightarrow> P rv s))
2152                  {s. \<forall>rv. (ksReadyQueuesL2Bitmap_' (globals s)).[unat d].[i] = ucast rv
2153                                 \<longrightarrow> s \<in> P' rv }
2154                          hs (getReadyQueuesL2Bitmap d i >>= (\<lambda>rv. f rv)) c"
2155  apply (rule ccorres_guard_imp)
2156  apply (rule ccorres_symb_exec_l2)
2157      defer
2158      defer
2159      apply (rule getReadyQueuesL2Bitmap_sp)
2160     apply blast
2161    apply clarsimp
2162    prefer 3
2163    apply (clarsimp simp: bitmap_fun_defs gets_exs_valid)
2164   defer
2165   apply (rule ccorres_guard_imp)
2166     apply (rule cc)
2167    apply blast
2168   apply assumption
2169  apply (drule rf_sr_cbitmap_L2_relation)
2170  apply (clarsimp simp: cbitmap_L2_relation_def)
2171  done
2172
2173lemma rf_sr_ksReadyQueuesL1Bitmap_simp:
2174  "\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain \<rbrakk>
2175  \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap \<sigma> d"
2176  apply (drule rf_sr_cbitmap_L1_relation)
2177  apply (simp add: cbitmap_L1_relation_def)
2178  done
2179
2180lemma cguard_UNIV:
2181  "P s \<Longrightarrow> s \<in> (if P s then UNIV else {})"
2182  by fastforce
2183
2184lemma lookupBitmapPriority_le_maxPriority:
2185  "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; valid_queues s \<rbrakk>
2186   \<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority"
2187   unfolding valid_queues_def valid_queues_no_bitmap_def
2188   by (fastforce dest!: bitmapQ_from_bitmap_lookup bitmapQ_ksReadyQueuesI intro: ccontr)
2189
2190lemma rf_sr_ksReadyQueuesL1Bitmap_not_zero:
2191  "\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<rbrakk>
2192  \<Longrightarrow> ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0"
2193  apply (drule rf_sr_cbitmap_L1_relation)
2194  apply (simp add: cbitmap_L1_relation_def)
2195  done
2196
2197lemma ksReadyQueuesL1Bitmap_word_log2_max:
2198    "\<lbrakk>valid_queues s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk>
2199    \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize"
2200    unfolding valid_queues_def
2201    by (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD)
2202
2203lemma word_log2_max_word64[simp]:
2204  "word_log2 (w :: 64 word) < 64"
2205  using word_log2_max[where w=w]
2206  by (simp add: word_size)
2207
2208lemma rf_sr_ksReadyQueuesL2Bitmap_simp:
2209  "\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; valid_queues \<sigma> ; ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0 \<rbrakk>
2210   \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[word_log2 (ksReadyQueuesL1Bitmap \<sigma> d)] =
2211      ksReadyQueuesL2Bitmap \<sigma> (d, word_log2 (ksReadyQueuesL1Bitmap \<sigma> d))"
2212  apply (frule rf_sr_cbitmap_L2_relation)
2213  apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
2214  apply (drule (3) cbitmap_L2_relationD)
2215  done
2216
2217lemma ksReadyQueuesL2Bitmap_nonzeroI:
2218  "\<lbrakk> d \<le> maxDomain ; valid_queues s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
2219   \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0"
2220   unfolding valid_queues_def
2221   apply clarsimp
2222   apply (frule bitmapQ_no_L1_orphansD)
2223    apply (erule word_log2_nth_same)
2224   apply clarsimp
2225   done
2226
2227lemma clzl_spec:
2228  "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc
2229       \<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"
2230  apply (rule allI, rule conseqPre, vcg)
2231  apply clarsimp
2232  apply (rule_tac x="ret__long_'_update f x" for f in exI)
2233  apply (simp add: mex_def meq_def)
2234  done
2235
2236lemma l1index_to_prio_spec:
2237  "\<forall>s. \<Gamma> \<turnstile> {s} Call l1index_to_prio_'proc
2238       \<lbrace>\<acute>ret__unsigned_long = l1index_' s << wordRadix \<rbrace>"
2239  by vcg (simp add: word_sle_def wordRadix_def')
2240
2241lemma getHighestPrio_ccorres:
2242  "ccorres (\<lambda>rv rv'. rv' = ucast rv) ret__unsigned_long_'
2243    (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s)
2244    (UNIV \<inter> {s. dom_' s = ucast d}) hs
2245    (getHighestPrio d) (Call getHighestPrio_'proc)"
2246proof -
2247
2248  note prio_and_dom_limit_helpers [simp]
2249  note Collect_const_mem [simp]
2250
2251  have signed_word_log2:
2252  "\<And>w. w \<noteq> 0 \<Longrightarrow> (0x3F::64 signed word) - of_nat (word_clz (w::machine_word)) = (of_nat (word_log2 w))"
2253  unfolding word_log2_def
2254  by (clarsimp dest!: word_clz_nonzero_max simp: word_size)
2255
2256  have word_log2_def64:
2257    "\<And>w. word_log2 (w::machine_word) = 63 - word_clz w"
2258    unfolding word_log2_def by (simp add: word_size)
2259
2260  (* FIXME generalise *)
2261  have word_clz_sint_upper[simp]:
2262    "\<And>(w::machine_word). sint (of_nat (word_clz w) :: 64 signed word) \<le> 9223372036854775871"
2263    apply (subst sint_eq_uint)
2264     apply (rule not_msb_from_less)
2265     apply simp
2266     apply (rule word_of_nat_less)
2267     apply simp
2268     apply (rule order_le_less_trans[OF word_clz_max])
2269     apply (simp add: word_size)
2270    apply (subst uint_nat)
2271    apply (simp add: unat_of_nat)
2272    apply (subst Divides.mod_less, simp)
2273     apply (rule order_le_less_trans[OF word_clz_max])
2274     apply (simp add: word_size)
2275    apply (rule iffD2 [OF le_nat_iff[symmetric]])
2276    apply simp
2277    apply (rule order_trans[OF word_clz_max])
2278    apply (simp add: word_size)
2279    done
2280
2281  have word_clz_sint_lower[simp]:
2282    "\<And>(w::machine_word). - sint (of_nat (word_clz w) :: 64 signed word) \<le> 9223372036854775744"
2283    apply (subst sint_eq_uint)
2284     apply (rule not_msb_from_less)
2285     apply simp
2286     apply (rule word_of_nat_less)
2287     apply simp
2288     apply (rule order_le_less_trans[OF word_clz_max])
2289     apply (simp add: word_size)
2290    apply (subst uint_nat)
2291    apply (simp add: unat_of_nat)
2292    done
2293
2294  have invertL1Index_unat_fold:
2295    "\<And>(w::machine_word). \<lbrakk> w \<noteq> 0 ; word_log2 w < l2BitmapSize \<rbrakk> \<Longrightarrow>
2296       unat (of_nat l2BitmapSize - (1::machine_word) - of_nat (word_log2 w))
2297     = invertL1Index (word_log2 w)"
2298    apply (subst unat_sub)
2299     apply (clarsimp simp: l2BitmapSize_def')
2300     apply (rule word_of_nat_le)
2301     apply (drule word_log2_nth_same)
2302     apply (clarsimp simp: l2BitmapSize_def')
2303    apply (clarsimp simp: invertL1Index_def l2BitmapSize_def')
2304    apply (simp add: unat_of_nat_eq)
2305    done
2306
2307  show ?thesis
2308  apply (cinit lift: dom_')
2309   apply (clarsimp split del: if_split)
2310   apply (rule ccorres_pre_getReadyQueuesL1Bitmap)
2311   apply (rule ccorres_pre_getReadyQueuesL2Bitmap)
2312   apply (rename_tac l2)
2313   apply (rule ccorres_Guard_Seq|csymbr)+
2314   apply (rule ccorres_abstract_cleanup)
2315   apply (rule ccorres_Guard_Seq|csymbr)+
2316   apply (rule ccorres_abstract_cleanup)
2317   apply (rule ccorres_Guard_Seq|csymbr)+
2318   apply (clarsimp simp: word_log2_def word_size)
2319   apply (rename_tac clz_l1index clz_l2index)
2320   apply (rule_tac P="\<lambda>s. l1 \<noteq> 0 \<and> l2 \<noteq> 0 \<and> word_log2 l1 < l2BitmapSize"
2321            and P'="{s. clz_l1index = of_nat (word_clz l1) \<and>
2322                        clz_l2index = of_nat (word_clz l2) }"
2323            in ccorres_from_vcg_throws)
2324   apply (rule allI, rule conseqPre, vcg)
2325    subgoal for l1 l2 _ _ _
2326    apply (clarsimp simp: return_def l1IndexToPrio_def)
2327    apply (simp add: signed_word_log2 word_log2_def64[symmetric] ucast_or_distrib)
2328    apply (rule_tac f="(||)" in arg_cong2)
2329     apply (subst of_nat_shiftl)+
2330     apply (subst ucast_of_nat_small, simp add: wordRadix_def l2BitmapSize_def')
2331     apply (rule refl)
2332    apply (subst ucast_of_nat_small, simp add: wordRadix_def)
2333     apply (rule word_log2_max_word64[THEN order_less_le_trans], simp)
2334    apply (rule refl)
2335    done
2336   apply (clarsimp simp: word_sle_def)
2337
2338   apply (frule rf_sr_cbitmap_L1_relation)
2339   apply (subgoal_tac "ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0")
2340    prefer 2
2341    subgoal by (fastforce simp: cbitmap_L1_relation_def)
2342
2343   apply (clarsimp simp: signed_word_log2 cbitmap_L1_relation_def)
2344   apply (frule bitmapQ_no_L1_orphansD, erule word_log2_nth_same)
2345   apply simp
2346   apply (rule conjI, fastforce simp: invertL1Index_def l2BitmapSize_def')
2347   apply (rule conjI, fastforce simp: invertL1Index_unat_fold)
2348   apply (rule conjI)
2349    apply (subst invertL1Index_unat_fold, assumption, fastforce)
2350    apply (frule rf_sr_cbitmap_L2_relation)
2351    apply (fastforce simp: cbitmap_L2_relation_def)
2352   apply (clarsimp simp: l2BitmapSize_def')
2353   apply (fastforce simp: word_less_nat_alt word_le_nat_alt unat_sub unat_of_nat)
2354   done
2355qed
2356
2357lemma ccorres_abstract_ksCurThread:
2358  assumes ceqv: "\<And>rv' t t'. ceqv \<Gamma> (\<lambda>s. ksCurThread_' (globals s)) rv' t t' d (d' rv')"
2359  and       cc: "\<And>ct. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (G ct) (G' ct) hs a (d' (tcb_ptr_to_ctcb_ptr ct))"
2360  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s)
2361            {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} hs a d"
2362  apply (rule ccorres_guard_imp)
2363    prefer 2
2364    apply assumption
2365   apply (rule ccorres_abstract[OF ceqv, where G'="\<lambda>ct. \<lbrace>ct = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr ct)"])
2366   apply (subgoal_tac "\<exists>t. rv' = tcb_ptr_to_ctcb_ptr t")
2367    apply clarsimp
2368    apply (rule ccorres_guard_imp2)
2369     apply (rule cc)
2370    apply (clarsimp simp: rf_sr_ksCurThread)
2371   apply (metis tcb_ptr_to_tcb_ptr)
2372  apply simp
2373  done
2374
2375lemma ctcb_relation_unat_tcbPriority_C:
2376  "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority_C tcb') = unat (tcbPriority tcb)"
2377  apply (clarsimp simp: ctcb_relation_def)
2378  apply (rule trans, rule arg_cong[where f=unat], erule sym)
2379  apply (simp(no_asm))
2380  done
2381
2382lemma ctcb_relation_unat_tcbDomain_C:
2383  "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain_C tcb') = unat (tcbDomain tcb)"
2384  apply (clarsimp simp: ctcb_relation_def)
2385  apply (rule trans, rule arg_cong[where f=unat], erule sym)
2386  apply (simp(no_asm))
2387  done
2388
2389lemma getCurDomain_ccorres_dom_':
2390  "ccorres (\<lambda>rv rv'. rv' = ucast rv) dom_'
2391       \<top> UNIV hs curDomain (\<acute>dom :== \<acute>ksCurDomain)"
2392  apply (rule ccorres_from_vcg)
2393  apply (rule allI, rule conseqPre, vcg)
2394  apply (clarsimp simp: curDomain_def simpler_gets_def
2395                        rf_sr_ksCurDomain)
2396  done
2397
2398lemma rf_sr_cscheduler_action_relation:
2399  "(s, s') \<in> rf_sr
2400   \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))"
2401  by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
2402
2403lemma threadGet_get_obj_at'_has_domain:
2404  "\<lbrace> tcb_at' t \<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. rv = tcbDomain tcb) t\<rbrace>"
2405  by (wp threadGet_obj_at') (simp add: obj_at'_def)
2406
2407lemma possibleSwitchTo_ccorres:
2408  shows
2409  "ccorres dc xfdc
2410         (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
2411            and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain)
2412            and valid_objs')
2413         ({s. target_' s = tcb_ptr_to_ctcb_ptr t}
2414          \<inter> UNIV) []
2415     (possibleSwitchTo t )
2416     (Call possibleSwitchTo_'proc)"
2417  supply if_split [split del]
2418  supply Collect_const [simp del]
2419  supply dc_simp [simp del]
2420  supply prio_and_dom_limit_helpers[simp]
2421  (* FIXME: these should likely be in simpset for CRefine, or even in general *)
2422  supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp]
2423         ccorres_IF_True[simp]
2424  apply (cinit lift: target_')
2425   apply (rule ccorres_move_c_guard_tcb)
2426   apply (rule ccorres_pre_curDomain, rename_tac curDom)
2427   apply (rule ccorres_symb_exec_l3[OF _ threadGet_inv _ empty_fail_threadGet], rename_tac targetDom)
2428    apply (rule ccorres_symb_exec_l3[OF _ gsa_wp _ empty_fail_getSchedulerAction], rename_tac sact)
2429     apply (rule_tac C'="{s. targetDom \<noteq> curDom}"
2430              and Q="\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s"
2431              and Q'=UNIV in ccorres_rewrite_cond_sr)
2432      subgoal
2433        apply clarsimp
2434        apply (drule obj_at_ko_at', clarsimp  simp: rf_sr_ksCurDomain)
2435        apply (frule (1) obj_at_cslift_tcb, clarsimp simp: typ_heap_simps')
2436        apply (drule ctcb_relation_unat_tcbDomain_C)
2437        apply unat_arith
2438        done
2439     apply (rule ccorres_cond2[where R=\<top>], simp)
2440      apply (ctac add: tcbSchedEnqueue_ccorres)
2441     apply (rule_tac R="\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s"
2442                     in ccorres_cond)
2443       apply (fastforce dest!: rf_sr_cscheduler_action_relation pred_tcb_at' tcb_at_not_NULL
2444                        simp: cscheduler_action_relation_def max_word_def weak_sch_act_wf_def
2445                        split: scheduler_action.splits)
2446      apply (ctac add: rescheduleRequired_ccorres)
2447        apply (ctac add: tcbSchedEnqueue_ccorres)
2448       apply wp
2449      apply (vcg exspec=rescheduleRequired_modifies)
2450     apply (rule ccorres_setSchedulerAction, simp add: cscheduler_action_relation_def)
2451    apply clarsimp
2452    apply wp
2453   apply clarsimp
2454   apply (wp hoare_drop_imps threadGet_get_obj_at'_has_domain)
2455  apply (clarsimp simp: pred_tcb_at')
2456  done
2457
2458lemma scheduleTCB_ccorres':
2459  "ccorres dc xfdc
2460           (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_queues
2461                           and valid_objs')
2462           (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread})
2463           []
2464  (do (runnable, curThread, action) \<leftarrow> do
2465      runnable \<leftarrow> isRunnable thread;
2466      curThread \<leftarrow> getCurThread;
2467      action \<leftarrow> getSchedulerAction;
2468      return (runnable, curThread, action) od;
2469      when (\<not> runnable \<and>
2470              curThread = thread \<and> action = ResumeCurrentThread)
2471       rescheduleRequired
2472  od)
2473  (Call scheduleTCB_'proc)"
2474  apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
2475   apply (rule ccorres_rhs_assoc2)+
2476   apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
2477       defer
2478       apply ceqv
2479      apply (unfold split_def)[1]
2480      apply (rule ccorres_when[where R=\<top>])
2481       apply (intro allI impI)
2482       apply (unfold mem_simps)[1]
2483       apply assumption
2484      apply (ctac add: rescheduleRequired_ccorres)
2485     prefer 4
2486     apply (rule ccorres_symb_exec_l)
2487        apply (rule ccorres_pre_getCurThread)
2488        apply (rule ccorres_symb_exec_l)
2489           apply (rule_tac P="\<lambda>s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s
2490                                 \<and> curThread = ksCurThread s
2491                                 \<and> action = ksSchedulerAction s
2492                                 \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)"
2493                           and P'=UNIV in ccorres_from_vcg)
2494           apply (rule allI, rule conseqPre, vcg)
2495           apply (clarsimp simp: return_def if_1_0_0 split del: if_split)
2496           apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread)
2497           apply (rule conjI)
2498            apply (clarsimp simp: st_tcb_at'_def)
2499            apply (drule (1) obj_at_cslift_tcb)
2500            apply (clarsimp simp: typ_heap_simps)
2501            apply (subgoal_tac "ksSchedulerAction \<sigma> = ResumeCurrentThread")
2502             apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def)
2503             apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1]
2504            apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2505                                  cscheduler_action_relation_def max_word_def
2506                                  tcb_at_not_NULL
2507                           split: scheduler_action.split_asm)
2508           apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2509                                 cscheduler_action_relation_def)
2510          apply wp+
2511     apply (simp add: isRunnable_def isBlocked_def)
2512    apply wp
2513   apply (simp add: guard_is_UNIV_def)
2514  apply clarsimp
2515  apply (clarsimp simp: st_tcb_at'_def obj_at'_def weak_sch_act_wf_def)
2516  done
2517
2518lemma scheduleTCB_ccorres_valid_queues'_pre:
2519        "ccorresG rf_sr \<Gamma> dc xfdc (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs')
2520         (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) []
2521         (do (runnable, curThread, action) \<leftarrow> do
2522             runnable \<leftarrow> isRunnable thread;
2523             curThread \<leftarrow> getCurThread;
2524             action \<leftarrow> getSchedulerAction;
2525             return (runnable, curThread, action) od;
2526             when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
2527          od)
2528         (Call scheduleTCB_'proc)"
2529  apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
2530   apply (rule ccorres_rhs_assoc2)+
2531   apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
2532       defer
2533       apply ceqv
2534      apply (unfold split_def)[1]
2535      apply (rule ccorres_when[where R=\<top>])
2536       apply (intro allI impI)
2537       apply (unfold mem_simps)[1]
2538       apply assumption
2539      apply (ctac add: rescheduleRequired_ccorres)
2540     prefer 4
2541     apply (rule ccorres_symb_exec_l)
2542        apply (rule ccorres_pre_getCurThread)
2543        apply (rule ccorres_symb_exec_l)
2544           apply (rule_tac P="\<lambda>s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s
2545                                 \<and> curThread = ksCurThread s
2546                                 \<and> action = ksSchedulerAction s
2547                                 \<and> weak_sch_act_wf (ksSchedulerAction s) s"
2548                           and P'=UNIV in ccorres_from_vcg)
2549           apply (rule allI, rule conseqPre, vcg)
2550           apply (clarsimp simp: return_def if_1_0_0 split del: if_split)
2551           apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread)
2552           apply (rule conjI)
2553            apply (clarsimp simp: st_tcb_at'_def)
2554            apply (drule (1) obj_at_cslift_tcb)
2555            apply (clarsimp simp: typ_heap_simps)
2556            apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def weak_sch_act_wf_def)
2557             apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1]
2558                 apply (fold_subgoals (prefix))[6]
2559                 subgoal premises prems using prems
2560                         by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2561                                       cscheduler_action_relation_def max_word_def
2562                                       tcb_at_not_NULL[OF obj_tcb_at'] st_tcb_at'_def
2563                                split: scheduler_action.split_asm)+
2564           apply (clarsimp simp: rf_sr_def cstate_relation_def cscheduler_action_relation_def
2565                           split: scheduler_action.split_asm)
2566          apply wp+
2567     apply (simp add: isRunnable_def isBlocked_def)
2568    apply wp
2569   apply (simp add: guard_is_UNIV_def)
2570  apply (clarsimp simp: st_tcb_at'_def obj_at'_def)
2571  done
2572
2573
2574lemmas scheduleTCB_ccorres_valid_queues'
2575    = scheduleTCB_ccorres_valid_queues'_pre[unfolded bind_assoc return_bind split_conv]
2576
2577lemma rescheduleRequired_ccorres_valid_queues'_simple:
2578  "ccorresG rf_sr \<Gamma> dc xfdc (valid_queues' and sch_act_simple) UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)"
2579  apply cinit
2580   apply (rule ccorres_symb_exec_l)
2581      apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc])
2582          apply (simp add: scheduler_action_case_switch_to_if
2583                      cong: if_weak_cong split del: if_split)
2584          apply (rule_tac R="\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s"
2585                     in ccorres_cond)
2586            apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2587                                  cscheduler_action_relation_def)
2588            apply (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
2589                           split: scheduler_action.split_asm dest!: st_tcb_strg'[rule_format])
2590           apply (ctac add: tcbSchedEnqueue_ccorres)
2591          apply (rule ccorres_return_Skip)
2592         apply ceqv
2593        apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
2594        apply (rule allI, rule conseqPre, vcg)
2595        apply (clarsimp simp: setSchedulerAction_def simpler_modify_def)
2596        apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2597                              cscheduler_action_relation_def
2598                              carch_state_relation_def cmachine_state_relation_def
2599                              max_word_def)
2600       apply wp
2601      apply (simp add: guard_is_UNIV_def)
2602     apply wp+
2603   apply (simp add: getSchedulerAction_def)
2604  apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
2605                        Let_def cscheduler_action_relation_def)
2606  by (auto simp: tcb_at_not_NULL tcb_at_1
2607                    tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
2608                 split: scheduler_action.split_asm)
2609
2610lemma scheduleTCB_ccorres_valid_queues'_pre_simple:
2611        "ccorresG rf_sr \<Gamma> dc xfdc (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and sch_act_simple)
2612         (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) []
2613         (do (runnable, curThread, action) \<leftarrow> do
2614             runnable \<leftarrow> isRunnable thread;
2615             curThread \<leftarrow> getCurThread;
2616             action \<leftarrow> getSchedulerAction;
2617             return (runnable, curThread, action) od;
2618             when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
2619          od)
2620         (Call scheduleTCB_'proc)"
2621  apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
2622   apply (rule ccorres_rhs_assoc2)+
2623   apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
2624       defer
2625       apply ceqv
2626      apply (unfold split_def)[1]
2627      apply (rule ccorres_when[where R=\<top>])
2628       apply (intro allI impI)
2629       apply (unfold mem_simps)[1]
2630       apply assumption
2631      apply (ctac add: rescheduleRequired_ccorres_valid_queues'_simple)
2632     prefer 4
2633     apply (rule ccorres_symb_exec_l)
2634        apply (rule ccorres_pre_getCurThread)
2635        apply (rule ccorres_symb_exec_l)
2636           apply (rule_tac P="\<lambda>s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s
2637                                 \<and> curThread = ksCurThread s
2638                                 \<and> action = ksSchedulerAction s
2639                                 \<and> sch_act_simple s"
2640                           and P'=UNIV in ccorres_from_vcg)
2641           apply (rule allI, rule conseqPre, vcg)
2642           apply (clarsimp simp: return_def if_1_0_0 split del: if_split)
2643           apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread)
2644           apply (rule conjI)
2645            apply (clarsimp simp: st_tcb_at'_def)
2646            apply (drule (1) obj_at_cslift_tcb)
2647            apply (clarsimp simp: typ_heap_simps)
2648            apply (subgoal_tac "ksSchedulerAction \<sigma> = ResumeCurrentThread")
2649             apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def)
2650             apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1]
2651            apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2652                                  cscheduler_action_relation_def max_word_def
2653                                  tcb_at_not_NULL
2654                           split: scheduler_action.split_asm)
2655           apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
2656                                 cscheduler_action_relation_def)
2657          apply wp+
2658     apply (simp add: isRunnable_def isBlocked_def)
2659    apply wp
2660   apply (simp add: guard_is_UNIV_def)
2661  apply clarsimp
2662  apply (clarsimp simp: st_tcb_at'_def obj_at'_def valid_queues'_def)
2663  done
2664
2665lemmas scheduleTCB_ccorres_valid_queues'_simple
2666    = scheduleTCB_ccorres_valid_queues'_pre_simple[unfolded bind_assoc return_bind split_conv]
2667
2668lemmas scheduleTCB_ccorres[corres]
2669    = scheduleTCB_ccorres'[unfolded bind_assoc return_bind split_conv]
2670
2671lemma threadSet_weak_sch_act_wf_runnable':
2672            "\<lbrace> \<lambda>s. (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>
2673               threadSet (tcbState_update (\<lambda>_. st)) thread
2674             \<lbrace> \<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>"
2675  apply (simp add: weak_sch_act_wf_def)
2676  apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift threadSet_pred_tcb_at_state
2677            threadSet_tcbDomain_triv)
2678   apply simp
2679  apply (clarsimp)
2680done
2681
2682lemma threadSet_valid_queues_and_runnable': "\<lbrace>\<lambda>s. valid_queues s \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st)\<rbrace>
2683                 threadSet (tcbState_update (\<lambda>_. st)) thread
2684               \<lbrace>\<lambda>rv s. valid_queues s\<rbrace>"
2685  apply (wp threadSet_valid_queues)
2686  apply (clarsimp simp: inQ_def)
2687done
2688
2689lemma setThreadState_ccorres[corres]:
2690   "ccorres dc xfdc
2691   (\<lambda>s. tcb_at' thread s \<and> valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and>
2692                 (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and>
2693                 (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st) \<and>
2694                 sch_act_wf (ksSchedulerAction s) s)
2695     ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))}
2696    \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) hs
2697         (setThreadState st thread) (Call setThreadState_'proc)"
2698   apply (cinit lift: tptr_' cong add: call_ignore_cong)
2699   apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres)
2700    apply (ctac add: scheduleTCB_ccorres)
2701  apply (wp threadSet_weak_sch_act_wf_runnable' threadSet_valid_queues_and_runnable'
2702            threadSet_valid_objs')
2703  by (clarsimp simp: weak_sch_act_wf_def valid_queues_def valid_tcb'_tcbState_update)
2704
2705lemma threadSet_valid_queues'_and_not_runnable': "\<lbrace>tcb_at' thread and valid_queues' and (\<lambda>s. (\<not> runnable' st))\<rbrace>
2706                  threadSet (tcbState_update (\<lambda>_. st)) thread
2707               \<lbrace>\<lambda>rv. tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' \<rbrace>"
2708
2709  apply (wp threadSet_valid_queues' threadSet_tcbState_st_tcb_at')
2710  apply (clarsimp simp: pred_neg_def valid_queues'_def inQ_def)+
2711done
2712
2713lemma setThreadState_ccorres_valid_queues':
2714   "ccorres dc xfdc
2715   (\<lambda>s. tcb_at' thread s \<and> valid_queues' s \<and> \<not> runnable' st \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_tcb_state' st s)
2716     ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))}
2717    \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) []
2718         (setThreadState st thread) (Call setThreadState_'proc)"
2719   apply (cinit lift: tptr_' cong add: call_ignore_cong)
2720   apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres)
2721    apply (ctac add: scheduleTCB_ccorres_valid_queues')
2722   apply (wp threadSet_valid_queues'_and_not_runnable' threadSet_weak_sch_act_wf_runnable' threadSet_valid_queues_and_runnable' threadSet_valid_objs')
2723  by (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
2724
2725lemma simp_list_case_return:
2726  "(case x of [] \<Rightarrow> return e | y # ys \<Rightarrow> return f) = return (if x = [] then e else f)"
2727  by (clarsimp split: list.splits)
2728
2729lemma cancelSignal_ccorres [corres]:
2730     "ccorres dc xfdc
2731      (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread)
2732      (UNIV \<inter> {s. threadPtr_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. ntfnPtr_' s = Ptr ntfn})
2733      [] (cancelSignal thread ntfn) (Call cancelSignal_'proc)"
2734  apply (cinit lift: threadPtr_' ntfnPtr_' simp add: Let_def list_case_return cong add: call_ignore_cong)
2735   apply (unfold fun_app_def)
2736   apply (simp only: simp_list_case_return return_bind ccorres_seq_skip)
2737   apply (rule ccorres_pre_getNotification)
2738   apply (rule ccorres_assert)
2739   apply (rule ccorres_rhs_assoc2)
2740   apply (rule ccorres_rhs_assoc2)
2741   apply (rule ccorres_rhs_assoc2)
2742   apply (ctac (no_vcg) add: cancelSignal_ccorres_helper)
2743     apply (ctac add: setThreadState_ccorres_valid_queues')
2744    apply ((wp setNotification_nosch setNotification_ksQ hoare_vcg_all_lift set_ntfn_valid_objs' | simp add: valid_tcb_state'_def split del: if_split)+)[1]
2745   apply (simp add: "StrictC'_thread_state_defs")
2746  apply (rule conjI, clarsimp, rule conjI, clarsimp)
2747    apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs'])
2748   subgoal by ((auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def
2749                     isTS_defs cte_wp_at_ctes_of "StrictC'_thread_state_defs"
2750                     cthread_state_relation_def sch_act_wf_weak valid_ntfn'_def
2751             dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] |
2752           clarsimp simp: eq_commute)+)
2753   apply (clarsimp)
2754   apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs'])
2755   apply (frule (2) ntfn_blocked_in_queueD)
2756   by (auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def
2757                     isTS_defs cte_wp_at_ctes_of "StrictC'_thread_state_defs" valid_ntfn'_def
2758                     cthread_state_relation_def sch_act_wf_weak isWaitingNtfn_def
2759             dest!: valid_queues_not_runnable'_not_ksQ[where t=thread]
2760             split: ntfn.splits option.splits
2761         |  clarsimp simp: eq_commute
2762         | drule_tac x=thread in bspec)+
2763
2764lemma ko_at_valid_ep':
2765  "\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s"
2766  apply (erule obj_atE')
2767  apply (erule (1) valid_objsE')
2768   apply (simp add: projectKOs valid_obj'_def)
2769   done
2770
2771(* FIXME: MOVE *)
2772lemma ccorres_pre_getEndpoint [corres_pre]:
2773  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
2774  shows   "ccorres r xf
2775           (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s))
2776           ({s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (Ptr p))) \<longrightarrow> s' \<in> P' ep})
2777           hs (getEndpoint p >>= (\<lambda>rv. f rv)) c"
2778  apply (rule ccorres_guard_imp)
2779  apply (rule ccorres_symb_exec_l2)
2780      defer
2781      defer
2782      apply (rule get_ep_sp')
2783     apply assumption
2784    apply clarsimp
2785    prefer 3
2786    apply (clarsimp simp add: getEndpoint_def exs_getObject objBits_simps')
2787   defer
2788   apply (rule ccorres_guard_imp)
2789     apply (rule cc)
2790    apply simp
2791   apply assumption
2792  apply (drule spec, erule mp)
2793  apply (drule cmap_relation_ep)
2794  apply (drule (1) cmap_relation_ko_atD)
2795  apply clarsimp
2796  done
2797
2798lemma ep_blocked_in_queueD:
2799  "\<lbrakk> st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st)
2800                      \<and> blockingObject st = ep) thread \<sigma>;
2801               ko_at' ep' ep \<sigma>; invs' \<sigma> \<rbrakk>
2802   \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep')"
2803  apply (drule sym_refs_st_tcb_atD')
2804   apply clarsimp
2805  apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs)
2806  apply (clarsimp simp: isTS_defs split: Structures_H.thread_state.split_asm)
2807   apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1]
2808  apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1]
2809  done
2810
2811lemma ep_ptr_get_queue_spec:
2812  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> \<acute>ret__struct_tcb_queue_C :== PROC ep_ptr_get_queue(\<acute>epptr)
2813       \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = Ptr (epQueue_head_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr)))) \<and>
2814        end_C \<acute>ret__struct_tcb_queue_C = Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr))))\<rbrace>"
2815  apply vcg
2816  apply clarsimp
2817  done
2818
2819(* FIXME x64: bitfield shenanigans *)
2820lemma ep_ptr_set_queue_spec:
2821  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> Call ep_ptr_set_queue_'proc
2822           {t. (\<exists>ep'. endpoint_lift ep' =
2823  (endpoint_lift (the (cslift s (\<^bsup>s\<^esup>epptr))))\<lparr> epQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>queue) && ~~ mask 4,
2824                                                      epQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>queue) && ~~ mask 4 \<rparr>
2825             \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>epptr) ep')
2826                 (t_hrs_' (globals s)))}"
2827  apply vcg
2828  apply (auto simp: split_def h_t_valid_clift_Some_iff
2829                    typ_heap_simps packed_heap_update_collapse_hrs)
2830  oops
2831
2832lemma valid_ep_blockedD:
2833  "\<lbrakk> valid_ep' ep s; (isSendEP ep \<or> isRecvEP ep) \<rbrakk> \<Longrightarrow> (epQueue ep) \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s) \<and> distinct (epQueue ep)"
2834  unfolding valid_ep'_def isSendEP_def isRecvEP_def
2835  by (clarsimp split: endpoint.splits)
2836
2837
2838lemma ep_to_ep_queue:
2839  assumes ko: "ko_at' ep' ep s"
2840  and     waiting: "(isSendEP ep' \<or> isRecvEP ep')"
2841  and     rf: "(s, s') \<in> rf_sr"
2842  shows "ep_queue_relation' (cslift s') (epQueue ep')
2843              (Ptr (epQueue_head_CL
2844                     (endpoint_lift (the (cslift s' (Ptr ep))))))
2845              (Ptr (epQueue_tail_CL
2846                     (endpoint_lift (the (cslift s' (Ptr ep))))))"
2847proof -
2848  from rf have
2849    "cmap_relation (map_to_eps (ksPSpace s)) (cslift s') Ptr (cendpoint_relation (cslift s'))"
2850    by (rule cmap_relation_ep)
2851
2852  thus ?thesis using ko waiting
2853    apply -
2854    apply (erule (1) cmap_relation_ko_atE)
2855    apply (clarsimp simp: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits)
2856    done
2857qed
2858
2859lemma ep_ep_disjoint:
2860  assumes srs: "sym_refs (state_refs_of' s)"
2861  and    epat: "ko_at' ep epptr s"
2862  and   epat': "ko_at' ep' epptr' s"
2863  and     epq: "(isSendEP ep \<or> isRecvEP ep)"
2864  and    epq': "(isSendEP ep' \<or> isRecvEP ep')"
2865  and      neq: "epptr' \<noteq> epptr"
2866  shows  "set (epQueue ep) \<inter> set (epQueue ep') = {}"
2867  using srs epat epat' epq epq' neq
2868  apply -
2869  apply (subst disjoint_iff_not_equal, intro ballI, rule notI)
2870  apply (drule sym_refs_ko_atD', clarsimp)+
2871  apply clarsimp
2872  apply (clarsimp simp: isSendEP_def isRecvEP_def split: endpoint.splits)
2873  apply (simp_all add: st_tcb_at_refs_of_rev')
2874  apply (fastforce simp: st_tcb_at'_def obj_at'_def)+
2875  done
2876
2877lemma cendpoint_relation_ep_queue:
2878  fixes ep :: "endpoint"
2879  assumes   ep: "cendpoint_relation mp ep' b"
2880  and     mpeq: "(mp' |` (- S)) = (mp |` (- S))"
2881  and      epq: "ep' \<noteq> IdleEP \<Longrightarrow>
2882                     set (epQueue ep') \<inter> (ctcb_ptr_to_tcb_ptr ` S) = {}"
2883  shows  "cendpoint_relation mp' ep' b"
2884proof -
2885
2886  have rl: "\<And>p list. \<lbrakk> ctcb_ptr_to_tcb_ptr p \<in> set list;
2887                          ep' = RecvEP list \<or> ep' = SendEP list \<rbrakk>
2888                         \<Longrightarrow> mp' p = mp p"
2889    using epq
2890    apply (cut_tac x=p in fun_cong[OF mpeq])
2891    apply (cases ep', auto simp: restrict_map_def split: if_split_asm)
2892    done
2893
2894  have rl': "\<And>p list. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set list;
2895                          ep' = RecvEP list \<or> ep' = SendEP list \<rbrakk>
2896                         \<Longrightarrow> mp' p = mp p"
2897    by (clarsimp elim!: rl[rotated])
2898
2899  show ?thesis using ep rl' mpeq unfolding cendpoint_relation_def
2900    by (simp add: Let_def
2901            cong: Structures_H.endpoint.case_cong tcb_queue_relation'_cong)
2902qed
2903
2904lemma cpspace_relation_ep_update_an_ep:
2905  fixes ep :: "endpoint"
2906  defines "qs \<equiv> if (isSendEP ep \<or> isRecvEP ep) then set (epQueue ep) else {}"
2907  assumes koat: "ko_at' ep epptr s"
2908  and      cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
2909  and     rel: "cendpoint_relation mp' ep' endpoint"
2910  and    mpeq: "(mp' |` (- S)) = (mp |` (- S))"
2911  and     pal: "pspace_aligned' s" "pspace_distinct' s"
2912  and  others: "\<And>epptr' ep'. \<lbrakk> ko_at' ep' epptr' s; epptr' \<noteq> epptr; ep' \<noteq> IdleEP \<rbrakk>
2913                                 \<Longrightarrow> set (epQueue ep') \<inter> (ctcb_ptr_to_tcb_ptr ` S) = {}"
2914  shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep')))
2915           (cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
2916  using cp koat pal rel unfolding cmap_relation_def
2917  apply -
2918  apply (clarsimp elim!: obj_atE' simp: map_comp_update projectKO_opts_defs)
2919  apply (drule (1) bspec [OF _ domI])
2920  apply simp
2921  apply (erule cendpoint_relation_ep_queue[OF _ mpeq])
2922  apply (erule(4) others[OF map_to_ko_atI])
2923  done
2924
2925lemma endpoint_not_idle_cases:
2926  "ep \<noteq> IdleEP \<Longrightarrow> isSendEP ep \<or> isRecvEP ep"
2927  by (clarsimp simp: isRecvEP_def isSendEP_def split: Structures_H.endpoint.split)
2928
2929lemma cpspace_relation_ep_update_ep:
2930  fixes ep :: "endpoint"
2931  defines "qs \<equiv> if (isSendEP ep \<or> isRecvEP ep) then set (epQueue ep) else {}"
2932  assumes koat: "ko_at' ep epptr s"
2933  and     invs: "invs' s"
2934  and      cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
2935  and     rel: "cendpoint_relation mp' ep' endpoint"
2936  and    mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
2937  shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep')))
2938           (cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
2939  using invs
2940  apply (intro cpspace_relation_ep_update_an_ep[OF koat cp rel mpeq])
2941    apply clarsimp+
2942  apply (clarsimp simp add: qs_def image_image simp del: imp_disjL)
2943  apply (rule ep_ep_disjoint[OF _ _ koat endpoint_not_idle_cases], auto)
2944  done
2945
2946lemma cpspace_relation_ep_update_ep':
2947  fixes ep :: "endpoint" and ep' :: "endpoint"
2948    and epptr :: "machine_word" and s :: "kernel_state"
2949  defines "qs \<equiv> if (isSendEP ep' \<or> isRecvEP ep') then set (epQueue ep') else {}"
2950  defines "s' \<equiv> s\<lparr>ksPSpace := ksPSpace s(epptr \<mapsto> KOEndpoint ep')\<rparr>"
2951  assumes koat: "ko_at' ep epptr s"
2952  and       vp: "valid_pspace' s"
2953  and      cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
2954  and      srs: "sym_refs (state_refs_of' s')"
2955  and     rel: "cendpoint_relation mp' ep' endpoint"
2956  and    mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
2957  shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep')))
2958           (cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
2959proof -
2960  from koat have koat': "ko_at' ep' epptr s'"
2961    by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs)
2962
2963  from koat have koat'': "\<And>ep'' epptr'. \<lbrakk> ko_at' ep'' epptr' s; epptr' \<noteq> epptr \<rbrakk>
2964              \<Longrightarrow> ko_at' ep'' epptr' s'"
2965    by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs)
2966
2967  show ?thesis using vp ep_ep_disjoint[OF srs koat'' koat' endpoint_not_idle_cases]
2968  apply (intro cpspace_relation_ep_update_an_ep[OF koat cp rel mpeq])
2969    apply clarsimp+
2970  apply (clarsimp simp add: qs_def image_image simp del: imp_disjL)
2971  done
2972qed
2973
2974lemma cnotification_relation_ep_queue:
2975  assumes   srs: "sym_refs (state_refs_of' s)"
2976  and      koat: "ko_at' ep epptr s"
2977  and iswaiting: "(isSendEP ep \<or> isRecvEP ep)"
2978  and      mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` set (epQueue ep))))
2979  = (mp |` (- (tcb_ptr_to_ctcb_ptr ` set (epQueue ep))))"
2980  and      koat': "ko_at' a ntfnPtr s"
2981  shows "cnotification_relation mp a b = cnotification_relation mp' a b"
2982proof -
2983  have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a));
2984                  isWaitingNtfn (ntfnObj a) \<rbrakk>
2985    \<Longrightarrow> mp p = mp' p" using srs koat' koat iswaiting mpeq
2986    apply -
2987    apply (drule (4) ntfn_ep_disjoint)
2988    apply (erule restrict_map_eqI [symmetric])
2989    apply (erule imageE)
2990    apply (fastforce simp: disjoint_iff_not_equal inj_eq)
2991    done
2992
2993  show ?thesis
2994    unfolding cnotification_relation_def using rl
2995    apply (simp add: Let_def)
2996    apply (cases "ntfnObj a")
2997       apply (simp add: isWaitingNtfn_def cong: tcb_queue_relation'_cong)+
2998    done
2999qed
3000
3001(* FIXME: x64 can be removed? *)
3002lemma epQueue_head_mask_2 [simp]:
3003  "epQueue_head_CL (endpoint_lift ko') && ~~ mask 2 = epQueue_head_CL (endpoint_lift ko')"
3004  unfolding endpoint_lift_def
3005  oops (*by (clarsimp simp: mask_def word_bw_assocs) *)
3006
3007lemma epQueue_tail_mask_2 [simp]:
3008  "epQueue_tail_CL (endpoint_lift ko') && ~~ mask 2 = epQueue_tail_CL (endpoint_lift ko')"
3009  unfolding endpoint_lift_def
3010  by (clarsimp simp: mask_def word_bw_assocs sign_extend_def) word_bitwise
3011
3012lemma epQueue_tail_sign[simp]:
3013  "sign_extend 47 (epQueue_tail_CL (endpoint_lift ko)) = epQueue_tail_CL (endpoint_lift ko)"
3014  by (simp add: endpoint_lift_def sign_extend_sign_extend_eq)
3015
3016(* Clag from cancelSignal_ccorres_helper *)
3017
3018lemma cancelIPC_ccorres_helper:
3019  "ccorres dc xfdc (invs' and
3020         st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st)
3021                            \<and> blockingObject st = ep) thread
3022        and ko_at' ep' ep)
3023        {s. epptr_' s = Ptr ep}
3024        []
3025        (setEndpoint ep (if remove1 thread (epQueue ep') = [] then Structures_H.endpoint.IdleEP
3026                         else epQueue_update (\<lambda>_. remove1 thread (epQueue ep')) ep'))
3027        (\<acute>queue :== CALL ep_ptr_get_queue(\<acute>epptr);;
3028         \<acute>queue :== CALL tcbEPDequeue(tcb_ptr_to_ctcb_ptr thread,\<acute>queue);;
3029          CALL ep_ptr_set_queue(\<acute>epptr,\<acute>queue);;
3030          IF head_C \<acute>queue = NULL THEN
3031              CALL endpoint_ptr_set_state(\<acute>epptr,scast EPState_Idle)
3032          FI)"
3033  apply (rule ccorres_from_vcg)
3034  apply (rule allI)
3035  apply (rule conseqPre)
3036   apply vcg
3037  apply (clarsimp split del: if_split simp del: comp_def)
3038  apply (frule (2) ep_blocked_in_queueD)
3039  apply (frule (1) ko_at_valid_ep' [OF _ invs_valid_objs'])
3040  apply (elim conjE)
3041  apply (frule (1) valid_ep_blockedD)
3042  apply (elim conjE)
3043  apply (frule cmap_relation_ep)
3044  apply (erule (1) cmap_relation_ko_atE)
3045  apply (intro conjI)
3046   apply (erule h_t_valid_clift)
3047  apply (rule impI)
3048  apply (rule exI)
3049  apply (rule conjI)
3050   apply (rule_tac x = \<sigma> in exI)
3051   apply (intro conjI)
3052       apply assumption+
3053   apply (drule (2) ep_to_ep_queue)
3054   apply (simp add: tcb_queue_relation'_def)
3055  apply (clarsimp simp: typ_heap_simps cong: imp_cong split del: if_split simp del: comp_def)
3056  apply (frule null_ep_queue [simplified comp_def] null_ep_queue)
3057  apply (intro impI conjI allI)
3058   \<comment> \<open>empty case\<close>
3059   apply clarsimp
3060   apply (frule iffD1 [OF tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel]])
3061     apply (rule ballI, erule bspec)
3062     apply (erule subsetD [rotated])
3063     apply clarsimp
3064    subgoal by simp
3065   apply (simp add: setEndpoint_def split_def)
3066   apply (rule bexI [OF _ setObject_eq])
3067       apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
3068                        cpspace_relation_def update_ep_map_tos typ_heap_simps')
3069       apply (elim conjE)
3070       apply (intro conjI)
3071       \<comment> \<open>tcb relation\<close>
3072            apply (erule ctcb_relation_null_queue_ptrs)
3073            subgoal by (clarsimp simp: comp_def)
3074        \<comment> \<open>ep relation\<close>
3075           apply (rule cpspace_relation_ep_update_ep, assumption+)
3076            subgoal by (simp add: cendpoint_relation_def Let_def EPState_Idle_def)
3077           subgoal by simp
3078           \<comment> \<open>ntfn relation\<close>
3079          apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
3080          apply simp
3081          apply (rule cnotification_relation_ep_queue [OF invs_sym'], assumption+)
3082           subgoal by simp
3083          apply (erule (1) map_to_ko_atI')
3084         apply (simp add: heap_to_user_data_def Let_def)
3085        \<comment> \<open>queue relation\<close>
3086         apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
3087         subgoal by (clarsimp simp: comp_def)
3088        subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def
3089                                   fpu_null_state_heap_update_tag_disj_simps
3090                                   global_ioport_bitmap_heap_update_tag_disj_simps
3091                                   packed_heap_update_collapse_hrs
3092                            elim!: fpu_null_state_typ_heap_preservation)
3093       subgoal by (simp add: cmachine_state_relation_def)
3094      subgoal by (simp add: h_t_valid_clift_Some_iff)
3095     subgoal by (simp add: objBits_simps')
3096    subgoal by (simp add: objBits_simps)
3097   apply assumption
3098  \<comment> \<open>non empty case\<close>
3099  apply clarsimp
3100  apply (frule tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel])
3101   apply (rule ballI, erule bspec)
3102   apply (erule subsetD [rotated])
3103   apply clarsimp
3104  apply (simp add: setEndpoint_def split_def)
3105  apply (rule bexI [OF _ setObject_eq])
3106      apply (frule (1) st_tcb_at_h_t_valid)
3107      apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
3108                       cpspace_relation_def update_ep_map_tos typ_heap_simps')
3109      apply (elim conjE)
3110      apply (intro conjI)
3111      \<comment> \<open>tcb relation\<close>
3112           apply (erule ctcb_relation_null_queue_ptrs)
3113           subgoal by (clarsimp simp: comp_def)
3114       \<comment> \<open>ep relation\<close>
3115          apply (rule cpspace_relation_ep_update_ep, assumption+)
3116           apply (simp add: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits split del: if_split)
3117           \<comment> \<open>recv case\<close>
3118            apply (subgoal_tac "pspace_canonical' \<sigma>")
3119             prefer 2
3120             apply fastforce
3121            apply (clarsimp simp add:  h_t_valid_clift_Some_iff ctcb_offset_defs
3122              tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
3123              tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign
3124              cong: tcb_queue_relation'_cong)
3125            subgoal by (intro impI conjI; simp)
3126           \<comment> \<open>send case\<close>
3127            apply (subgoal_tac "pspace_canonical' \<sigma>")
3128             prefer 2
3129             apply fastforce
3130           apply (clarsimp simp add: h_t_valid_clift_Some_iff ctcb_offset_defs
3131             tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask
3132             tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign
3133             cong: tcb_queue_relation'_cong)
3134           subgoal by (intro impI conjI; simp)
3135          subgoal by simp
3136                \<comment> \<open>ntfn relation\<close>
3137         apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
3138         apply simp
3139         apply (rule cnotification_relation_ep_queue [OF invs_sym'], assumption+)
3140         apply simp
3141         apply (erule (1) map_to_ko_atI')
3142         \<comment> \<open>queue relation\<close>
3143        apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
3144        subgoal by (clarsimp simp: comp_def)
3145       subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def
3146                                  fpu_null_state_heap_update_tag_disj_simps
3147                                  global_ioport_bitmap_heap_update_tag_disj_simps
3148                                  packed_heap_update_collapse_hrs
3149                           elim!: fpu_null_state_typ_heap_preservation)
3150      subgoal by (simp add: cmachine_state_relation_def)
3151     subgoal by (simp add: h_t_valid_clift_Some_iff)
3152    subgoal by (simp add: objBits_simps')
3153   subgoal by (simp add: objBits_simps)
3154  by assumption
3155
3156declare empty_fail_get[iff]
3157
3158lemma getThreadState_ccorres_foo:
3159  "(\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
3160    ccorres r xf (\<lambda>s. \<forall>ts. st_tcb_at' ((=) ts) t s \<longrightarrow> P ts s)
3161                 {s. \<forall>ts tcb'. cslift s (tcb_ptr_to_ctcb_ptr t) = Some tcb'
3162                              \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb')
3163                            \<longrightarrow> s \<in> P' ts} hs
3164        (getThreadState t >>= f) c"
3165  apply (rule ccorres_symb_exec_l' [OF _ gts_inv' gts_sp' empty_fail_getThreadState])
3166  apply (erule_tac x=rv in meta_allE)
3167  apply (erule ccorres_guard_imp2)
3168  apply (clarsimp simp: st_tcb_at'_def)
3169  apply (drule obj_at_ko_at', clarsimp)
3170  apply (erule cmap_relationE1 [OF cmap_relation_tcb])
3171   apply (erule ko_at_projectKO_opt)
3172  apply (clarsimp simp: ctcb_relation_def obj_at'_def)
3173  done
3174
3175lemma ep_blocked_in_queueD_recv:
3176  "\<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isRecvEP ep'"
3177  apply (frule sym_refs_st_tcb_atD', clarsimp)
3178  apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs)
3179  apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1]
3180  done
3181
3182lemma ep_blocked_in_queueD_send:
3183  "\<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x xa xb xc)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isSendEP ep'"
3184  apply (frule sym_refs_st_tcb_atD', clarsimp)
3185  apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs)
3186  apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1]
3187  done
3188
3189lemma cancelIPC_ccorres1:
3190  assumes cteDeleteOne_ccorres:
3191  "\<And>w slot. ccorres dc xfdc
3192   (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap
3193        \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)
3194   ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w}
3195        \<inter> {s. slot_' s = Ptr slot}) []
3196   (cteDeleteOne slot) (Call cteDeleteOne_'proc)"
3197  shows
3198  "ccorres dc xfdc (tcb_at' thread and invs')
3199                   (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) []
3200          (cancelIPC thread) (Call cancelIPC_'proc)"
3201  apply (cinit lift: tptr_' simp: Let_def cong: call_ignore_cong)
3202   apply (rule ccorres_move_c_guard_tcb)
3203   apply csymbr
3204   apply (rule getThreadState_ccorres_foo)
3205   apply (rule ccorres_symb_exec_r)
3206     apply (rule_tac xf'=ret__unsigned_longlong_' in ccorres_abstract, ceqv)
3207     apply (rule_tac P="rv' = thread_state_to_tsType rv" in ccorres_gen_asm2)
3208     apply wpc
3209            \<comment> \<open>BlockedOnReceive\<close>
3210            apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs cong: call_ignore_cong)
3211            apply (fold dc_def)
3212            apply (rule ccorres_rhs_assoc)+
3213            apply csymbr
3214            apply csymbr
3215            apply (rule ccorres_pre_getEndpoint)
3216            apply (rule ccorres_assert)
3217            apply (rule ccorres_symb_exec_r) \<comment> \<open>ptr_get lemmas don't work so well :(\<close>
3218              apply (rule ccorres_symb_exec_r)
3219                apply (simp only: fun_app_def simp_list_case_return
3220                                  return_bind ccorres_seq_skip)
3221                apply (rule ccorres_rhs_assoc2)
3222                apply (rule ccorres_rhs_assoc2)
3223                apply (rule ccorres_rhs_assoc2)
3224                apply (ctac (no_vcg) add: cancelIPC_ccorres_helper)
3225                  apply (ctac add: setThreadState_ccorres_valid_queues')
3226                 apply (wp hoare_vcg_all_lift set_ep_valid_objs' | simp add: valid_tcb_state'_def split del: if_split)+
3227                apply (simp add: "StrictC'_thread_state_defs")
3228               apply vcg
3229              apply (rule conseqPre, vcg)
3230              apply clarsimp
3231             apply clarsimp
3232             apply (rule conseqPre, vcg)
3233             apply (rule subset_refl)
3234            apply (rule conseqPre, vcg)
3235            apply clarsimp
3236          \<comment> \<open>BlockedOnReply case\<close>
3237           apply (simp add: "StrictC'_thread_state_defs" ccorres_cond_iffs
3238                            Collect_False Collect_True word_sle_def
3239                      cong: call_ignore_cong del: Collect_const)
3240           apply (fold dc_def)
3241           apply (rule ccorres_rhs_assoc)+
3242           apply csymbr
3243           apply csymbr
3244           apply (unfold comp_def)[1]
3245           apply csymbr
3246           apply (rule ccorres_move_c_guard_tcb)+
3247           apply (rule ccorres_split_nothrow_novcg)
3248               apply (rule_tac P=\<top> in threadSet_ccorres_lemma2)
3249                apply vcg
3250               apply (clarsimp simp: typ_heap_simps')
3251               apply (erule(1) rf_sr_tcb_update_no_queue2,
3252                 (simp add: typ_heap_simps')+)[1]
3253                apply (rule ball_tcb_cte_casesI, simp_all)[1]
3254               apply (clarsimp simp: ctcb_relation_def seL4_Fault_lift_NullFault
3255                                     cfault_rel_def cthread_state_relation_def)
3256               apply (case_tac "tcbState tcb", simp_all add: is_cap_fault_def)[1]
3257              apply ceqv
3258             apply ccorres_remove_UNIV_guard
3259             apply (rule ccorres_move_array_assertion_tcb_ctes)
3260             apply (rule_tac P="tcb_at' thread" in ccorres_cross_over_guard)
3261             apply (simp add: getThreadReplySlot_def)
3262             apply ctac
3263               apply (simp only: liftM_def bind_assoc return_bind del: Collect_const)
3264               apply (rule ccorres_pre_getCTE)
3265               apply (rename_tac slot slot' cte)
3266               apply (rule ccorres_move_c_guard_cte)
3267               apply (rule_tac xf'=ret__unsigned_longlong_' and val="mdbNext (cteMDBNode cte)"
3268                         and R="cte_wp_at' ((=) cte) slot and invs'"
3269                          in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
3270                  apply vcg
3271                  apply (clarsimp simp: cte_wp_at_ctes_of)
3272                  apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
3273                  apply (clarsimp simp: typ_heap_simps)
3274                  apply (clarsimp simp: ccte_relation_def map_option_Some_eq2)
3275                 apply ceqv
3276                apply csymbr
3277                apply (rule ccorres_Cond_rhs)
3278                 apply (simp add: nullPointer_def when_def)
3279                 apply (rule ccorres_symb_exec_l[OF _ _ _ empty_fail_stateAssert])
3280                   apply (simp only: dc_def[symmetric])
3281                   apply (rule ccorres_symb_exec_r)
3282                     apply (ctac add: cteDeleteOne_ccorres[where w1="scast cap_reply_cap"])
3283                    apply vcg
3284                   apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def
3285                       gs_set_assn_Delete_cstate_relation[unfolded o_def])
3286                  apply (wp | simp)+
3287                apply (simp add: when_def nullPointer_def dc_def[symmetric])
3288                apply (rule ccorres_return_Skip)
3289               apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
3290                                ghost_assertion_data_set_def cap_tag_defs)
3291              apply (simp add: locateSlot_conv, wp)
3292             apply vcg
3293            apply (rule_tac Q="\<lambda>rv. tcb_at' thread and invs'" in hoare_post_imp)
3294             apply (clarsimp simp: cte_wp_at_ctes_of capHasProperty_def
3295                                   cap_get_tag_isCap ucast_id)
3296            apply (wp threadSet_invs_trivial | simp)+
3297           apply (clarsimp simp add: guard_is_UNIV_def tcbReplySlot_def
3298                        Kernel_C.tcbReply_def tcbCNodeEntries_def)
3299          \<comment> \<open>BlockedOnNotification\<close>
3300          apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong)
3301          apply (rule ccorres_symb_exec_r)
3302            apply (ctac (no_vcg))
3303           apply clarsimp
3304           apply (rule conseqPre, vcg)
3305           apply (rule subset_refl)
3306          apply (rule conseqPre, vcg)
3307          apply clarsimp
3308         \<comment> \<open>Running, Inactive, and Idle\<close>
3309         apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong,
3310                rule ccorres_return_Skip)+
3311      \<comment> \<open>BlockedOnSend\<close>
3312      apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong)
3313      \<comment> \<open>clag\<close>
3314      apply (rule ccorres_rhs_assoc)+
3315      apply csymbr
3316      apply csymbr
3317      apply (rule ccorres_pre_getEndpoint)
3318      apply (rule ccorres_assert)
3319      apply (rule ccorres_symb_exec_r) \<comment> \<open>ptr_get lemmas don't work so well :(\<close>
3320        apply (rule ccorres_symb_exec_r)
3321          apply (simp only: fun_app_def simp_list_case_return return_bind ccorres_seq_skip)
3322          apply (rule ccorres_rhs_assoc2)
3323          apply (rule ccorres_rhs_assoc2)
3324          apply (rule ccorres_rhs_assoc2)
3325          apply (ctac (no_vcg) add: cancelIPC_ccorres_helper)
3326            apply (ctac add: setThreadState_ccorres_valid_queues')
3327           apply (wp hoare_vcg_all_lift set_ep_valid_objs' | simp add: valid_tcb_state'_def split del:if_split)+
3328       apply (simp add: "StrictC'_thread_state_defs")
3329         apply clarsimp
3330         apply (rule conseqPre, vcg, rule subset_refl)
3331        apply (rule conseqPre, vcg)
3332        apply clarsimp
3333       apply clarsimp
3334       apply (rule conseqPre, vcg, rule subset_refl)
3335      apply (rule conseqPre, vcg)
3336      apply clarsimp
3337  \<comment> \<open>Restart\<close>
3338     apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong,
3339            rule ccorres_return_Skip)
3340    \<comment> \<open>Post wp proofs\<close>
3341    apply vcg
3342   apply clarsimp
3343   apply (rule conseqPre, vcg)
3344   apply clarsimp
3345  apply clarsimp
3346  apply (drule(1) obj_at_cslift_tcb)
3347  apply clarsimp
3348  apply (frule obj_at_valid_objs', clarsimp+)
3349  apply (clarsimp simp: projectKOs valid_obj'_def valid_tcb'_def
3350                        valid_tcb_state'_def typ_heap_simps
3351                        word_sle_def)
3352  apply (rule conjI, clarsimp)
3353   apply (rule conjI, clarsimp)
3354    apply (rule conjI)
3355     subgoal by (auto simp: projectKOs obj_at'_def pred_tcb_at'_def split: thread_state.splits)[1]
3356    apply (clarsimp)
3357    apply (rule conjI)
3358     subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def
3359                     isTS_defs cte_wp_at_ctes_of
3360                     cthread_state_relation_def sch_act_wf_weak valid_ep'_def
3361             dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits)
3362    apply clarsimp
3363    apply (frule (2) ep_blocked_in_queueD_recv)
3364    apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs'])
3365    subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def
3366                         isTS_defs cte_wp_at_ctes_of isRecvEP_def
3367                         cthread_state_relation_def sch_act_wf_weak valid_ep'_def
3368                 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits endpoint.splits)
3369   apply (rule conjI)
3370    apply (clarsimp simp: inQ_def)
3371   apply (rule conjI)
3372    apply clarsimp
3373   apply clarsimp
3374   apply (rule conjI)
3375    subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def
3376                         isTS_defs cte_wp_at_ctes_of
3377                         cthread_state_relation_def sch_act_wf_weak valid_ep'_def
3378                 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits)
3379   apply clarsimp
3380   apply (rule conjI)
3381    subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def
3382                         isTS_defs cte_wp_at_ctes_of
3383                         cthread_state_relation_def sch_act_wf_weak valid_ep'_def
3384                 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits)
3385   apply clarsimp
3386   apply (frule (2) ep_blocked_in_queueD_send)
3387   apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs'])
3388   subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def
3389                        isTS_defs cte_wp_at_ctes_of isSendEP_def
3390                        cthread_state_relation_def sch_act_wf_weak valid_ep'_def
3391                dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits endpoint.splits)[1]
3392  apply (auto simp: isTS_defs cthread_state_relation_def typ_heap_simps weak_sch_act_wf_def)
3393  apply (case_tac ts,
3394           auto simp: isTS_defs cthread_state_relation_def typ_heap_simps)
3395  done
3396
3397end
3398end
3399