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 Schedule_R
12imports VSpace_R
13begin
14
15context begin interpretation Arch . (*FIXME: arch_split*)
16
17declare static_imp_wp[wp_split del]
18
19(* FIXME: move *)
20lemma corres_if_r':
21  "\<lbrakk> G' \<Longrightarrow> corres_underlying sr nf nf' r P P' a c; \<not>G' \<Longrightarrow> corres_underlying sr nf nf' r P Q' a d \<rbrakk>
22   \<Longrightarrow> corres_underlying sr nf nf' r (P) (if G' then P' else Q')
23                                     (a) (if G' then c  else d)"
24  by (simp)
25
26(* FIXME: move *)
27lemma corres_gets_pre_lhs:
28  "(\<And>x. corres r (P x) P' (g x) g') \<Longrightarrow>
29  corres r (\<lambda>s. P (f s) s) P' (gets f >>= (\<lambda>x. g x)) g'"
30  by (rule corres_underlying_gets_pre_lhs)
31
32(* FIXME: move *)
33lemma corres_if_lhs:
34  assumes "P \<Longrightarrow> corres r A Q f f'"
35  assumes "\<not>P \<Longrightarrow> corres r B Q g f'"
36  shows "corres r (\<lambda>s. (P \<longrightarrow> A s) \<and> (\<not>P \<longrightarrow> B s)) Q (if P then f else g) f'"
37  by (simp add: assms)
38
39(* Levity: added (20090713 10:04:12) *)
40declare sts_rel_idle [simp]
41
42(* FIXME: move to NonDetMonadVCG *)
43lemma return_wp_exs_valid [wp]: "\<lbrace> P x \<rbrace> return x \<exists>\<lbrace> P \<rbrace>"
44  by (simp add: exs_valid_def return_def)
45
46(* FIXME: move to NonDetMonadVCG *)
47lemma get_exs_valid [wp]: "\<lbrace>(=) s\<rbrace> get \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
48  by (simp add: get_def exs_valid_def)
49
50lemma invs_no_cicd'_queues:
51  "invs_no_cicd' s \<Longrightarrow> valid_queues s"
52  unfolding invs_no_cicd'_def
53  by simp
54
55lemma gsa_wf [wp]: "\<lbrace>invs'\<rbrace> getSchedulerAction \<lbrace>sch_act_wf\<rbrace>"
56  by (simp add: getSchedulerAction_def invs'_def valid_state'_def | wp)+
57
58lemma corres_if2:
59 "\<lbrakk> G = G'; G \<Longrightarrow> corres r P P' a c; \<not> G' \<Longrightarrow> corres r Q Q' b d \<rbrakk>
60    \<Longrightarrow> corres r (if G then P else Q) (if G' then P' else Q') (if G then a else b) (if G' then c else d)"
61  by simp
62
63lemma findM_awesome':
64  assumes x: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow>
65                  corres (\<lambda>a b. if b then (\<exists>a'. a = Some a' \<and> r a' (Some x)) else a = None)
66                      P (P' (x # xs))
67                      ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)"
68  assumes y: "corres r P (P' []) f (return None)"
69  assumes z: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow>
70                 \<lbrace>P' (x # xs)\<rbrace> g x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P' xs s\<rbrace>"
71  assumes p: "suffix xs xs'"
72  shows      "corres r P (P' xs) f (findM g xs)"
73proof -
74  have P: "f = do x \<leftarrow> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None; if x \<noteq> None then return (the x) else f od"
75    apply (rule ext)
76    apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff)
77    done
78  have Q: "\<lbrace>P\<rbrace> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None \<lbrace>\<lambda>rv. if rv \<noteq> None then \<top> else P\<rbrace>"
79    by (wp alternative_wp | simp)+
80  show ?thesis using p
81    apply (induct xs)
82     apply (simp add: y del: dc_simp)
83    apply (simp only: findM.simps)
84    apply (subst P)
85    apply (rule corres_guard_imp)
86      apply (rule corres_split [OF _ x])
87         apply (rule corres_if2)
88           apply (case_tac ra, clarsimp+)[1]
89          apply (rule corres_trivial, clarsimp)
90          apply (case_tac ra, simp_all)[1]
91         apply (erule(1) meta_mp [OF _ suffix_ConsD])
92        apply assumption
93       apply (rule Q)
94      apply (rule hoare_post_imp [OF _ z])
95      apply simp+
96    done
97qed
98
99lemmas findM_awesome = findM_awesome' [OF _ _ _ suffix_order.order.refl]
100
101lemma corres_rhs_disj_division:
102  "\<lbrakk> P \<or> Q; P \<Longrightarrow> corres r R S x y; Q \<Longrightarrow> corres r T U x y \<rbrakk>
103     \<Longrightarrow> corres r (R and T) (\<lambda>s. (P \<longrightarrow> S s) \<and> (Q \<longrightarrow> U s)) x y"
104  apply (rule corres_guard_imp)
105    apply (erule corres_disj_division)
106     apply simp+
107  done
108
109lemma findM_alternative_awesome:
110  assumes x: "\<And>x. corres (\<lambda>a b. if b then (\<exists>a'. a = Some a') else a = None)
111                      P (P' and (\<lambda>s. x \<in> fn s)) ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)"
112  assumes z: "\<And>x xs. \<lbrace>\<lambda>s. P' s \<and> x \<in> fn s \<and> set xs \<subseteq> fn s\<rbrace> g x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P' s \<and> set xs \<subseteq> fn s\<rbrace>"
113  assumes on_none: "corres dc P P' f g'"
114  shows      "corres dc P (P' and (\<lambda>s. set xs \<subseteq> fn s)) f (findM g xs >>= (\<lambda>x. when (x = None) g'))"
115proof -
116  have P: "f = do x \<leftarrow> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None; if x \<noteq> None then return (the x) else f od"
117    apply (rule ext)
118    apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff)
119    done
120  have Q: "\<lbrace>P\<rbrace> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None \<lbrace>\<lambda>rv. if rv \<noteq> None then \<top> else P\<rbrace>"
121    by (wp alternative_wp | simp)+
122  have R: "\<And>P x g xs. (do x \<leftarrow> if P then return (Some x) else findM g xs;
123                         when (x = None) g'
124                       od) = (if P then return () else (findM g xs >>= (\<lambda>x . when (x = None) g')))"
125    by (simp add: when_def)
126  show ?thesis
127    apply (induct xs)
128     apply (simp add: when_def)
129     apply (fold dc_def, rule on_none)
130    apply (simp only: findM.simps bind_assoc)
131    apply (subst P)
132    apply (rule corres_guard_imp)
133      apply (rule corres_split [OF _ x])
134        apply (subst R)
135        apply (rule corres_if2)
136          apply (case_tac xa, simp_all)[1]
137         apply (rule corres_trivial, simp)
138        apply assumption
139       apply (rule Q)
140      apply (rule hoare_post_imp [OF _ z])
141      apply simp+
142    done
143qed
144
145lemma awesome_case1:
146  assumes x: "corres (=) P P' (return False) (g x)"
147  shows      "corres (\<lambda>a b. if b then (\<exists>a'. a = Some a' \<and> r a' (Some x)) else a = None)
148            P P' ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)"
149proof -
150  have P: "return None = liftM (\<lambda>x. None) (return False)"
151    by (simp add: liftM_def)
152  show ?thesis
153    apply (rule corres_alternate2)
154    apply (subst P, simp only: corres_liftM_simp, simp)
155    apply (subst corres_cong [OF refl refl refl refl])
156     defer
157     apply (rule x)
158    apply (simp add: return_def)
159    done
160qed
161
162lemma awesome_case2:
163  assumes x: "corres (\<lambda>a b. r a (Some x) \<and> b) P P' f (g x)"
164  shows      "corres (\<lambda>a b. if b then (\<exists>a'. a = Some a' \<and> r a' (Some x)) else a = None)
165            P P' ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)"
166  apply (rule corres_alternate1)
167  apply (fold liftM_def)
168  apply (simp add: o_def)
169  apply (rule corres_rel_imp [OF x])
170  apply simp
171  done
172
173lemma bind_select_corres:
174  assumes x: "corres (\<lambda>rvs rv'. \<exists>rv\<in>rvs. r rv rv') P P' m m'"
175  shows      "corres r P P' (m >>= select) m'"
176  apply (insert x)
177  apply (clarsimp simp: corres_underlying_def bind_def select_def split_def)
178  done
179
180lemma bind_select_fail_corres:
181  assumes x: "corres (\<lambda>rvs rv'. \<exists>rv\<in>rvs. r rv rv') P P' m m'"
182  shows      "corres r P P' (m >>= (\<lambda>x. select x \<sqinter> fail)) m'"
183  apply (insert x)
184  apply (clarsimp simp: corres_underlying_def bind_def
185                        select_def fail_def alternative_def split_def)
186  done
187
188(* Levity: added (20090721 10:56:29) *)
189declare objBitsT_koTypeOf [simp]
190
191lemma arch_switch_thread_corres:
192  "corres dc (valid_arch_state and valid_objs and valid_asid_map
193              and valid_vspace_objs and pspace_aligned and pspace_distinct
194              and valid_vs_lookup and valid_global_objs
195              and unique_table_refs o caps_of_state
196              and st_tcb_at runnable t)
197             (valid_arch_state' and valid_pspace' and st_tcb_at' runnable' t)
198             (arch_switch_to_thread t) (Arch.switchToThread t)"
199  apply (simp add: arch_switch_to_thread_def X64_H.switchToThread_def)
200  apply (rule corres_guard_imp)
201    apply (rule set_vm_root_corres[OF refl])
202   apply (clarsimp simp: st_tcb_at_tcb_at)
203  apply (clarsimp simp: valid_pspace'_def)
204  done
205
206lemma schedule_choose_new_thread_sched_act_rct[wp]:
207  "\<lbrace>\<top>\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace>"
208  unfolding schedule_choose_new_thread_def
209  by wp
210
211lemma tcbSchedAppend_corres:
212  notes trans_state_update'[symmetric, simp del]
213  shows
214  "corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action (tcb_sched_append) t) (tcbSchedAppend t)"
215  apply (simp only: tcbSchedAppend_def tcb_sched_action_def)
216  apply (rule corres_symb_exec_r [OF _ _ threadGet_inv, where Q'="\<lambda>rv. tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"])
217    defer
218    apply (wp threadGet_obj_at', simp, simp)
219   apply (rule no_fail_pre, wp, simp)
220  apply (case_tac queued)
221   apply (simp add: unless_def when_def)
222   apply (rule corres_no_failI)
223    apply wp+
224   apply (clarsimp simp: in_monad ethread_get_def gets_the_def bind_assoc
225                         assert_opt_def exec_gets is_etcb_at_def get_etcb_def get_tcb_queue_def
226                         set_tcb_queue_def simpler_modify_def)
227
228   apply (subgoal_tac "tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y))
229                       = (ready_queues a (tcb_domain y) (tcb_priority y))")
230    apply (simp add: state_relation_def ready_queues_relation_def)
231   apply (clarsimp simp: tcb_sched_append_def state_relation_def
232                         valid_queues'_def ready_queues_relation_def
233                         ekheap_relation_def etcb_relation_def
234                         obj_at'_def inQ_def projectKO_eq project_inject)
235   apply (drule_tac x=t in bspec,clarsimp)
236   apply clarsimp
237  apply (clarsimp simp: unless_def when_def cong: if_cong)
238  apply (rule stronger_corres_guard_imp)
239    apply (rule corres_split[where r'="(=)", OF _ ethreadget_corres])
240       apply (rule corres_split[where r'="(=)", OF _ ethreadget_corres])
241          apply (rule corres_split[where r'="(=)"])
242             apply (rule corres_split_noop_rhs2)
243                apply (rule corres_split_noop_rhs2)
244                   apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1]
245                  apply (rule addToBitmap_if_null_corres_noop)
246                 apply wp+
247               apply (simp add: tcb_sched_append_def)
248               apply (intro conjI impI)
249                apply (rule corres_guard_imp)
250                  apply (rule setQueue_corres)
251                 prefer 3
252                 apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre)
253                 apply (wp getQueue_corres getObject_tcb_wp  | simp add: etcb_relation_def threadGet_def)+
254  apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def
255                         projectKO_eq project_inject)
256  done
257
258
259crunch valid_pspace'[wp]: tcbSchedEnqueue valid_pspace'
260  (simp: unless_def)
261crunch valid_pspace'[wp]: tcbSchedAppend valid_pspace'
262  (simp: unless_def)
263crunch valid_pspace'[wp]: tcbSchedDequeue valid_pspace'
264
265crunch valid_arch_state'[wp]: tcbSchedEnqueue valid_arch_state'
266  (simp: unless_def)
267crunch valid_arch_state'[wp]: tcbSchedAppend valid_arch_state'
268  (simp: unless_def)
269crunch valid_arch_state'[wp]: tcbSchedDequeue valid_arch_state'
270
271crunch pred_tcb_at'[wp]: tcbSchedAppend, tcbSchedDequeue "pred_tcb_at' proj P t"
272  (wp: threadSet_pred_tcb_no_state simp: unless_def tcb_to_itcb'_def ignore: getObject setObject)
273
274crunch state_refs_of'[wp]: setQueue "\<lambda>s. P (state_refs_of' s)"
275
276lemma removeFromBitmap_valid_queues_no_bitmap[wp]:
277" \<lbrace> valid_queues_no_bitmap \<rbrace>
278     removeFromBitmap d p
279  \<lbrace>\<lambda>_. valid_queues_no_bitmap \<rbrace>"
280  unfolding bitmapQ_defs valid_queues_no_bitmap_def
281  by (wp| clarsimp simp: bitmap_fun_defs comp_def pred_conj_def)+
282
283lemma removeFromBitmap_valid_queues_no_bitmap_except[wp]:
284" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
285     removeFromBitmap d p
286  \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>"
287  unfolding bitmapQ_defs valid_queues_no_bitmap_except_def
288  by (wp| clarsimp simp: bitmap_fun_defs)+
289
290lemma removeFromBitmap_bitmapQ:
291  "\<lbrace> \<lambda>s. True \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. \<not> bitmapQ d p s \<rbrace>"
292  unfolding bitmapQ_defs bitmap_fun_defs
293  apply (wp| clarsimp simp: bitmap_fun_defs)+
294  apply (subst (asm) complement_nth_w2p, simp_all)
295  apply (fastforce intro!: order_less_le_trans[OF word_unat_mask_lt] simp: word_size wordRadix_def')
296  done
297
298lemma removeFromBitmap_valid_bitmapQ[wp]:
299" \<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and
300    (\<lambda>s. ksReadyQueues s (d,p) = []) \<rbrace>
301     removeFromBitmap d p
302  \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>"
303proof -
304  have "\<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and
305            (\<lambda>s. ksReadyQueues s (d,p) = []) \<rbrace>
306         removeFromBitmap d p
307         \<lbrace>\<lambda>_. valid_bitmapQ_except d p and  bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and
308              (\<lambda>s. \<not> bitmapQ d p s \<and> ksReadyQueues s (d,p) = []) \<rbrace>"
309    by (rule hoare_pre)
310       (wp removeFromBitmap_valid_queues_no_bitmap_except removeFromBitmap_valid_bitmapQ_except
311           removeFromBitmap_bitmapQ, simp)
312  thus ?thesis
313    by - (erule hoare_strengthen_post; fastforce elim: valid_bitmap_valid_bitmapQ_exceptE)
314qed
315
316lemma threadSet_bitmapQ_no_L1_orphans[wp]:
317  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> threadSet f t \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>"
318  unfolding bitmapQ_defs threadSet_def
319  by (wp hoare_vcg_all_lift hoare_vcg_imp_lift) simp
320
321lemma threadSet_bitmapQ_no_L2_orphans[wp]:
322  "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> threadSet f t \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>"
323  unfolding bitmapQ_defs threadSet_def
324  by (wp hoare_vcg_all_lift hoare_vcg_imp_lift) simp
325
326lemma threadSet_valid_bitmapQ[wp]:
327  "\<lbrace> valid_bitmapQ \<rbrace> threadSet f t \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>"
328  unfolding bitmapQ_defs threadSet_def
329  by (wp hoare_vcg_all_lift hoare_vcg_imp_lift hoare_vcg_conj_lift | wps)+
330
331lemma setQueue_valid_queues_no_bitmap_except:
332  "\<lbrace> valid_queues_no_bitmap_except t
333      and (\<lambda>s. \<forall>t \<in> set ts. obj_at' (inQ d p and runnable' \<circ> tcbState) t s)
334      and K (t \<notin> set ts)
335      and K (distinct ts) and K (d \<le> maxDomain \<and> p \<le> maxPriority)\<rbrace>
336  setQueue d p ts
337  \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>"
338  unfolding setQueue_def valid_queues_def
339  by (wp, fastforce simp: valid_queues_no_bitmap_except_def)
340
341(* this should be the actual weakest precondition to establish valid_queues
342   under tagging a thread as not queued *)
343lemma threadSet_valid_queues_dequeue_wp:
344 "\<lbrace> valid_queues_no_bitmap_except t and
345        valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and
346        (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d,p))) \<rbrace>
347          threadSet (tcbQueued_update (\<lambda>_. False)) t
348       \<lbrace>\<lambda>rv. valid_queues \<rbrace>"
349  unfolding threadSet_def
350  apply (rule hoare_seq_ext[OF _ getObject_tcb_sp])
351  apply (rule hoare_pre)
352   apply (simp add: valid_queues_def valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def)
353   apply (wp setObject_queues_unchanged_tcb hoare_Ball_helper hoare_vcg_all_lift
354             setObject_tcb_strongest)
355  apply (clarsimp simp: valid_queues_no_bitmap_except_def obj_at'_def valid_queues_no_bitmap_def)
356  done
357
358(* FIXME move *)
359lemmas obj_at'_conjI = obj_at_conj'
360
361lemma obj_at'_disj:
362  "\<lbrakk> obj_at' (\<lambda>x. P x s) t s \<or> obj_at' (\<lambda>x. Q x s) t s  \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. P x s \<or> Q x s) t s"
363  by (auto simp: obj_at'_def)
364
365(* FIXME move, also not_obj_at' is too type constrained *)
366lemma obj_at'_imp:
367  "\<lbrakk> obj_at' (\<lambda>(_::'a::pspace_storable). True) t s ;
368     obj_at' (\<lambda>(x::'a). P x s) t s \<longrightarrow> obj_at' (\<lambda>x. Q x s) t s  \<rbrakk>
369   \<Longrightarrow> obj_at' (\<lambda>x. P x s \<longrightarrow> Q x s) t s"
370  by (auto simp: obj_at'_def)
371
372lemma setQueue_valid_queues_no_bitmap_except_dequeue_wp:
373  "\<And>d p ts t.
374   \<lbrace> \<lambda>s. valid_queues_no_bitmap_except t s \<and>
375         (\<forall>t' \<in> set ts. obj_at' (inQ d p and runnable' \<circ> tcbState) t' s) \<and>
376         t \<notin> set ts \<and> distinct ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain \<rbrace>
377       setQueue d p ts
378   \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t \<rbrace>"
379  unfolding setQueue_def valid_queues_no_bitmap_except_def null_def
380  by wp force
381
382definition (* if t is in a queue, it should be tagged with right priority and domain *)
383  "correct_queue t s \<equiv> \<forall>d p. t \<in> set(ksReadyQueues s (d, p)) \<longrightarrow>
384             (obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s)"
385
386lemma valid_queues_no_bitmap_correct_queueI[intro]:
387  "valid_queues_no_bitmap s \<Longrightarrow> correct_queue t s"
388  unfolding correct_queue_def valid_queues_no_bitmap_def
389  by (fastforce simp: obj_at'_def inQ_def)
390
391
392lemma tcbSchedDequeue_valid_queues_weak:
393  "\<lbrace> valid_queues_no_bitmap_except t and valid_bitmapQ and
394     bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and
395     correct_queue t and
396     obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority) t \<rbrace>
397   tcbSchedDequeue t
398   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>"
399proof -
400  show ?thesis
401  unfolding tcbSchedDequeue_def null_def valid_queues_def
402  apply wp (* stops on threadSet *)
403          apply (rule hoare_post_eq[OF _ threadSet_valid_queues_dequeue_wp],
404                 simp add: valid_queues_def)
405         apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift)+
406             apply (wp hoare_vcg_imp_lift setQueue_valid_queues_no_bitmap_except_dequeue_wp
407                       setQueue_valid_bitmapQ threadGet_const_tcb_at)+
408  (* wp done *)
409  apply (normalise_obj_at')
410  apply (clarsimp simp: correct_queue_def)
411  apply (normalise_obj_at')
412  apply (fastforce simp add: valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def elim: obj_at'_weaken)+
413  done
414qed
415
416lemma tcbSchedDequeue_valid_queues:
417  "\<lbrace>Invariants_H.valid_queues
418    and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t
419    and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t\<rbrace>
420     tcbSchedDequeue t
421   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>"
422  apply (rule hoare_pre, rule tcbSchedDequeue_valid_queues_weak)
423  apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def)
424  done
425
426lemma tcbSchedAppend_valid_queues'[wp]:
427  (* most of this is identical to tcbSchedEnqueue_valid_queues' in TcbAcc_R *)
428  "\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. valid_queues'\<rbrace>"
429  apply (simp add: tcbSchedAppend_def)
430  apply (rule hoare_pre)
431   apply (rule_tac B="\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"
432           in hoare_seq_ext)
433    apply (rename_tac queued)
434    apply (case_tac queued; simp_all add: unless_def when_def)
435     apply (wp threadSet_valid_queues' setQueue_valid_queues' | simp)+
436         apply (subst conj_commute, wp)
437         apply (rule hoare_pre_post, assumption)
438         apply (clarsimp simp: addToBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
439                               getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def)
440         apply wp
441         apply fastforce
442        apply wp
443       apply (subst conj_commute)
444       apply (clarsimp simp: imp_conj_taut)
445       apply (rule_tac Q="\<lambda>rv. valid_queues'
446                   and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t
447                   and obj_at' (\<lambda>obj. tcbPriority obj = prio) t
448                   and obj_at' (\<lambda>obj. tcbDomain obj = tdom) t
449                   and (\<lambda>s. t \<in> set (ksReadyQueues s (tdom, prio)))"
450                   in hoare_post_imp)
451        apply (clarsimp simp: valid_queues'_def obj_at'_def projectKOs inQ_def)
452       apply (wp setQueue_valid_queues' | simp | simp add: setQueue_def)+
453     apply (wp getObject_tcb_wp | simp add: threadGet_def)+
454     apply (clarsimp simp: obj_at'_def inQ_def projectKOs valid_queues'_def)
455    apply (wp getObject_tcb_wp | simp add: threadGet_def)+
456  apply (clarsimp simp: obj_at'_def)
457  done
458
459crunch norq[wp]: threadSet "\<lambda>s. P (ksReadyQueues s)"
460  (simp: updateObject_default_def ignore: setObject getObject)
461
462lemma removeFromBitmap_valid_queues'[wp]:
463  "\<lbrace> valid_queues' \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_queues' \<rbrace>"
464  unfolding valid_queues'_def
465  by (wp| simp add: bitmap_fun_defs)+
466
467lemma threadSet_valid_queues'_dequeue: (* threadSet_valid_queues' is too weak for dequeue *)
468  "\<lbrace>\<lambda>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and>
469        obj_at' (inQ d p) t s \<rbrace>
470   threadSet (tcbQueued_update (\<lambda>_. False)) t
471   \<lbrace>\<lambda>rv. valid_queues' \<rbrace>"
472   unfolding valid_queues'_def
473   apply (rule hoare_pre)
474    apply (wp hoare_vcg_all_lift)
475    apply (simp only: imp_conv_disj not_obj_at')
476   apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift)
477   apply (simp add: not_obj_at')
478   apply (clarsimp simp: typ_at_tcb')
479   apply normalise_obj_at'
480   apply (fastforce elim: obj_at'_weaken simp: inQ_def)
481   done
482
483lemma setQueue_ksReadyQueues_lift:
484  "\<lbrace> \<lambda>s. P (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := ts)\<rparr>) ts \<rbrace>
485   setQueue d p ts
486   \<lbrace> \<lambda>_ s. P s (ksReadyQueues s (d,p))\<rbrace>"
487  unfolding setQueue_def
488  by (wp, clarsimp simp: fun_upd_def cong: if_cong)
489
490lemma tcbSchedDequeue_valid_queues'[wp]:
491  "\<lbrace>valid_queues' and tcb_at' t\<rbrace>
492    tcbSchedDequeue t \<lbrace>\<lambda>_. valid_queues'\<rbrace>"
493  unfolding tcbSchedDequeue_def
494  apply (rule_tac B="\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"
495                in hoare_seq_ext)
496   prefer 2
497   apply (wp threadGet_const_tcb_at)
498   apply (fastforce simp: obj_at'_def)
499  apply clarsimp
500  apply (rename_tac queued)
501  apply (case_tac queued, simp_all)
502   apply wp
503        apply (rule_tac d=tdom and p=prio in threadSet_valid_queues'_dequeue)
504       apply (rule hoare_pre_post, assumption)
505       apply (wp | clarsimp simp: bitmap_fun_defs)+
506      apply (wp hoare_vcg_all_lift setQueue_ksReadyQueues_lift)
507     apply clarsimp
508     apply (wp threadGet_obj_at' threadGet_const_tcb_at)+
509   apply clarsimp
510   apply (rule context_conjI, clarsimp simp: obj_at'_def)
511   apply (clarsimp simp: valid_queues'_def obj_at'_def projectKOs inQ_def|wp)+
512  done
513
514crunch tcb_at'[wp]: tcbSchedEnqueue "tcb_at' t"
515  (simp: unless_def)
516crunch tcb_at'[wp]: tcbSchedAppend "tcb_at' t"
517  (simp: unless_def)
518crunch tcb_at'[wp]: tcbSchedDequeue "tcb_at' t"
519
520crunch state_refs_of'[wp]: tcbSchedEnqueue "\<lambda>s. P (state_refs_of' s)"
521  (wp: refl simp: crunch_simps unless_def)
522crunch state_refs_of'[wp]: tcbSchedAppend "\<lambda>s. P (state_refs_of' s)"
523  (wp: refl simp: crunch_simps unless_def)
524crunch state_refs_of'[wp]: tcbSchedDequeue "\<lambda>s. P (state_refs_of' s)"
525  (wp: refl simp: crunch_simps)
526
527crunch cap_to'[wp]: tcbSchedEnqueue "ex_nonz_cap_to' p"
528  (simp: unless_def)
529crunch cap_to'[wp]: tcbSchedAppend "ex_nonz_cap_to' p"
530  (simp: unless_def)
531crunch cap_to'[wp]: tcbSchedDequeue "ex_nonz_cap_to' p"
532
533crunch iflive'[wp]: setQueue if_live_then_nonz_cap'
534
535lemma tcbSchedAppend_iflive'[wp]:
536  "\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' tcb\<rbrace>
537    tcbSchedAppend tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>"
538  apply (simp add: tcbSchedAppend_def unless_def)
539  apply (wp threadSet_iflive' hoare_drop_imps | simp add: crunch_simps)+
540  done
541
542lemma tcbSchedDequeue_iflive'[wp]:
543  "\<lbrace>if_live_then_nonz_cap'\<rbrace> tcbSchedDequeue tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>"
544  apply (simp add: tcbSchedDequeue_def)
545  apply (wp threadSet_iflive' hoare_when_weak_wp | simp add: crunch_simps)+
546       apply ((wp | clarsimp simp: bitmap_fun_defs)+)[1] (* deal with removeFromBitmap *)
547      apply (wp threadSet_iflive' hoare_when_weak_wp | simp add: crunch_simps)+
548      apply (rule_tac Q="\<lambda>rv. \<top>" in hoare_post_imp, fastforce)
549      apply (wp | simp add: crunch_simps)+
550  done
551
552crunch ifunsafe'[wp]: tcbSchedEnqueue if_unsafe_then_cap'
553  (simp: unless_def)
554crunch ifunsafe'[wp]: tcbSchedAppend if_unsafe_then_cap'
555  (simp: unless_def)
556crunch ifunsafe'[wp]: tcbSchedDequeue if_unsafe_then_cap'
557
558crunch idle'[wp]: tcbSchedEnqueue valid_idle'
559  (simp: crunch_simps unless_def)
560crunch idle'[wp]: tcbSchedAppend valid_idle'
561  (simp: crunch_simps unless_def)
562crunch idle'[wp]: tcbSchedDequeue valid_idle'
563  (simp: crunch_simps)
564
565crunch global_refs'[wp]: tcbSchedEnqueue valid_global_refs'
566  (wp: threadSet_global_refs simp: unless_def ignore: getObject setObject)
567crunch global_refs'[wp]: tcbSchedAppend valid_global_refs'
568  (wp: threadSet_global_refs simp: unless_def)
569crunch global_refs'[wp]: tcbSchedDequeue valid_global_refs'
570  (wp: threadSet_global_refs)
571
572crunch irq_node'[wp]: tcbSchedEnqueue "\<lambda>s. P (irq_node' s)"
573  (simp: unless_def)
574crunch irq_node'[wp]: tcbSchedAppend "\<lambda>s. P (irq_node' s)"
575  (simp: unless_def)
576crunch irq_node'[wp]: tcbSchedDequeue "\<lambda>s. P (irq_node' s)"
577
578crunch typ_at'[wp]: tcbSchedEnqueue "\<lambda>s. P (typ_at' T p s)"
579  (simp: unless_def)
580crunch typ_at'[wp]: tcbSchedAppend "\<lambda>s. P (typ_at' T p s)"
581  (simp: unless_def)
582crunch typ_at'[wp]: tcbSchedDequeue "\<lambda>s. P (typ_at' T p s)"
583
584crunch ctes_of[wp]: tcbSchedEnqueue "\<lambda>s. P (ctes_of s)"
585  (simp: unless_def)
586crunch ctes_of[wp]: tcbSchedAppend "\<lambda>s. P (ctes_of s)"
587  (simp: unless_def)
588crunch ctes_of[wp]: tcbSchedDequeue "\<lambda>s. P (ctes_of s)"
589
590crunch ksInterrupt[wp]: tcbSchedEnqueue "\<lambda>s. P (ksInterruptState s)"
591  (simp: unless_def)
592crunch ksInterrupt[wp]: tcbSchedAppend "\<lambda>s. P (ksInterruptState s)"
593  (simp: unless_def)
594crunch ksInterrupt[wp]: tcbSchedDequeue "\<lambda>s. P (ksInterruptState s)"
595
596crunch irq_states[wp]: tcbSchedEnqueue valid_irq_states'
597  (simp: unless_def)
598crunch irq_states[wp]: tcbSchedAppend valid_irq_states'
599  (simp: unless_def)
600crunch irq_states[wp]: tcbSchedDequeue valid_irq_states'
601
602crunch ct'[wp]: tcbSchedEnqueue "\<lambda>s. P (ksCurThread s)"
603  (simp: unless_def)
604crunch ct'[wp]: tcbSchedAppend "\<lambda>s. P (ksCurThread s)"
605  (simp: unless_def)
606crunch ct'[wp]: tcbSchedDequeue "\<lambda>s. P (ksCurThread s)"
607
608lemma tcbSchedEnqueue_vms'[wp]:
609  "\<lbrace>valid_machine_state'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>"
610  apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def)
611  apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedEnqueue_ksMachine)
612  done
613
614crunch ksCurDomain[wp]: tcbSchedEnqueue "\<lambda>s. P (ksCurDomain s)"
615(simp: unless_def)
616
617lemma tcbSchedEnqueue_tcb_in_cur_domain'[wp]:
618  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>"
619  apply (rule tcb_in_cur_domain'_lift)
620   apply wp
621  apply (clarsimp simp: tcbSchedEnqueue_def)
622  apply (wpsimp simp: unless_def)+
623  done
624
625lemma ct_idle_or_in_cur_domain'_lift2:
626  "\<lbrakk> \<And>t. \<lbrace>tcb_in_cur_domain' t\<rbrace>         f \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>;
627     \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s) \<rbrace>       f \<lbrace>\<lambda>_ s. P (ksCurThread s) \<rbrace>;
628     \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s) \<rbrace>      f \<lbrace>\<lambda>_ s. P (ksIdleThread s) \<rbrace>;
629     \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s) \<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s) \<rbrace>\<rbrakk>
630   \<Longrightarrow> \<lbrace> ct_idle_or_in_cur_domain'\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>"
631  apply (unfold ct_idle_or_in_cur_domain'_def)
632  apply (rule hoare_lift_Pf2[where f=ksCurThread])
633  apply (rule hoare_lift_Pf2[where f=ksSchedulerAction])
634  including no_pre
635  apply (wp static_imp_wp hoare_vcg_disj_lift)
636  apply simp+
637  done
638
639lemma tcbSchedEnqueue_invs'[wp]:
640  "\<lbrace>invs'
641    and st_tcb_at' runnable' t
642    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
643     tcbSchedEnqueue t
644   \<lbrace>\<lambda>_. invs'\<rbrace>"
645  apply (simp add: invs'_def valid_state'_def)
646  apply (rule hoare_pre)
647   apply (wp tcbSchedEnqueue_ct_not_inQ valid_irq_node_lift irqs_masked_lift hoare_vcg_disj_lift
648             valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
649             untyped_ranges_zero_lift valid_ioports_lift'
650        | simp add: cteCaps_of_def o_def
651        | auto elim!: st_tcb_ex_cap'' valid_objs'_maxDomain valid_objs'_maxPriority split: thread_state.split_asm simp: valid_pspace'_def)+
652  done
653
654crunch ksMachine[wp]: tcbSchedAppend "\<lambda>s. P (ksMachineState s)"
655  (simp: unless_def)
656
657lemma tcbSchedAppend_vms'[wp]:
658  "\<lbrace>valid_machine_state'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>"
659  apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def)
660  apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedAppend_ksMachine)
661  done
662
663crunch pspace_domain_valid[wp]: tcbSchedAppend "pspace_domain_valid"
664  (simp: unless_def)
665
666crunch ksCurDomain[wp]: tcbSchedAppend "\<lambda>s. P (ksCurDomain s)"
667(simp: unless_def)
668
669crunch ksIdleThread[wp]: tcbSchedAppend "\<lambda>s. P (ksIdleThread s)"
670(simp: unless_def)
671
672crunch ksDomSchedule[wp]: tcbSchedAppend "\<lambda>s. P (ksDomSchedule s)"
673(simp: unless_def)
674
675lemma tcbSchedAppend_tcbDomain[wp]:
676  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>
677     tcbSchedAppend t
678   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>"
679  apply (clarsimp simp: tcbSchedAppend_def)
680  apply (wpsimp simp: unless_def)+
681  done
682
683lemma tcbSchedAppend_tcbPriority[wp]:
684  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>
685     tcbSchedAppend t
686   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>"
687  apply (clarsimp simp: tcbSchedAppend_def)
688  apply (wpsimp simp: unless_def)+
689  done
690
691lemma tcbSchedAppend_tcb_in_cur_domain'[wp]:
692  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>"
693  apply (rule tcb_in_cur_domain'_lift)
694   apply wp+
695  done
696
697crunch ksDomScheduleIdx[wp]: tcbSchedAppend "\<lambda>s. P (ksDomScheduleIdx s)"
698  (simp: unless_def)
699
700crunch gsUntypedZeroRanges[wp]: tcbSchedAppend, tcbSchedDequeue "\<lambda>s. P (gsUntypedZeroRanges s)"
701  (simp: unless_def)
702
703crunches tcbSchedDequeue, tcbSchedAppend
704  for arch'[wp]: "\<lambda>s. P (ksArchState s)"
705  and ioports'[wp]: valid_ioports'
706  (wp: valid_ioports_lift'')
707
708lemma tcbSchedAppend_invs_but_ct_not_inQ':
709  "\<lbrace>invs' and st_tcb_at' runnable' t and tcb_in_cur_domain' t \<rbrace>
710   tcbSchedAppend t \<lbrace>\<lambda>_. all_invs_but_ct_not_inQ'\<rbrace>"
711  apply (simp add: invs'_def valid_state'_def)
712  apply (rule hoare_pre)
713   apply (wp sch_act_wf_lift valid_irq_node_lift irqs_masked_lift
714             valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
715             untyped_ranges_zero_lift
716        | simp add: cteCaps_of_def o_def
717        | fastforce elim!: st_tcb_ex_cap'' split: thread_state.split_asm)+
718  done
719
720lemma tcbSchedAppend_sch_act_wf[wp]:
721  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedAppend thread
722  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
723  apply (simp add:tcbSchedAppend_def bitmap_fun_defs)
724  apply (wp hoare_unless_wp setQueue_sch_act threadGet_wp|simp)+
725  apply (fastforce simp:typ_at'_def obj_at'_def)
726  done
727
728lemma tcbSchedAppend_invs'[wp]:
729  "\<lbrace>invs'
730    and st_tcb_at' runnable' t
731    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
732     tcbSchedAppend t
733   \<lbrace>\<lambda>_. invs'\<rbrace>"
734  apply (simp add: invs'_def valid_state'_def)
735  apply (rule hoare_pre)
736   apply (wp tcbSchedAppend_ct_not_inQ valid_irq_node_lift irqs_masked_lift hoare_vcg_disj_lift
737             valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
738             untyped_ranges_zero_lift
739        | simp add: cteCaps_of_def o_def
740        | auto elim!: st_tcb_ex_cap'' valid_objs'_maxDomain valid_objs'_maxPriority split: thread_state.split_asm simp: valid_pspace'_def)+
741  done
742
743lemma tcbSchedAppend_invs'_weak:
744  "\<lbrace>invs' and st_tcb_at' runnable' t  and (\<lambda>s. t \<noteq> ksCurThread s) \<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. invs'\<rbrace>"
745  apply (simp add: invs'_def valid_state'_def)
746  apply (rule hoare_pre)
747   apply (wp tcbSchedAppend_ct_not_inQ sch_act_wf_lift valid_irq_node_lift irqs_masked_lift
748             valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
749             untyped_ranges_zero_lift
750       | simp add: cteCaps_of_def o_def
751       | fastforce elim!: st_tcb_ex_cap'' split: thread_state.split_asm)+
752  done
753
754lemma tcbSchedEnqueue_invs'_not_ResumeCurrentThread:
755  "\<lbrace>invs'
756    and st_tcb_at' runnable' t
757    and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
758     tcbSchedEnqueue t
759   \<lbrace>\<lambda>_. invs'\<rbrace>"
760  by wpsimp
761
762lemma tcbSchedAppend_invs'_not_ResumeCurrentThread:
763  "\<lbrace>invs'
764    and st_tcb_at' runnable' t
765    and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
766     tcbSchedAppend t
767   \<lbrace>\<lambda>_. invs'\<rbrace>"
768  by wpsimp
769
770lemma tcb_at'_has_tcbDomain:
771 "tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbDomain tcb = p) t s"
772 by (clarsimp simp add: obj_at'_def)
773
774lemma tcbSchedEnqueue_in_ksQ:
775  "\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t
776   \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace>"
777  apply (rule_tac Q="\<lambda>s. \<exists>d p. valid_queues' s \<and>
778                             obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and>
779                             obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
780           in hoare_pre_imp)
781   apply (clarsimp simp: tcb_at'_has_tcbPriority tcb_at'_has_tcbDomain)
782  apply (rule hoare_vcg_ex_lift)+
783  apply (simp add: tcbSchedEnqueue_def unless_def)
784  apply wpsimp
785    apply (rule_tac Q="\<lambda>rv s. tdom = d \<and> rv = p \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
786                            \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
787             in hoare_post_imp, clarsimp)
788    apply (wp, (wp threadGet_const)+)
789  apply (rule_tac Q="\<lambda>rv s.
790             obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and>
791             obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<and>
792             obj_at' (\<lambda>tcb. tcbQueued tcb = rv) t s \<and>
793             (rv \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)))" in hoare_post_imp)
794   apply (clarsimp simp: o_def elim!: obj_at'_weakenE)
795  apply (wp threadGet_obj_at' hoare_vcg_imp_lift threadGet_const)
796  apply (clarsimp simp: valid_queues'_def)
797  apply (drule_tac x=d in spec)
798  apply (drule_tac x=p in spec)
799  apply (drule_tac x=t in spec)
800  apply normalise_obj_at'
801  apply (clarsimp simp: inQ_def)
802  done
803
804crunch ksMachine[wp]: tcbSchedDequeue "\<lambda>s. P (ksMachineState s)"
805  (simp: unless_def)
806
807lemma tcbSchedDequeue_vms'[wp]:
808  "\<lbrace>valid_machine_state'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>"
809  apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def)
810  apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedDequeue_ksMachine)
811  done
812
813crunch pspace_domain_valid[wp]: tcbSchedDequeue "pspace_domain_valid"
814
815crunch ksCurDomain[wp]: tcbSchedDequeue "\<lambda>s. P (ksCurDomain s)"
816(simp: unless_def)
817
818crunch ksIdleThread[wp]: tcbSchedDequeue "\<lambda>s. P (ksIdleThread s)"
819(simp: unless_def)
820
821crunch ksDomSchedule[wp]: tcbSchedDequeue "\<lambda>s. P (ksDomSchedule s)"
822(simp: unless_def)
823
824crunch ksDomScheduleIdx[wp]: tcbSchedDequeue "\<lambda>s. P (ksDomScheduleIdx s)"
825(simp: unless_def)
826
827lemma tcbSchedDequeue_tcb_in_cur_domain'[wp]:
828  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>"
829  apply (rule tcb_in_cur_domain'_lift)
830   apply wp
831  apply (clarsimp simp: tcbSchedDequeue_def)
832  apply (wp hoare_when_weak_wp | simp)+
833  done
834
835lemma tcbSchedDequeue_tcbDomain[wp]:
836  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>
837     tcbSchedDequeue t
838   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>"
839  apply (clarsimp simp: tcbSchedDequeue_def)
840  apply (wp hoare_when_weak_wp | simp)+
841  done
842
843lemma tcbSchedDequeue_tcbPriority[wp]:
844  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>
845     tcbSchedDequeue t
846   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>"
847  apply (clarsimp simp: tcbSchedDequeue_def)
848  apply (wp hoare_when_weak_wp | simp)+
849  done
850
851lemma tcbSchedDequeue_invs'[wp]:
852  "\<lbrace>invs' and tcb_at' t\<rbrace>
853     tcbSchedDequeue t
854   \<lbrace>\<lambda>_. invs'\<rbrace>"
855  unfolding invs'_def valid_state'_def
856  apply (rule hoare_pre)
857   apply (wp tcbSchedDequeue_ct_not_inQ sch_act_wf_lift valid_irq_node_lift irqs_masked_lift
858             valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
859             tcbSchedDequeue_valid_queues
860             untyped_ranges_zero_lift
861        | simp add: cteCaps_of_def o_def)+
862  apply (fastforce elim: valid_objs'_maxDomain valid_objs'_maxPriority simp: valid_pspace'_def)+
863  done
864
865lemma no_fail_isRunnable[wp]:
866  "no_fail (tcb_at' t) (isRunnable t)"
867  apply (simp add: isRunnable_def isBlocked_def)
868  apply (rule no_fail_pre, wp)
869  apply (clarsimp simp: pred_tcb_at'_def)
870  done
871
872lemma corres_when_r:
873  "\<lbrakk> G \<Longrightarrow> corres r P P' f g;
874   \<not> G \<Longrightarrow> corres r Q Q' f (return ()) \<rbrakk>
875  \<Longrightarrow> corres r (P and Q) (\<lambda>s. (G \<longrightarrow> P' s) \<and> (\<not>G \<longrightarrow> Q' s)) f (when G g)"
876  apply (cases G, simp_all add: when_def)
877   apply (rule corres_guard_imp, simp+)+
878  done
879
880lemma cur_thread_update_corres:
881  "corres dc \<top> \<top> (modify (cur_thread_update (\<lambda>_. t))) (setCurThread t)"
882  apply (unfold setCurThread_def)
883  apply (rule corres_modify)
884  apply (simp add: state_relation_def swp_def)
885  done
886
887lemma arch_switch_thread_tcb_at' [wp]: "\<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>"
888  by (unfold X64_H.switchToThread_def, wp typ_at_lift_tcb')
889
890crunch typ_at'[wp]: "switchToThread" "\<lambda>s. P (typ_at' T p s)"
891  (ignore: )
892
893lemma Arch_switchToThread_pred_tcb'[wp]:
894  "\<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace>
895   Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace>"
896proof -
897  have pos: "\<And>P t t'. \<lbrace>pred_tcb_at' proj P t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace>"
898    apply (simp add:  pred_tcb_at'_def X64_H.switchToThread_def)
899     apply (rule setVMRoot_obj_at)
900    done
901  show ?thesis
902    apply (rule P_bool_lift [OF pos])
903    by (rule lift_neg_pred_tcb_at' [OF ArchThreadDecls_H_X64_H_switchToThread_typ_at' pos])
904qed
905
906
907crunch ksQ[wp]: storeWordUser "\<lambda>s. P (ksReadyQueues s p)"
908crunch ksQ[wp]: setVMRoot "\<lambda>s. P (ksReadyQueues s)"
909(wp: crunch_wps simp: crunch_simps)
910crunch ksIdleThread[wp]: storeWordUser "\<lambda>s. P (ksIdleThread s)"
911crunch ksIdleThread[wp]: asUser "\<lambda>s. P (ksIdleThread s)"
912(wp: crunch_wps simp: crunch_simps)
913crunch ksQ[wp]: asUser "\<lambda>s. P (ksReadyQueues s p)"
914(wp: crunch_wps simp: crunch_simps)
915
916lemma arch_switch_thread_ksQ[wp]:
917  "\<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>"
918  apply (simp add: X64_H.switchToThread_def)
919  apply (wp)
920  done
921
922crunch valid_queues[wp]: "Arch.switchToThread" "Invariants_H.valid_queues"
923(wp: crunch_wps simp: crunch_simps)
924
925lemma switch_thread_corres:
926  "corres dc (valid_arch_state and valid_objs and valid_asid_map
927                and valid_vspace_objs and pspace_aligned and pspace_distinct
928                and valid_vs_lookup and valid_global_objs
929                and unique_table_refs o caps_of_state
930                and st_tcb_at runnable t and valid_etcbs)
931             (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues
932                and st_tcb_at' runnable' t and cur_tcb')
933             (switch_to_thread t) (switchToThread t)"
934  (is "corres _ ?PA ?PH _ _")
935
936proof -
937  have mainpart: "corres dc (?PA) (?PH)
938     (do y \<leftarrow> arch_switch_to_thread t;
939         y \<leftarrow> (tcb_sched_action tcb_sched_dequeue t);
940         modify (cur_thread_update (\<lambda>_. t))
941      od)
942     (do y \<leftarrow> Arch.switchToThread t;
943         y \<leftarrow> tcbSchedDequeue t;
944         setCurThread t
945      od)"
946    apply (rule corres_guard_imp)
947      apply (rule corres_split [OF _ arch_switch_thread_corres])
948        apply (rule corres_split[OF cur_thread_update_corres tcbSchedDequeue_corres])
949         apply (wp|clarsimp simp: tcb_at_is_etcb_at st_tcb_at_tcb_at)+
950    done
951
952  show ?thesis
953    apply -
954    apply (simp add: switch_to_thread_def Thread_H.switchToThread_def)
955    apply (rule corres_symb_exec_l [where Q = "\<lambda> s rv. (?PA and (=) rv) s",
956                                    OF corres_symb_exec_l [OF mainpart]])
957    apply (auto intro: no_fail_pre [OF no_fail_assert]
958                      no_fail_pre [OF no_fail_get]
959                dest: st_tcb_at_tcb_at [THEN get_tcb_at] |
960           simp add: assert_def | wp)+
961    done
962qed
963
964lemma allActiveTCBs_corres:
965  assumes "\<And>threads. corres r (P threads) P' (m threads) m'"
966  shows "corres r (\<lambda>s. P {x. getActiveTCB x s \<noteq> None} s) P' (do threads \<leftarrow> allActiveTCBs; m threads od) m'"
967  apply (simp add: allActiveTCBs_def)
968  apply (simp add: bind_def get_def)
969  apply (insert assms)
970  apply (simp add: corres_underlying_def)
971  apply force
972  done
973
974lemma typ_at'_typ_at'_mask: "\<And>s. \<lbrakk> typ_at' t (P s) s \<rbrakk> \<Longrightarrow>  typ_at' t (P s && ~~mask (objBitsT t)) s"
975  apply (rule split_state_strg [where P = "typ_at' t", THEN mp])
976  apply (frule typ_at_aligned')
977  apply (clarsimp dest!: is_aligned_neg_mask_eq)
978  done
979
980lemma arch_switch_idle_thread_corres:
981  "corres dc
982        (valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state
983           and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct
984           and valid_vspace_objs and valid_idle)
985        (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle')
986        arch_switch_to_idle_thread Arch.switchToIdleThread"
987  apply (simp add: arch_switch_to_idle_thread_def
988                X64_H.switchToIdleThread_def)
989  apply (corressimp corres: git_corres set_vm_root_corres)
990  apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb)
991  done
992
993lemma switch_idle_thread_corres:
994  "corres dc invs invs_no_cicd' switch_to_idle_thread switchToIdleThread"
995  apply (simp add: switch_to_idle_thread_def Thread_H.switchToIdleThread_def)
996  apply (rule corres_guard_imp)
997    apply (rule corres_split [OF _ git_corres])
998      apply (rule corres_split [OF _ arch_switch_idle_thread_corres])
999        apply (unfold setCurThread_def)
1000        apply (rule corres_trivial, rule corres_modify)
1001        apply (simp add: state_relation_def cdt_relation_def)
1002       apply (wp+, simp+)
1003   apply (simp add: invs_unique_refs invs_valid_vs_lookup invs_valid_objs invs_valid_asid_map
1004                    invs_arch_state invs_valid_global_objs invs_psp_aligned invs_distinct
1005                    invs_valid_idle invs_vspace_objs)
1006  apply (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def)
1007  done
1008
1009lemma gq_sp: "\<lbrace>P\<rbrace> getQueue d p \<lbrace>\<lambda>rv. P and (\<lambda>s. ksReadyQueues s (d, p) = rv)\<rbrace>"
1010  by (unfold getQueue_def, rule gets_sp)
1011
1012lemma gq_se: "\<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> True\<rbrace> getQueue d p \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>"
1013  by (simp add: getQueue_def)
1014
1015lemma setQueue_no_change_ct[wp]:
1016  "\<lbrace>ct_in_state' st\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. ct_in_state' st\<rbrace>"
1017  apply (simp add: setQueue_def)
1018  apply wp
1019  apply (simp add: ct_in_state'_def pred_tcb_at'_def)
1020  done
1021
1022lemma sch_act_wf:
1023  "sch_act_wf sa s = ((\<forall>t. sa = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and>
1024                                                    tcb_in_cur_domain' t s) \<and>
1025                      (sa = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s))"
1026  by (case_tac sa,  simp_all add: )
1027
1028declare gq_wp[wp]
1029declare setQueue_obj_at[wp]
1030
1031lemma ready_tcb':
1032   "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); invs' s \<rbrakk>
1033        \<Longrightarrow> obj_at' (inQ d p) t s"
1034  apply (clarsimp simp: invs'_def valid_state'_def
1035                        valid_pspace'_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def)
1036  apply (drule_tac x=d in spec)
1037  apply (drule_tac x=p in spec)
1038  apply (clarsimp)
1039  apply (drule(1) bspec)
1040  apply (erule obj_at'_weakenE)
1041  apply (simp)
1042  done
1043
1044lemma ready_tcb_valid_queues:
1045   "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); valid_queues s \<rbrakk>
1046        \<Longrightarrow> obj_at' (inQ d p) t s"
1047  apply (clarsimp simp: invs'_def valid_state'_def
1048                        valid_pspace'_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def)
1049  apply (drule_tac x=d in spec)
1050  apply (drule_tac x=p in spec)
1051  apply (clarsimp)
1052  apply (drule(1) bspec)
1053  apply (erule obj_at'_weakenE)
1054  apply (simp)
1055  done
1056
1057lemma queued_vs_state[wp]:
1058  "\<lbrace>ct_in_state' st\<rbrace> threadSet (tcbQueued_update x) t \<lbrace>\<lambda>rv. ct_in_state' st\<rbrace>"
1059  apply (rule hoare_vcg_precond_imp)
1060   apply (rule hoare_post_imp[where Q="\<lambda>rv s. \<exists>t. t = ksCurThread s \<and> st_tcb_at' st t s"])
1061    apply (simp add: ct_in_state'_def)
1062   apply (unfold pred_tcb_at'_def)
1063   apply (wp hoare_ex_wp threadSet_ct)
1064  apply (simp add: ct_in_state'_def pred_tcb_at'_def)
1065  done
1066
1067lemma threadSet_timeslice_invs:
1068  "\<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbTimeSlice_update b) t \<lbrace>\<lambda>rv. invs'\<rbrace>"
1069  by (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong)
1070
1071lemma setCurThread_invs_no_cicd':
1072  "\<lbrace>invs_no_cicd' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace>
1073     setCurThread t
1074   \<lbrace>\<lambda>rv. invs'\<rbrace>"
1075proof -
1076  have obj_at'_ct: "\<And>f P addr s.
1077       obj_at' P addr (ksCurThread_update f s) = obj_at' P addr s"
1078    by (fastforce intro: obj_at'_pspaceI)
1079  have valid_pspace'_ct: "\<And>s f.
1080       valid_pspace' (ksCurThread_update f s) = valid_pspace' s"
1081    by (rule valid_pspace'_ksPSpace, simp)
1082  have vms'_ct: "\<And>s f.
1083       valid_machine_state' (ksCurThread_update f s) = valid_machine_state' s"
1084    by (simp add: valid_machine_state'_def)
1085  have ct_not_inQ_ct: "\<And>s t . \<lbrakk> ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr> ksCurThread := t \<rparr>)"
1086    apply (simp add: ct_not_inQ_def o_def)
1087    done
1088  have tcb_in_cur_domain_ct: "\<And>s f t.
1089       tcb_in_cur_domain' t  (ksCurThread_update f s)= tcb_in_cur_domain' t s"
1090    by (fastforce simp: tcb_in_cur_domain'_def)
1091  show ?thesis
1092    apply (simp add: setCurThread_def)
1093    apply wp
1094    apply (clarsimp simp add: all_invs_but_ct_idle_or_in_cur_domain'_def invs'_def cur_tcb'_def valid_state'_def obj_at'_ct
1095                              valid_pspace'_ct vms'_ct Invariants_H.valid_queues_def
1096                              sch_act_wf ct_in_state'_def state_refs_of'_def
1097                              ps_clear_def valid_irq_node'_def valid_queues'_def ct_not_inQ_ct
1098                              tcb_in_cur_domain_ct ct_idle_or_in_cur_domain'_def
1099                              bitmapQ_defs valid_queues_no_bitmap_def
1100                        cong: option.case_cong)
1101    done
1102qed
1103
1104(* Don't use this rule when considering the idle thread. The invariant ct_idle_or_in_cur_domain'
1105   says that either "tcb_in_cur_domain' t" or "t = ksIdleThread s".
1106   Use setCurThread_invs_idle_thread instead. *)
1107lemma setCurThread_invs:
1108  "\<lbrace>invs' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and
1109    tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>"
1110  by (rule hoare_pre, rule setCurThread_invs_no_cicd')
1111     (simp add: invs'_to_invs_no_cicd'_def)
1112
1113lemma valid_queues_not_runnable_not_queued:
1114  fixes s
1115  assumes vq:  "Invariants_H.valid_queues s"
1116      and vq': "valid_queues' s"
1117      and st: "st_tcb_at' (Not \<circ> runnable') t s"
1118  shows "obj_at' (Not \<circ> tcbQueued) t s"
1119proof (rule ccontr)
1120  assume "\<not> obj_at' (Not \<circ> tcbQueued) t s"
1121  moreover from st have "typ_at' TCBT t s"
1122    by (rule pred_tcb_at' [THEN tcb_at_typ_at' [THEN iffD1]])
1123  ultimately have "obj_at' tcbQueued t s"
1124    by (clarsimp simp: not_obj_at' comp_def)
1125
1126  moreover
1127  from st [THEN pred_tcb_at', THEN tcb_at'_has_tcbPriority]
1128  obtain p where tp: "obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s"
1129    by clarsimp
1130
1131  moreover
1132  from st [THEN pred_tcb_at', THEN tcb_at'_has_tcbDomain]
1133  obtain d where td: "obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
1134    by clarsimp
1135
1136  ultimately
1137  have "t \<in> set (ksReadyQueues s (d, p))" using vq'
1138    unfolding valid_queues'_def
1139    apply -
1140    apply (drule_tac x=d in spec)
1141    apply (drule_tac x=p in spec)
1142    apply (drule_tac x=t in spec)
1143    apply (erule impE)
1144     apply (fastforce simp add: inQ_def obj_at'_def)
1145    apply (assumption)
1146    done
1147
1148  with vq have "st_tcb_at' runnable' t s"
1149    unfolding Invariants_H.valid_queues_def valid_queues_no_bitmap_def
1150    apply -
1151    apply clarsimp
1152    apply (drule_tac x=d in spec)
1153    apply (drule_tac x=p in spec)
1154    apply (clarsimp simp add: st_tcb_at'_def)
1155    apply (drule(1) bspec)
1156    apply (erule obj_at'_weakenE)
1157    apply (clarsimp)
1158    done
1159
1160  with st show False
1161    apply -
1162    apply (drule(1) pred_tcb_at_conj')
1163    apply (clarsimp)
1164    done
1165qed
1166
1167(*
1168 * The idle thread is not part of any ready queues.
1169 *)
1170lemma idle'_not_tcbQueued':
1171 assumes vq:   "Invariants_H.valid_queues s"
1172     and vq':  "valid_queues' s"
1173     and idle: "valid_idle' s"
1174 shows "obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s"
1175 proof -
1176   from idle have stidle: "st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s"
1177     by (clarsimp simp add: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs)
1178
1179   with vq vq' show ?thesis
1180     by (rule valid_queues_not_runnable_not_queued)
1181 qed
1182
1183lemma idle'_not_tcbQueued:
1184 assumes "invs' s"
1185 shows "obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s"
1186  by (insert assms)
1187     (clarsimp simp: invs'_def valid_state'_def
1188              elim!: idle'_not_tcbQueued')
1189
1190lemma setCurThread_invs_no_cicd'_idle_thread:
1191  "\<lbrace>invs_no_cicd' and (\<lambda>s. t = ksIdleThread s) \<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>"
1192proof -
1193  have vms'_ct: "\<And>s f.
1194       valid_machine_state' (ksCurThread_update f s) = valid_machine_state' s"
1195    by (simp add: valid_machine_state'_def)
1196  have ct_not_inQ_ct: "\<And>s t . \<lbrakk> ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr> ksCurThread := t \<rparr>)"
1197    apply (simp add: ct_not_inQ_def o_def)
1198    done
1199  have idle'_activatable': "\<And> s t. st_tcb_at' idle' t s \<Longrightarrow> st_tcb_at' activatable' t s"
1200    apply (clarsimp simp: st_tcb_at'_def o_def obj_at'_def)
1201  done
1202  show ?thesis
1203    apply (simp add: setCurThread_def)
1204    apply wp
1205    apply (clarsimp simp add: vms'_ct ct_not_inQ_ct idle'_activatable' idle'_not_tcbQueued'[simplified o_def]
1206                              invs'_def cur_tcb'_def valid_state'_def valid_idle'_def
1207                              sch_act_wf ct_in_state'_def state_refs_of'_def
1208                              ps_clear_def valid_irq_node'_def
1209                              ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
1210                              valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def valid_queues'_def
1211                              all_invs_but_ct_idle_or_in_cur_domain'_def pred_tcb_at'_def
1212                        cong: option.case_cong)
1213    apply (clarsimp simp: obj_at'_def projectKOs)
1214    done
1215qed
1216
1217lemma setCurThread_invs_idle_thread:
1218  "\<lbrace>invs' and (\<lambda>s. t = ksIdleThread s) \<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>"
1219  by (rule hoare_pre, rule setCurThread_invs_no_cicd'_idle_thread)
1220     (clarsimp simp: invs'_to_invs_no_cicd'_def all_invs_but_ct_idle_or_in_cur_domain'_def)
1221
1222lemma Arch_switchToThread_invs[wp]:
1223  "\<lbrace>invs' and tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace>"
1224  apply (simp add: X64_H.switchToThread_def)
1225  apply (wp; auto)
1226  done
1227
1228lemma Arch_switchToThread_tcb'[wp]:
1229  "\<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>"
1230  apply (simp add: X64_H.switchToThread_def)
1231  apply (wp doMachineOp_obj_at hoare_drop_imps)+
1232  done
1233
1234crunch ksCurDomain[wp]: "Arch.switchToThread" "\<lambda>s. P (ksCurDomain s)"
1235(simp: crunch_simps)
1236
1237lemma Arch_swichToThread_tcbDomain_triv[wp]:
1238  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at'  (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>"
1239  apply (clarsimp simp: X64_H.switchToThread_def storeWordUser_def)
1240  apply (wp hoare_drop_imp | simp)+
1241  done
1242
1243lemma Arch_swichToThread_tcbPriority_triv[wp]:
1244  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at'  (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>"
1245  apply (clarsimp simp: X64_H.switchToThread_def storeWordUser_def)
1246  apply (wp hoare_drop_imp | simp)+
1247  done
1248
1249lemma Arch_switchToThread_tcb_in_cur_domain'[wp]:
1250  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>"
1251  apply (rule tcb_in_cur_domain'_lift)
1252   apply wp+
1253  done
1254
1255lemma tcbSchedDequeue_not_tcbQueued:
1256  "\<lbrace> tcb_at' t \<rbrace> tcbSchedDequeue t \<lbrace> \<lambda>_. obj_at' (\<lambda>x. \<not> tcbQueued x) t \<rbrace>"
1257  apply (simp add: tcbSchedDequeue_def)
1258  apply (wp|clarsimp)+
1259  apply (rule_tac Q="\<lambda>queued. obj_at' (\<lambda>x. tcbQueued x = queued) t" in hoare_post_imp)
1260   apply (clarsimp simp: obj_at'_def)
1261  apply (wp threadGet_obj_at')
1262  apply (simp)
1263  done
1264
1265lemma asUser_obj_at[wp]:  "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace>
1266   asUser t' f
1267   \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace>"
1268  apply (simp add: asUser_def threadGet_stateAssert_gets_asUser)
1269  apply (wp|wpc)+
1270  apply (simp add: asUser_fetch_def obj_at'_def)
1271  done
1272
1273lemma Arch_switchToThread_obj_at[wp]:
1274  "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace>
1275   Arch.switchToThread t
1276   \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace>"
1277  apply (simp add: X64_H.switchToThread_def )
1278  apply (rule setVMRoot_obj_at)
1279  done
1280
1281declare doMachineOp_obj_at[wp]
1282
1283crunch valid_arch_state'[wp]: asUser "valid_arch_state'"
1284(wp: crunch_wps simp: crunch_simps)
1285
1286crunch valid_irq_states'[wp]: asUser "valid_irq_states'"
1287(wp: crunch_wps simp: crunch_simps)
1288
1289crunch valid_machine_state'[wp]: asUser "valid_machine_state'"
1290(wp: crunch_wps simp: crunch_simps)
1291
1292crunch valid_queues'[wp]: asUser "valid_queues'"
1293(wp: crunch_wps simp: crunch_simps)
1294
1295
1296lemma asUser_valid_irq_node'[wp]:
1297  "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s\<rbrace> asUser t (setRegister f r)
1298          \<lbrace>\<lambda>_ s. valid_irq_node' (irq_node' s) s\<rbrace>"
1299  apply (rule_tac valid_irq_node_lift)
1300   apply (simp add: asUser_def)
1301   apply (wpsimp wp: crunch_wps)+
1302  done
1303
1304crunch irq_masked'_helper: asUser "\<lambda>s. P (intStateIRQTable (ksInterruptState s))"
1305(wp: crunch_wps simp: crunch_simps)
1306
1307lemma asUser_irq_masked'[wp]:
1308  "\<lbrace>irqs_masked'\<rbrace> asUser t (setRegister f r)
1309          \<lbrace>\<lambda>_ . irqs_masked'\<rbrace>"
1310  apply (rule irqs_masked_lift)
1311  apply (rule asUser_irq_masked'_helper)
1312  done
1313
1314lemma asUser_ct_not_inQ[wp]:
1315  "\<lbrace>ct_not_inQ\<rbrace> asUser t (setRegister f r)
1316          \<lbrace>\<lambda>_ . ct_not_inQ\<rbrace>"
1317  apply (clarsimp simp: submonad_asUser.fn_is_sm submonad_fn_def)
1318  apply (rule hoare_seq_ext)+
1319     prefer 4
1320     apply (rule stateAssert_sp)
1321    prefer 3
1322    apply (rule gets_inv)
1323   defer
1324   apply (rule select_f_inv)
1325   apply (case_tac x; simp)
1326  apply (clarsimp simp: projectKOs asUser_replace_def obj_at'_def fun_upd_def
1327          split: option.split kernel_object.split)
1328  apply wp
1329  apply (clarsimp simp: ct_not_inQ_def obj_at'_def projectKOs objBitsKO_def  ps_clear_def dom_def)
1330  apply (rule conjI; clarsimp; blast)
1331  done
1332
1333crunch pspace_domain_valid[wp]: asUser "pspace_domain_valid"
1334(wp: crunch_wps simp: crunch_simps)
1335
1336crunch valid_dom_schedule'[wp]: asUser "valid_dom_schedule'"
1337(wp: crunch_wps simp: crunch_simps)
1338
1339crunch gsUntypedZeroRanges[wp]: asUser "\<lambda>s. P (gsUntypedZeroRanges s)"
1340  (wp: crunch_wps simp: unless_def)
1341
1342crunch ctes_of[wp]: asUser "\<lambda>s. P (ctes_of s)"
1343  (wp: crunch_wps simp: unless_def)
1344
1345lemmas asUser_cteCaps_of[wp] = cteCaps_of_ctes_of_lift[OF asUser_ctes_of]
1346
1347lemma asUser_utr[wp]:
1348  "\<lbrace>untyped_ranges_zero'\<rbrace> asUser f t \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace>"
1349  apply (simp add: cteCaps_of_def)
1350  apply (rule hoare_pre, wp untyped_ranges_zero_lift)
1351  apply (simp add: o_def)
1352  done
1353
1354lemma asUser_ioports'[wp]:
1355  "\<lbrace>valid_ioports'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_ioports'\<rbrace>"
1356  apply (simp add: asUser_def split_def)
1357  apply (wpsimp wp: valid_ioports_lift'' select_f_inv threadSet_ctes_of)
1358  done
1359
1360lemma asUser_invs_no_cicd'[wp]:
1361  "\<lbrace>invs_no_cicd'\<rbrace> asUser t (setRegister f r) \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
1362  apply (simp add: invs_no_cicd'_def)
1363  apply (rule hoare_pre)
1364  apply  (wpc | wp asUser_global_refs' asUser_irq_handlers')+
1365  apply (rule hoare_post_imp[rotated])
1366   apply (rule hoare_vcg_conj_lift)
1367     apply (rule asUser_valid_dom_schedule')
1368    apply (rule asUser_utr)
1369   apply clarsimp
1370  apply clarsimp
1371  done
1372
1373
1374lemma Arch_switchToThread_invs_no_cicd':
1375  "\<lbrace>invs_no_cicd'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
1376  apply (simp add: X64_H.switchToThread_def)
1377  by (wp|rule setVMRoot_invs_no_cicd')+
1378
1379lemma tcbSchedDequeue_invs_no_cicd'[wp]:
1380  "\<lbrace>invs_no_cicd' and tcb_at' t\<rbrace>
1381     tcbSchedDequeue t
1382   \<lbrace>\<lambda>_. invs_no_cicd'\<rbrace>"
1383  unfolding all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def
1384  apply (wp tcbSchedDequeue_ct_not_inQ sch_act_wf_lift valid_irq_node_lift irqs_masked_lift
1385            valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
1386            tcbSchedDequeue_valid_queues_weak
1387            untyped_ranges_zero_lift
1388        | simp add: cteCaps_of_def o_def)+
1389  apply clarsimp
1390  apply (fastforce simp: valid_pspace'_def valid_queues_def
1391                   elim: valid_objs'_maxDomain valid_objs'_maxPriority intro: obj_at'_conjI)
1392  done
1393
1394lemma switchToThread_invs_no_cicd':
1395  "\<lbrace>invs_no_cicd' and st_tcb_at' runnable' t and tcb_in_cur_domain' t \<rbrace> ThreadDecls_H.switchToThread t \<lbrace>\<lambda>rv. invs' \<rbrace>"
1396  apply (simp add: Thread_H.switchToThread_def)
1397  apply (wp setCurThread_invs_no_cicd' tcbSchedDequeue_not_tcbQueued
1398            Arch_switchToThread_invs_no_cicd' Arch_switchToThread_pred_tcb')
1399  apply (auto elim!: pred_tcb'_weakenE)
1400  done
1401
1402lemma switchToThread_invs[wp]:
1403  "\<lbrace>invs' and st_tcb_at' runnable' t and tcb_in_cur_domain' t \<rbrace> switchToThread t \<lbrace>\<lambda>rv. invs' \<rbrace>"
1404  apply (simp add: Thread_H.switchToThread_def )
1405  apply (wp threadSet_timeslice_invs setCurThread_invs
1406             Arch_switchToThread_invs dmo_invs'
1407             doMachineOp_obj_at tcbSchedDequeue_not_tcbQueued)
1408  by (auto elim!: pred_tcb'_weakenE)
1409
1410lemma setCurThread_ct_in_state:
1411  "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>"
1412proof -
1413  have obj_at'_ct: "\<And>P addr f s.
1414       obj_at' P addr (ksCurThread_update f s) = obj_at' P addr s"
1415    by (fastforce intro: obj_at'_pspaceI)
1416  show ?thesis
1417    apply (simp add: setCurThread_def)
1418    apply wp
1419    apply (simp add: ct_in_state'_def pred_tcb_at'_def obj_at'_ct o_def)
1420    done
1421qed
1422
1423lemma switchToThread_ct_in_state[wp]:
1424  "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> switchToThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>"
1425proof -
1426  have P: "\<And>f x. tcbState (tcbTimeSlice_update f x) = tcbState x"
1427    by (case_tac x, simp)
1428  show ?thesis
1429    apply (simp add: Thread_H.switchToThread_def tcbSchedEnqueue_def unless_def)
1430    apply (wp setCurThread_ct_in_state Arch_switchToThread_obj_at
1431         | simp add: P o_def cong: if_cong)+
1432    done
1433qed
1434
1435lemma setCurThread_obj_at[wp]:
1436  "\<lbrace>obj_at' P addr\<rbrace> setCurThread t \<lbrace>\<lambda>rv. obj_at' P addr\<rbrace>"
1437  apply (simp add: setCurThread_def)
1438  apply wp
1439  apply (fastforce intro: obj_at'_pspaceI)
1440  done
1441
1442lemma switchToThread_tcb'[wp]:
1443  "\<lbrace>tcb_at' t\<rbrace> switchToThread t \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>"
1444  apply (simp add: Thread_H.switchToThread_def when_def)
1445  apply wp
1446  done
1447
1448crunch cap_to'[wp]: setQueue "ex_nonz_cap_to' p"
1449
1450lemma dmo_cap_to'[wp]:
1451  "\<lbrace>ex_nonz_cap_to' p\<rbrace>
1452     doMachineOp m
1453   \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>"
1454  by (wp ex_nonz_cap_to_pres')
1455
1456lemma sct_cap_to'[wp]:
1457  "\<lbrace>ex_nonz_cap_to' p\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>"
1458  apply (simp add: setCurThread_def)
1459  apply (wp ex_nonz_cap_to_pres')
1460   apply (clarsimp elim!: cte_wp_at'_pspaceI)+
1461  done
1462
1463
1464crunch cap_to'[wp]: "Arch.switchToThread" "ex_nonz_cap_to' p"
1465  (simp: crunch_simps)
1466
1467crunch cap_to'[wp]: switchToThread "ex_nonz_cap_to' p"
1468  (simp: crunch_simps)
1469
1470lemma no_longer_inQ[simp]:
1471  "\<not> inQ d p (tcbQueued_update (\<lambda>x. False) tcb)"
1472  by (simp add: inQ_def)
1473
1474lemma rq_distinct:
1475  "invs' s \<Longrightarrow> distinct (ksReadyQueues s (d, p))"
1476  by (clarsimp simp: invs'_def valid_state'_def Invariants_H.valid_queues_def
1477                     valid_queues_no_bitmap_def)
1478
1479lemma iflive_inQ_nonz_cap_strg:
1480  "if_live_then_nonz_cap' s \<and> obj_at' (inQ d prio) t s
1481          \<longrightarrow> ex_nonz_cap_to' t s"
1482  by (clarsimp simp: obj_at'_real_def projectKOs inQ_def
1483              elim!: if_live_then_nonz_capE' ko_wp_at'_weakenE)
1484
1485lemmas iflive_inQ_nonz_cap[elim]
1486    = mp [OF iflive_inQ_nonz_cap_strg, OF conjI[rotated]]
1487
1488crunch ksRQ[wp]: threadSet "\<lambda>s. P (ksReadyQueues s)"
1489  (ignore: setObject getObject
1490       wp: updateObject_default_inv)
1491
1492declare Cons_eq_tails[simp]
1493
1494lemma invs_ksReadyQueues_update_triv:
1495  assumes a: "\<forall>d p. set (f (ksReadyQueues s) (d,p)) = set (ksReadyQueues s (d,p))"
1496  assumes b: "\<forall>d p. distinct (f (ksReadyQueues s) (d,p)) = distinct (ksReadyQueues s (d,p))"
1497  assumes c: "\<forall>d p. (d > maxDomain \<or> p > maxPriority \<longrightarrow>
1498                       (f (ksReadyQueues s) (d,p) = [])) = (d > maxDomain \<or> p > maxPriority \<longrightarrow>
1499                         (ksReadyQueues s (d,p) = []))"
1500  shows "invs' (ksReadyQueues_update f s) = invs' s"
1501
1502proof -
1503  have orphans:
1504    "bitmapQ_no_L1_orphans (ksReadyQueues_update f s) = bitmapQ_no_L1_orphans s"
1505    "bitmapQ_no_L2_orphans (ksReadyQueues_update f s) = bitmapQ_no_L2_orphans s"
1506    using a b c unfolding bitmapQ_no_L2_orphans_def bitmapQ_no_L1_orphans_def by auto
1507
1508  have bitmapQ:
1509    "valid_bitmapQ (ksReadyQueues_update f s) = valid_bitmapQ s"
1510    using a b c
1511    unfolding valid_bitmapQ_def
1512    by (simp add: orphans bitmapQ_def set_empty[symmetric] del: set_empty)
1513
1514  show ?thesis
1515  unfolding invs'_def valid_state'_def ct_not_inQ_def valid_irq_node'_def cur_tcb'_def
1516                     Invariants_H.valid_queues_def valid_queues'_def valid_queues_no_bitmap_def
1517                     ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
1518  using a b c
1519  by (clarsimp simp: cur_tcb'_def orphans bitmapQ)
1520qed
1521
1522lemma tcbSchedDequeue_ksReadyQueues_eq:
1523  "\<lbrace>\<lambda>s. obj_at' (inQ d p) t s \<and> filter ((\<noteq>) t) (ksReadyQueues s (d, p)) = ts\<rbrace>
1524      tcbSchedDequeue t
1525   \<lbrace>\<lambda>rv s. ksReadyQueues s (d, p) = ts\<rbrace>"
1526  apply (simp add: tcbSchedDequeue_def threadGet_def liftM_def)
1527  apply (wp getObject_tcb_wp|clarsimp)+
1528  apply (clarsimp simp: obj_at'_def projectKOs inQ_def split del: if_split)
1529  apply (simp add: eq_commute)
1530  apply (rule_tac x=obj in exI, clarsimp)+
1531  done
1532
1533lemma hd_ksReadyQueues_runnable:
1534  "\<lbrakk>invs' s; ksReadyQueues s (d, p) = a # as\<rbrakk>
1535     \<Longrightarrow> st_tcb_at' runnable' a s"
1536  apply(simp add: invs'_def valid_state'_def, rule valid_queues_running, clarsimp)
1537   apply(rule suffix_Cons_mem)
1538   apply(simp add: suffix_def)
1539   apply(rule exI)
1540   apply(rule eq_Nil_appendI)
1541   by auto
1542
1543lemma chooseThread_invs_fragment: "\<lbrace>invs' and (\<lambda>s. ksCurDomain s = d)\<rbrace>
1544       do x \<leftarrow> getQueue d r;
1545        (case x of [] \<Rightarrow> return False
1546          | thread # x \<Rightarrow> do y \<leftarrow> ThreadDecls_H.switchToThread thread; return True od)
1547       od
1548       \<lbrace>\<lambda>_. invs'\<rbrace>"
1549  apply (rule seq_ext)
1550   apply (rule gq_sp)
1551  apply (case_tac x)
1552   apply (simp)
1553   apply (wp)
1554   apply (clarsimp)
1555  apply (simp)
1556  apply (wp)
1557  apply (clarsimp simp: invs'_def valid_state'_def , rule conjI)
1558   apply (rule valid_queues_running)
1559    apply (rule suffix_Cons_mem)
1560    apply (simp add: suffix_def)
1561    apply (rule exI)
1562    apply (rule eq_Nil_appendI)
1563    apply simp+
1564  apply (clarsimp simp add: tcb_in_cur_domain'_def valid_queues_def valid_queues_no_bitmap_def)
1565  apply (drule_tac x="ksCurDomain s" in spec)
1566  apply (drule_tac x=r in spec)
1567  apply (fastforce simp: obj_at'_def inQ_def)
1568  done
1569
1570crunch ksCurDomain[wp]: "ThreadDecls_H.switchToThread" "\<lambda>s. P (ksCurDomain s)"
1571
1572lemma chooseThread_ksCurDomain_fragment:
1573  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace>
1574       do x \<leftarrow> getQueue d r;
1575        (case x of [] \<Rightarrow> return False
1576          | thread # x \<Rightarrow> do y \<leftarrow> ThreadDecls_H.switchToThread thread; return True od)
1577       od
1578   \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>"
1579  apply (wp | wpc | clarsimp)+
1580  done
1581
1582(* FIXME move *)
1583lemma obj_tcb_at':
1584  "obj_at' (\<lambda>tcb::tcb. P tcb) t s \<Longrightarrow> tcb_at' t s"
1585  by (clarsimp simp: obj_at'_def)
1586
1587lemma valid_queues_queued_runnable:
1588  fixes s
1589  assumes vq:  "Invariants_H.valid_queues s"
1590      and vq': "valid_queues' s"
1591      and oa:  "obj_at' tcbQueued t s"
1592  shows "st_tcb_at' runnable' t s"
1593proof -
1594  from oa [THEN obj_tcb_at', THEN tcb_at'_has_tcbPriority]
1595  obtain p where tp: "obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s"
1596    by clarsimp
1597
1598  from oa [THEN obj_tcb_at', THEN tcb_at'_has_tcbDomain]
1599  obtain d where td: "obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
1600    by clarsimp
1601
1602  with oa tp have "obj_at' (inQ d p) t s"
1603    by (fastforce simp add: inQ_def obj_at'_def)
1604
1605  with vq' have "t \<in> set (ksReadyQueues s (d, p))"
1606    unfolding valid_queues'_def
1607    by (fastforce)
1608
1609  with vq show ?thesis
1610    unfolding Invariants_H.valid_queues_def valid_queues_no_bitmap_def
1611    apply -
1612    apply clarify
1613    apply (drule_tac x=d in spec)
1614    apply (drule_tac x=p in spec)
1615    apply (clarsimp simp: pred_tcb_at'_def)
1616    apply (drule(1) bspec)
1617    apply (erule obj_at'_weakenE)
1618    apply (simp)
1619    done
1620qed
1621
1622lemma tcb_at_typ_at':
1623  "tcb_at' p s = typ_at' TCBT p s"
1624  unfolding typ_at'_def
1625  apply rule
1626  apply (clarsimp simp add: obj_at'_def ko_wp_at'_def projectKOs)
1627  apply (clarsimp simp add: obj_at'_def ko_wp_at'_def projectKOs)
1628  apply (case_tac ko, simp_all)
1629  done
1630
1631
1632lemma invs'_not_runnable_not_queued:
1633  fixes s
1634  assumes inv: "invs' s"
1635      and st: "st_tcb_at' (Not \<circ> runnable') t s"
1636  shows "obj_at' (Not \<circ> tcbQueued) t s"
1637  apply (insert assms)
1638  apply (rule valid_queues_not_runnable_not_queued)
1639    apply (clarsimp simp add: invs'_def valid_state'_def)+
1640  done
1641
1642lemma valid_queues_not_tcbQueued_not_ksQ:
1643  fixes s
1644  assumes   vq: "Invariants_H.valid_queues s"
1645      and notq: "obj_at' (Not \<circ> tcbQueued) t s"
1646  shows "\<forall>d p. t \<notin> set (ksReadyQueues s (d, p))"
1647proof (rule ccontr, simp , erule exE, erule exE)
1648  fix d p
1649  assume "t \<in> set (ksReadyQueues s (d, p))"
1650  with vq have "obj_at' (inQ d p) t s"
1651    unfolding Invariants_H.valid_queues_def valid_queues_no_bitmap_def
1652    apply clarify
1653    apply (drule_tac x=d in spec)
1654    apply (drule_tac x=p in spec)
1655    apply (clarsimp)
1656    apply (drule(1) bspec)
1657    apply (erule obj_at'_weakenE)
1658    apply (simp)
1659    done
1660  hence "obj_at' tcbQueued t s"
1661    apply (rule obj_at'_weakenE)
1662    apply (simp only: inQ_def)
1663    done
1664  with notq show "False"
1665    by (clarsimp simp: obj_at'_def)
1666qed
1667
1668lemma not_tcbQueued_not_ksQ:
1669  fixes s
1670  assumes "invs' s"
1671      and "obj_at' (Not \<circ> tcbQueued) t s"
1672  shows "\<forall>d p. t \<notin> set (ksReadyQueues s (d, p))"
1673  apply (insert assms)
1674  apply (clarsimp simp add: invs'_def valid_state'_def)
1675  apply (drule(1) valid_queues_not_tcbQueued_not_ksQ)
1676  apply (clarsimp)
1677  done
1678
1679lemma ct_not_ksQ:
1680  "\<lbrakk> invs' s; ksSchedulerAction s = ResumeCurrentThread \<rbrakk>
1681   \<Longrightarrow> \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)"
1682  apply (clarsimp simp: invs'_def valid_state'_def ct_not_inQ_def)
1683  apply (frule(1) valid_queues_not_tcbQueued_not_ksQ)
1684  apply (fastforce)
1685  done
1686
1687crunch nosch[wp]: getCurThread "\<lambda>s. P (ksSchedulerAction s)"
1688
1689lemma setThreadState_rct:
1690  "\<lbrace>\<lambda>s. (runnable' st \<or> ksCurThread s \<noteq> t)
1691        \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace>
1692   setThreadState st t
1693   \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>"
1694  apply (simp add: setThreadState_def)
1695  apply (rule hoare_pre_disj')
1696   apply (rule hoare_seq_ext [OF _
1697                 hoare_vcg_conj_lift
1698                   [OF threadSet_tcbState_st_tcb_at' [where P=runnable']
1699                       threadSet_nosch]])
1700   apply (rule hoare_seq_ext [OF _
1701                 hoare_vcg_conj_lift [OF isRunnable_const isRunnable_inv]])
1702   apply (clarsimp simp: when_def)
1703   apply (case_tac x)
1704    apply (clarsimp, wp)[1]
1705   apply (clarsimp)
1706  apply (rule hoare_seq_ext [OF _
1707                hoare_vcg_conj_lift
1708                  [OF threadSet_ct threadSet_nosch]])
1709  apply (rule hoare_seq_ext [OF _ isRunnable_inv])
1710  apply (rule hoare_seq_ext [OF _
1711                hoare_vcg_conj_lift
1712                  [OF gct_wp gct_wp]])
1713  apply (rename_tac ct)
1714  apply (case_tac "ct\<noteq>t")
1715   apply (clarsimp simp: when_def)
1716   apply (wp)[1]
1717  apply (clarsimp)
1718  done
1719
1720lemma switchToIdleThread_invs'[wp]:
1721  "\<lbrace>invs'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace>"
1722  apply (clarsimp simp: Thread_H.switchToIdleThread_def X64_H.switchToIdleThread_def)
1723  apply (wp setCurThread_invs_idle_thread)
1724  apply clarsimp
1725
1726  done
1727
1728lemma bitmapQ_lookupBitmapPriority_simp: (* neater unfold, actual unfold is really ugly *)
1729  "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ;
1730     valid_bitmapQ s ; bitmapQ_no_L1_orphans s \<rbrakk> \<Longrightarrow>
1731   bitmapQ d (lookupBitmapPriority d s) s =
1732    (ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d) \<and>
1733     ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !!
1734       word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))"
1735  unfolding bitmapQ_def lookupBitmapPriority_def
1736  apply (drule word_log2_nth_same, clarsimp)
1737  apply (drule (1) bitmapQ_no_L1_orphansD, clarsimp)
1738  apply (drule word_log2_nth_same, clarsimp)
1739  apply (frule test_bit_size[where n="word_log2 (ksReadyQueuesL2Bitmap _ _)"])
1740  apply (clarsimp simp: numPriorities_def wordBits_def word_size)
1741  apply (subst prioToL1Index_l1IndexToPrio_or_id)
1742    apply (simp add: wordRadix_def' unat_of_nat word_size)
1743   apply (simp add: wordRadix_def' unat_of_nat word_size l2BitmapSize_def')
1744  apply (subst prioToL1Index_l1IndexToPrio_or_id)
1745    apply (simp add: wordRadix_def' unat_of_nat word_size)
1746   apply (simp add: wordRadix_def' unat_of_nat word_size l2BitmapSize_def')
1747  apply (simp add: word_ao_dist)
1748  apply (subst less_mask_eq)
1749   apply (fastforce intro: word_of_nat_less simp: wordRadix_def' unat_of_nat word_size)+
1750  done
1751
1752lemma bitmapQ_from_bitmap_lookup:
1753  "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ;
1754     valid_bitmapQ s ; bitmapQ_no_L1_orphans s
1755     \<rbrakk>
1756   \<Longrightarrow> bitmapQ d (lookupBitmapPriority d s) s"
1757  apply (simp add: bitmapQ_lookupBitmapPriority_simp)
1758  apply (drule word_log2_nth_same)
1759  apply (drule (1) bitmapQ_no_L1_orphansD)
1760  apply (fastforce dest!: word_log2_nth_same
1761                   simp: word_ao_dist lookupBitmapPriority_def word_size numPriorities_def
1762                         wordBits_def)
1763  done
1764
1765lemma lookupBitmapPriority_obj_at':
1766  "\<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; valid_queues_no_bitmap s; valid_bitmapQ s;
1767         bitmapQ_no_L1_orphans s\<rbrakk>
1768        \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState)
1769             (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s"
1770  apply (drule (2) bitmapQ_from_bitmap_lookup)
1771  apply (simp add: valid_bitmapQ_bitmapQ_simp)
1772  apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)", simp)
1773  apply (clarsimp, rename_tac t ts)
1774  apply (drule cons_set_intro)
1775  apply (drule (2) valid_queues_no_bitmap_objD)
1776  done
1777
1778lemma bitmapL1_zero_ksReadyQueues:
1779  "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s \<rbrakk>
1780   \<Longrightarrow> (ksReadyQueuesL1Bitmap s d = 0) = (\<forall>p. ksReadyQueues s (d,p) = [])"
1781  apply (cases "ksReadyQueuesL1Bitmap s d = 0")
1782   apply (force simp add: bitmapQ_def valid_bitmapQ_def)
1783  apply (fastforce dest: bitmapQ_from_bitmap_lookup simp: valid_bitmapQ_bitmapQ_simp)
1784  done
1785
1786lemma prioToL1Index_le_mask:
1787  "\<lbrakk> prioToL1Index p = prioToL1Index p' ; p && mask wordRadix \<le> p' && mask wordRadix \<rbrakk>
1788   \<Longrightarrow> p \<le> p'"
1789  unfolding prioToL1Index_def
1790  apply (simp add: wordRadix_def word_le_nat_alt[symmetric])
1791  apply (drule shiftr_eq_neg_mask_eq)
1792  apply (metis add.commute word_and_le2 word_plus_and_or_coroll2 word_plus_mono_left)
1793  done
1794
1795lemma prioToL1Index_le_index:
1796  "\<lbrakk> prioToL1Index p \<le> prioToL1Index p' ; prioToL1Index p \<noteq> prioToL1Index p' \<rbrakk>
1797   \<Longrightarrow> p \<le> p'"
1798  unfolding prioToL1Index_def
1799  apply (simp add: wordRadix_def word_le_nat_alt[symmetric])
1800  apply (erule (1) le_shiftr')
1801  done
1802
1803lemma bitmapL1_highest_lookup:
1804  "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ;
1805     bitmapQ d p' s \<rbrakk>
1806   \<Longrightarrow> p' \<le> lookupBitmapPriority d s"
1807  apply (subgoal_tac "ksReadyQueuesL1Bitmap s d \<noteq> 0")
1808   prefer 2
1809   apply (clarsimp simp add: bitmapQ_def)
1810  apply (case_tac "prioToL1Index (lookupBitmapPriority d s) = prioToL1Index p'")
1811   apply (rule prioToL1Index_le_mask, simp)
1812   apply (frule (2) bitmapQ_from_bitmap_lookup)
1813   apply (clarsimp simp: bitmapQ_lookupBitmapPriority_simp)
1814   apply (clarsimp simp: bitmapQ_def lookupBitmapPriority_def)
1815   apply (subst mask_or_not_mask[where n=wordRadix and x=p', symmetric])
1816   apply (subst word_bw_comms(2)) (* || commute *)
1817   apply (simp add: word_ao_dist mask_AND_NOT_mask mask_twice)
1818   apply (subst less_mask_eq[where x="of_nat _"])
1819    apply (subst word_less_nat_alt)
1820    apply (subst unat_of_nat_eq)
1821     apply (rule order_less_le_trans[OF word_log2_max])
1822     apply (simp add: word_size)
1823    apply (rule order_less_le_trans[OF word_log2_max])
1824    apply (simp add: word_size wordRadix_def')
1825   apply (subst word_le_nat_alt)
1826   apply (subst unat_of_nat_eq)
1827    apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size)
1828   apply (rule word_log2_highest)
1829   apply (subst (asm) prioToL1Index_l1IndexToPrio_or_id)
1830     apply (subst unat_of_nat_eq)
1831      apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size)
1832     apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def')
1833    apply (simp add: word_size wordRadix_def')
1834    apply (drule (1) bitmapQ_no_L1_orphansD[where d=d and i="word_log2 _"])
1835    apply (simp add: l2BitmapSize_def')
1836   apply simp
1837  apply (rule prioToL1Index_le_index[rotated], simp)
1838  apply (frule (2) bitmapQ_from_bitmap_lookup)
1839  apply (clarsimp simp: bitmapQ_lookupBitmapPriority_simp)
1840  apply (clarsimp simp: bitmapQ_def lookupBitmapPriority_def)
1841  apply (subst prioToL1Index_l1IndexToPrio_or_id)
1842    apply (subst unat_of_nat_eq)
1843     apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size)
1844    apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def')
1845   apply (fastforce dest: bitmapQ_no_L1_orphansD
1846                    simp: wordBits_def numPriorities_def word_size wordRadix_def' l2BitmapSize_def')
1847  apply (erule word_log2_highest)
1848  done
1849
1850lemma bitmapQ_ksReadyQueuesI:
1851  "\<lbrakk> bitmapQ d p s ; valid_bitmapQ s \<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p) \<noteq> []"
1852  unfolding valid_bitmapQ_def by simp
1853
1854lemma getReadyQueuesL2Bitmap_inv[wp]:
1855  "\<lbrace> P \<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>\<lambda>_. P\<rbrace>"
1856  unfolding getReadyQueuesL2Bitmap_def by wp
1857
1858lemma switchToThread_lookupBitmapPriority_wp:
1859  "\<lbrace>\<lambda>s. invs_no_cicd' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and>
1860        t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)) \<rbrace>
1861   ThreadDecls_H.switchToThread t
1862   \<lbrace>\<lambda>rv. invs'\<rbrace>"
1863proof -
1864  have switchToThread_pre:
1865    "\<And>s p t.\<lbrakk> valid_queues s ; bitmapQ (ksCurDomain s) p s ; t = hd (ksReadyQueues s (ksCurDomain s,p)) \<rbrakk>
1866            \<Longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s"
1867    unfolding valid_queues_def
1868    apply (clarsimp dest!: bitmapQ_ksReadyQueuesI)
1869    apply (case_tac "ksReadyQueues s (ksCurDomain s, p)", simp)
1870    apply (rename_tac t ts)
1871    apply (drule_tac t=t and p=p and d="ksCurDomain s" in valid_queues_no_bitmap_objD)
1872     apply simp
1873    apply (fastforce elim: obj_at'_weaken simp: inQ_def tcb_in_cur_domain'_def st_tcb_at'_def)
1874    done
1875  thus ?thesis
1876    by (wp switchToThread_invs_no_cicd') (fastforce dest: invs_no_cicd'_queues)
1877qed
1878
1879lemma switchToIdleThread_invs_no_cicd':
1880  "\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace>"
1881  apply (clarsimp simp: Thread_H.switchToIdleThread_def X64_H.switchToIdleThread_def)
1882  apply (wp setCurThread_invs_no_cicd'_idle_thread storeWordUser_invs_no_cicd'
1883            setVMRoot_invs_no_cicd')
1884  apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_idle'_def)
1885  done
1886
1887crunch obj_at'[wp]: "Arch.switchToIdleThread" "\<lambda>s. obj_at' P t s"
1888
1889
1890lemma switchToIdleThread_activatable[wp]:
1891  "\<lbrace>invs'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>"
1892  apply (simp add: Thread_H.switchToIdleThread_def
1893                   X64_H.switchToIdleThread_def)
1894  apply (wp setCurThread_ct_in_state)
1895  apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def
1896                        pred_tcb_at'_def obj_at'_def)
1897  done
1898
1899declare static_imp_conj_wp[wp_split del]
1900
1901lemma valid_queues_obj_at'_imp:
1902   "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); Invariants_H.valid_queues s; \<And>obj. runnable' obj \<Longrightarrow> P obj \<rbrakk>
1903        \<Longrightarrow> obj_at' (P \<circ> tcbState) t s"
1904  apply (clarsimp simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def o_def)
1905  apply(elim allE conjE)
1906  apply(rule obj_at'_weaken)
1907   apply(erule(1) ballE)
1908   apply(erule(1) notE)
1909  apply(clarsimp simp: obj_at'_def inQ_def)
1910done
1911
1912lemma setCurThread_const:
1913  "\<lbrace>\<lambda>_. P t \<rbrace> setCurThread t \<lbrace>\<lambda>_ s. P (ksCurThread s) \<rbrace>"
1914  by (simp add: setCurThread_def | wp)+
1915
1916
1917
1918crunch it[wp]: switchToIdleThread "\<lambda>s. P (ksIdleThread s)"
1919crunch it[wp]: switchToThread "\<lambda>s. P (ksIdleThread s)"
1920    (ignore: )
1921
1922lemma switchToIdleThread_curr_is_idle:
1923  "\<lbrace>\<top>\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s\<rbrace>"
1924  apply (rule hoare_weaken_pre)
1925   apply (wps switchToIdleThread_it)
1926   apply (simp add: Thread_H.switchToIdleThread_def)
1927   apply (wp setCurThread_const)
1928  apply (simp)
1929 done
1930
1931lemma chooseThread_it[wp]:
1932  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
1933  by (wp|clarsimp simp: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs|assumption)+
1934
1935lemma valid_queues_ct_update[simp]:
1936  "Invariants_H.valid_queues (s\<lparr>ksCurThread := t\<rparr>) = Invariants_H.valid_queues s"
1937  by (simp add: Invariants_H.valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def)
1938
1939lemma valid_queues'_ct_update[simp]:
1940  "valid_queues' (s\<lparr>ksCurThread := t\<rparr>) = valid_queues' s"
1941  by (simp add: valid_queues'_def)
1942
1943lemma valid_machine_state'_ct_update[simp]:
1944  "valid_machine_state' (s\<lparr>ksCurThread := t\<rparr>) = valid_machine_state' s"
1945  by (simp add: valid_machine_state'_def)
1946
1947lemma valid_irq_node'_ct_update[simp]:
1948  "valid_irq_node' w (s\<lparr>ksCurThread := t\<rparr>) = valid_irq_node' w s"
1949  by (simp add: valid_irq_node'_def)
1950
1951lemma switchToThread_ct_not_queued:
1952  "\<lbrace>invs' and tcb_at' t\<rbrace> switchToThread t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>"
1953  (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>")
1954  apply (simp add: Thread_H.switchToThread_def)
1955  apply (wp)
1956    apply (simp add: switchToThread_def setCurThread_def)
1957    apply (wp tcbSchedDequeue_not_tcbQueued | simp )+
1958  done
1959
1960lemma valid_irq_node'_ksCurThread: "valid_irq_node' w (s\<lparr>ksCurThread := t\<rparr>) = valid_irq_node' w s"
1961  unfolding valid_irq_node'_def
1962  by simp
1963
1964lemma threadGet_inv [wp]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>"
1965  apply (simp add: threadGet_def)
1966  apply (wp | simp)+
1967  done
1968
1969lemma getThreadState_ct_in_state:
1970  "\<lbrace>\<lambda>s. t = ksCurThread s \<and> tcb_at' t s\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. P rv \<longrightarrow> ct_in_state' P s\<rbrace>"
1971  apply (rule hoare_post_imp [where Q="\<lambda>rv s. t = ksCurThread s \<and> ((\<not> P rv) \<or> st_tcb_at' P t s)"])
1972   apply (clarsimp simp add: ct_in_state'_def)
1973  apply (rule hoare_vcg_precond_imp)
1974   apply (wp hoare_vcg_disj_lift)
1975  apply (clarsimp simp add: pred_tcb_at'_def obj_at'_def)
1976  done
1977
1978lemma gsa_wf_invs:
1979  "\<lbrace>invs'\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. invs' and sch_act_wf sa\<rbrace>"
1980  by wp (clarsimp simp add: invs'_def valid_state'_def)
1981
1982(* Helper for schedule_corres *)
1983lemma gsa_wf_invs_and_P:
1984  "\<lbrace>invs' and P\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. invs' and P
1985                                                and (\<lambda>s. ksSchedulerAction s = sa)
1986                                                and sch_act_wf sa\<rbrace>"
1987  apply ( wp |  simp )
1988  by auto
1989
1990lemma gets_the_simp:
1991  "f s = Some y \<Longrightarrow> gets_the f s = ({(y, s)}, False)"
1992  by (simp add: gets_the_def gets_def assert_opt_def get_def bind_def return_def fail_def split: option.splits)
1993
1994lemma corres_split_sched_act:
1995  "\<lbrakk>sched_act_relation act act';
1996    corres r P P' f1 g1;
1997    \<And>t. corres r (Q t) (Q' t) (f2 t) (g2 t);
1998    corres r R R' f3 g3\<rbrakk>
1999    \<Longrightarrow> corres r (case act of resume_cur_thread \<Rightarrow> P
2000                           | switch_thread t \<Rightarrow> Q t
2001                           | choose_new_thread \<Rightarrow> R)
2002               (case act' of ResumeCurrentThread \<Rightarrow> P'
2003                           | SwitchToThread t \<Rightarrow> Q' t
2004                           | ChooseThread \<Rightarrow> R')
2005       (case act of resume_cur_thread \<Rightarrow> f1
2006                  | switch_thread t \<Rightarrow> f2 t
2007                  | choose_new_thread \<Rightarrow> f3)
2008       (case act' of ResumeCurrentThread \<Rightarrow> g1
2009                   | ChooseNewThread \<Rightarrow> g3
2010                   | SwitchToThread t \<Rightarrow> g2 t)"
2011  apply (cases act)
2012    apply (rule corres_guard_imp, force+)+
2013    done
2014
2015lemma get_sa_corres':
2016  "corres sched_act_relation P P' (gets scheduler_action) getSchedulerAction"
2017  by (clarsimp simp: getSchedulerAction_def state_relation_def)
2018
2019lemma corres_assert_ret:
2020  "corres dc (\<lambda>s. P) \<top> (assert P) (return ())"
2021  apply (rule corres_no_failI)
2022   apply simp
2023  apply (simp add: assert_def return_def fail_def)
2024  done
2025
2026lemma corres_assert_assume_l:
2027  "corres dc P Q (f ()) g
2028  \<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
2029  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
2030
2031lemma corres_assert_assume_r:
2032  "corres dc P Q f (g ())
2033  \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"
2034  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
2035
2036lemma cur_tcb'_ksReadyQueuesL1Bitmap_upd[simp]:
2037  "cur_tcb' (s\<lparr>ksReadyQueuesL1Bitmap := x\<rparr>) = cur_tcb' s"
2038  unfolding cur_tcb'_def by simp
2039
2040lemma cur_tcb'_ksReadyQueuesL2Bitmap_upd[simp]:
2041  "cur_tcb' (s\<lparr>ksReadyQueuesL2Bitmap := x\<rparr>) = cur_tcb' s"
2042  unfolding cur_tcb'_def by simp
2043
2044crunch cur[wp]: tcbSchedEnqueue cur_tcb'
2045  (simp: unless_def)
2046
2047(* FIXME: move *)
2048lemma corres_noop3:
2049  assumes x: "\<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk>  \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
2050  assumes y: "\<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> g \<lbrace>\<lambda>r. (=) s'\<rbrace>"
2051  assumes z: "nf' \<Longrightarrow> no_fail P' g"
2052  shows      "corres_underlying sr nf nf' dc P P' f g"
2053  apply (clarsimp simp: corres_underlying_def)
2054  apply (rule conjI)
2055   apply clarsimp
2056   apply (rule use_exs_valid)
2057    apply (rule exs_hoare_post_imp)
2058     prefer 2
2059     apply (rule x)
2060       apply assumption+
2061    apply simp_all
2062   apply (subgoal_tac "ba = b")
2063    apply simp
2064   apply (rule sym)
2065   apply (rule use_valid[OF _ y], assumption+)
2066   apply simp
2067  apply (insert z)
2068  apply (clarsimp simp: no_fail_def)
2069  done
2070
2071lemma corres_symb_exec_l':
2072  assumes z: "\<And>rv. corres_underlying sr nf nf' r (Q' rv) P' (x rv) y"
2073  assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
2074  assumes y: "\<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>"
2075  shows      "corres_underlying sr nf nf' r (P and Q) P' (m >>= (\<lambda>rv. x rv)) y"
2076  apply (rule corres_guard_imp)
2077    apply (subst gets_bind_ign[symmetric], rule corres_split)
2078       apply (rule z)
2079      apply (rule corres_noop3)
2080        apply (erule x)
2081       apply (rule gets_wp)
2082      apply (rule non_fail_gets)
2083     apply (rule y)
2084    apply (rule gets_wp)
2085   apply simp+
2086   done
2087
2088lemma corres_symb_exec_r':
2089  assumes z: "\<And>rv. corres_underlying sr nf nf' r P (P'' rv) x (y rv)"
2090  assumes y: "\<lbrace>P'\<rbrace> m \<lbrace>P''\<rbrace>"
2091  assumes x: "\<And>s. Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
2092  assumes nf: "nf' \<Longrightarrow> no_fail R' m"
2093  shows      "corres_underlying sr nf nf' r P (P' and Q' and R') x (m >>= (\<lambda>rv. y rv))"
2094  apply (rule corres_guard_imp)
2095    apply (subst gets_bind_ign[symmetric], rule corres_split)
2096       apply (rule z)
2097      apply (rule_tac P'="a' and a''" for a' a'' in corres_noop3)
2098        apply (simp add: simpler_gets_def exs_valid_def)
2099       apply clarsimp
2100       apply (erule x)
2101      apply (rule no_fail_pre)
2102       apply (erule nf)
2103      apply clarsimp
2104      apply assumption
2105     apply (rule gets_wp)
2106    apply (rule y)
2107   apply simp+
2108  done
2109
2110lemma corres_case_list:
2111  "\<lbrakk>list = list'; corres r P P' f1 g1; \<And>x xs. corres r (Q x xs) (Q' x xs) (f2 x xs) (g2 x xs)\<rbrakk>
2112    \<Longrightarrow> corres r (case list of [] \<Rightarrow> P | x # xs \<Rightarrow> Q x xs)
2113                (case list' of [] \<Rightarrow> P' | x # xs \<Rightarrow> Q' x xs)
2114       (case list of [] \<Rightarrow> f1 | x # xs \<Rightarrow> f2 x xs)
2115       (case list' of [] \<Rightarrow> g1 | x # xs \<Rightarrow> g2 x xs)"
2116  apply (cases list)
2117   apply (rule corres_guard_imp, force+)+
2118   done
2119
2120lemma findM_corres:
2121  "\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> corres (=) P P' (f x) (f' x);
2122    \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>r. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P'\<rbrace> f' x \<lbrace>\<lambda>r. P'\<rbrace>\<rbrakk>
2123    \<Longrightarrow> corres (=) P P' (findM f xs) (findM f' xs)"
2124  apply (induct xs)
2125   apply simp
2126  apply simp
2127  apply (rule corres_guard_imp)
2128    apply (rule corres_split[where r'="(=)"])
2129       apply (rule corres_if[where P=P and P'=P'])
2130         apply simp
2131        apply simp
2132       apply force
2133      apply force
2134     apply (atomize, (erule_tac x=a in allE)+, force)+
2135     done
2136
2137lemma thread_get_exs_valid[wp]:
2138  "tcb_at t s \<Longrightarrow> \<lbrace>(=) s\<rbrace> thread_get f t \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
2139  apply (clarsimp simp: get_thread_state_def  assert_opt_def fail_def
2140             thread_get_def gets_the_def exs_valid_def gets_def
2141             get_def bind_def return_def split: option.splits)
2142  apply (erule get_tcb_at)
2143  done
2144
2145lemma gts_exs_valid[wp]:
2146  "tcb_at t s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_thread_state t \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
2147  apply (clarsimp simp: get_thread_state_def  assert_opt_def fail_def
2148             thread_get_def gets_the_def exs_valid_def gets_def
2149             get_def bind_def return_def split: option.splits)
2150  apply (erule get_tcb_at)
2151  done
2152
2153lemma guarded_switch_to_corres:
2154  "corres dc (valid_arch_state and valid_objs and valid_asid_map
2155                and valid_vspace_objs and pspace_aligned and pspace_distinct
2156                and valid_vs_lookup and valid_global_objs
2157                and unique_table_refs o caps_of_state
2158                and st_tcb_at runnable t and valid_etcbs)
2159             (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues
2160                and st_tcb_at' runnable' t and cur_tcb')
2161             (guarded_switch_to t) (switchToThread t)"
2162  apply (simp add: guarded_switch_to_def)
2163  apply (rule corres_guard_imp)
2164    apply (rule corres_symb_exec_l'[OF _ gts_exs_valid])
2165      apply (rule corres_assert_assume_l)
2166      apply (rule switch_thread_corres)
2167     apply (force simp: st_tcb_at_tcb_at)
2168    apply (wp gts_st_tcb_at)
2169    apply (force simp: st_tcb_at_tcb_at)+
2170    done
2171
2172 lemma findM_gets_outside:
2173   assumes terminate_False: "(\<And>s s' x. (False,s') \<in> fst (g x s) \<Longrightarrow> s = s')"
2174   shows
2175   "findM (\<lambda>x. gets (\<lambda>ks. f ks x) >>= g) l = do f' \<leftarrow> gets (\<lambda>ks. f ks); findM (\<lambda>x. (g (f' x))) l od"
2176   apply (rule ext)
2177   apply (induct l)
2178    apply (clarsimp simp add:  bind_def gets_def get_def return_def)
2179   apply simp
2180   apply (clarsimp simp add:  bind_def gets_def get_def return_def cong: if_cong split: if_split_asm)
2181   apply safe
2182      apply (clarsimp split: if_split_asm)
2183       apply force
2184      apply (frule terminate_False)
2185      apply simp
2186      apply (rule_tac x="(False,ba)" in bexI,clarsimp+)
2187     apply (clarsimp split: if_split_asm)+
2188      apply force
2189     apply (frule terminate_False)
2190     apply clarsimp
2191     apply (rule_tac x="(False,ba)" in bexI,clarsimp+)
2192    apply (clarsimp split: if_split_asm)+
2193    apply (frule terminate_False)
2194    apply clarsimp
2195    apply force
2196   apply (clarsimp split: if_split_asm)+
2197   apply (frule terminate_False)
2198   apply clarsimp
2199   apply (rule bexI [rotated], assumption)
2200   apply auto
2201   done
2202
2203lemma corres_gets_queues:
2204  "corres ready_queues_relation \<top> \<top> (gets ready_queues) (gets ksReadyQueues)"
2205  apply (simp add: state_relation_def)
2206  done
2207
2208lemma Max_lt_set: "\<forall>y\<in>A. Max B < (y::word8) \<Longrightarrow> \<forall>y\<in>A. y \<notin> B"
2209  apply clarsimp
2210  apply (drule_tac x=y in bspec,simp)
2211  apply (case_tac "B = {}")
2212  apply simp+
2213  apply blast
2214  done
2215
2216abbreviation "enumPrio \<equiv> [0.e.maxPriority]"
2217
2218lemma enumPrio_word_div:
2219  fixes v :: "8 word"
2220  assumes vlt: "unat v \<le> unat maxPriority"
2221  shows "\<exists>xs ys. enumPrio = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>y\<in>set ys. v < y)"
2222  apply (subst upto_enum_word)
2223  apply (subst upt_add_eq_append'[where j="unat v"])
2224    apply simp
2225   apply (rule le_SucI)
2226   apply (rule vlt)
2227  apply (simp only: upt_conv_Cons vlt[simplified less_Suc_eq_le[symmetric]])
2228  apply (intro exI conjI)
2229    apply fastforce
2230   apply clarsimp
2231   apply (drule of_nat_mono_maybe[rotated, where 'a="8"])
2232    apply (fastforce simp: vlt)
2233   apply simp
2234  apply (clarsimp simp: Suc_le_eq)
2235  apply (erule disjE)
2236   apply (drule of_nat_mono_maybe[rotated, where 'a="8"])
2237    apply (simp add: maxPriority_def numPriorities_def)
2238   apply (clarsimp simp: unat_of_nat_eq)
2239  apply (erule conjE)
2240  apply (drule_tac y="unat v" and x="x" in of_nat_mono_maybe[rotated, where 'a="8"])
2241   apply (simp add: maxPriority_def numPriorities_def)+
2242  done
2243
2244lemma rev_enumPrio_word_div:
2245  "unat v \<le> unat maxPriority \<Longrightarrow> \<exists>xs ys. rev enumPrio = ys @ [(v::word8)] @ xs \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>y\<in>set ys. v < y)"
2246  apply (cut_tac v=v in enumPrio_word_div)
2247  apply clarsimp
2248  apply clarsimp
2249  apply (rule_tac x="rev xs" in exI)
2250  apply (rule_tac x="rev ys" in exI)
2251  apply simp
2252  done
2253
2254lemma findM_ignore_head: "\<forall>y\<in> set ys. f y = return False \<Longrightarrow> findM f (ys @ xs) = findM f xs"
2255  apply (induct ys,simp+)
2256  done
2257
2258lemma curDomain_corres: "corres (=) \<top> \<top> (gets cur_domain) (curDomain)"
2259  by (simp add: curDomain_def state_relation_def)
2260
2261lemma valid_queues_non_empty:
2262  "\<And>s d p. \<lbrakk> valid_queues s; ksReadyQueues s (d, p) \<noteq> [] \<rbrakk>
2263   \<Longrightarrow> unat (Max {prio. ksReadyQueues s (d, prio) \<noteq> []}) \<le> unat maxPriority"
2264  apply (subst word_le_nat_alt[symmetric])
2265    apply (subst Max_le_iff)
2266    apply simp
2267   apply blast
2268  apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def)
2269  apply (drule spec)
2270  apply (drule_tac x="a" in spec)
2271  apply fastforce
2272  done
2273
2274lemma lookupBitmapPriority_Max_eqI:
2275  "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
2276   \<Longrightarrow> lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})"
2277  apply (rule Max_eqI[simplified eq_commute]; simp)
2278   apply (fastforce simp: bitmapL1_highest_lookup valid_bitmapQ_bitmapQ_simp)
2279  apply (metis valid_bitmapQ_bitmapQ_simp bitmapQ_from_bitmap_lookup)
2280  done
2281
2282lemma corres_gets_queues_getReadyQueuesL1Bitmap:
2283  "corres (\<lambda>qs l1. ((l1 = 0) = (\<forall>p. qs p = []))) \<top> valid_queues
2284    (gets (\<lambda>s. ready_queues s d)) (getReadyQueuesL1Bitmap d)"
2285  unfolding state_relation_def valid_queues_def getReadyQueuesL1Bitmap_def
2286  by (clarsimp simp: bitmapL1_zero_ksReadyQueues ready_queues_relation_def)
2287
2288lemma guarded_switch_to_chooseThread_fragment_corres:
2289  "corres dc
2290    (P and st_tcb_at runnable t and invs and valid_sched)
2291    (P' and st_tcb_at' runnable' t and invs_no_cicd')
2292          (guarded_switch_to t)
2293          (do runnable \<leftarrow> isRunnable t;
2294              y \<leftarrow> assert runnable;
2295              ThreadDecls_H.switchToThread t
2296           od)"
2297  unfolding guarded_switch_to_def isRunnable_def
2298  apply simp
2299  apply (rule corres_guard_imp)
2300    apply (rule corres_split[OF _ gts_corres])
2301      apply (rule corres_assert_assume_l)
2302      apply (rule corres_assert_assume_r)
2303      apply (rule switch_thread_corres)
2304     apply (wp gts_st_tcb_at)+
2305   apply (clarsimp simp: st_tcb_at_tcb_at invs_def valid_state_def valid_pspace_def valid_sched_def
2306                          invs_valid_vs_lookup invs_unique_refs)
2307  apply (auto elim!: pred_tcb'_weakenE split: thread_state.splits
2308              simp: pred_tcb_at' runnable'_def all_invs_but_ct_idle_or_in_cur_domain'_def)
2309  done
2310
2311lemma bitmap_lookup_queue_is_max_non_empty:
2312  "\<lbrakk> valid_queues s'; (s, s') \<in> state_relation; invs s;
2313     ksReadyQueuesL1Bitmap s' (ksCurDomain s') \<noteq> 0 \<rbrakk>
2314   \<Longrightarrow> ksReadyQueues s' (ksCurDomain s', lookupBitmapPriority (ksCurDomain s') s') =
2315        max_non_empty_queue (ready_queues s (cur_domain s))"
2316  unfolding all_invs_but_ct_idle_or_in_cur_domain'_def valid_queues_def
2317  by (clarsimp simp add: max_non_empty_queue_def lookupBitmapPriority_Max_eqI
2318                         state_relation_def ready_queues_relation_def)
2319
2320lemma ksReadyQueuesL1Bitmap_return_wp:
2321  "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s d) s \<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>rv s. P rv s\<rbrace>"
2322  unfolding getReadyQueuesL1Bitmap_def
2323  by wp
2324
2325lemma ksReadyQueuesL2Bitmap_return_wp:
2326  "\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s (d,i)) s \<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>\<lambda>rv s. P rv s\<rbrace>"
2327  unfolding getReadyQueuesL2Bitmap_def
2328  by wp
2329
2330lemma ksReadyQueuesL1Bitmap_st_tcb_at':
2331  "\<lbrakk> ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0 ; valid_queues s \<rbrakk>
2332   \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s"
2333   apply (drule bitmapQ_from_bitmap_lookup; clarsimp simp: valid_queues_def)
2334   apply (clarsimp simp add: valid_bitmapQ_bitmapQ_simp)
2335   apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)")
2336    apply simp
2337   apply (simp add: valid_queues_no_bitmap_def)
2338   apply (erule_tac x="ksCurDomain s" in allE)
2339   apply (erule_tac x="lookupBitmapPriority (ksCurDomain s) s" in allE)
2340   apply (clarsimp simp: st_tcb_at'_def)
2341   apply (erule obj_at'_weaken)
2342   apply simp
2343   done
2344
2345lemma chooseThread_corres:
2346  "corres dc (invs and valid_sched) (invs_no_cicd')
2347     choose_thread chooseThread" (is "corres _ ?PREI ?PREH _ _")
2348proof -
2349  show ?thesis
2350  unfolding choose_thread_def chooseThread_def numDomains_def
2351  apply (simp only: numDomains_def return_bind Let_def)
2352  apply (simp cong: if_cong) (* clean up if 1 < numDomains *)
2353  apply (subst if_swap[where P="_ \<noteq> 0"]) (* put switchToIdleThread on first branch*)
2354  apply (rule corres_name_pre)
2355  apply (rule corres_guard_imp)
2356    apply (rule corres_split[OF _ curDomain_corres])
2357      apply clarsimp
2358      apply (rule corres_split[OF _ corres_gets_queues_getReadyQueuesL1Bitmap])
2359        apply (erule corres_if2[OF sym])
2360         apply (rule switch_idle_thread_corres)
2361        apply (rule corres_symb_exec_r)
2362           apply (rule corres_symb_exec_r)
2363              apply (rule_tac
2364                       P="\<lambda>s. ?PREI s \<and> queues = ready_queues s (cur_domain s) \<and>
2365                              st_tcb_at runnable (hd (max_non_empty_queue queues)) s" and
2366                       P'="\<lambda>s. (?PREH s \<and> st_tcb_at' runnable' (hd queue) s) \<and>
2367                               l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and>
2368                               l1 \<noteq> 0 \<and>
2369                               queue = ksReadyQueues s (ksCurDomain s,
2370                                         lookupBitmapPriority (ksCurDomain s) s)" and
2371                       F="hd queue = hd (max_non_empty_queue queues)" in corres_req)
2372               apply (fastforce dest!: invs_no_cicd'_queues simp: bitmap_lookup_queue_is_max_non_empty)
2373              apply clarsimp
2374              apply (rule corres_guard_imp)
2375                apply (rule_tac P=\<top> and P'=\<top> in guarded_switch_to_chooseThread_fragment_corres)
2376               apply (wp ksReadyQueuesL2Bitmap_return_wp
2377                      |clarsimp simp: getQueue_def getReadyQueuesL2Bitmap_def)+
2378      apply (clarsimp simp: if_apply_def2)
2379      apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift ksReadyQueuesL1Bitmap_return_wp)
2380     apply (simp add: curDomain_def, wp)+
2381   apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def)
2382   apply (erule_tac x="cur_domain sa" in allE)
2383   apply (erule_tac x="Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}" in allE)
2384   apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []})")
2385    apply (clarsimp)
2386    apply (subgoal_tac
2387             "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}) \<noteq> []")
2388     apply (fastforce elim!: setcomp_Max_has_prop)+
2389  apply (clarsimp dest!: invs_no_cicd'_queues)
2390  apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at')
2391  done
2392qed
2393
2394lemma thread_get_comm: "do x \<leftarrow> thread_get f p; y \<leftarrow> gets g; k x y od =
2395           do y \<leftarrow> gets g; x \<leftarrow> thread_get f p; k x y od"
2396  apply (rule ext)
2397  apply (clarsimp simp add: gets_the_def assert_opt_def
2398                   bind_def gets_def get_def return_def
2399                   thread_get_def
2400                   fail_def split: option.splits)
2401  done
2402
2403lemma schact_bind_inside: "do x \<leftarrow> f; (case act of resume_cur_thread \<Rightarrow> f1 x
2404                     | switch_thread t \<Rightarrow> f2 t x
2405                     | choose_new_thread \<Rightarrow> f3 x) od
2406          = (case act of resume_cur_thread \<Rightarrow> (do x \<leftarrow> f; f1 x od)
2407                     | switch_thread t \<Rightarrow> (do x \<leftarrow> f; f2 t x od)
2408                     | choose_new_thread \<Rightarrow> (do x \<leftarrow> f; f3 x od))"
2409  apply (case_tac act,simp_all)
2410  done
2411
2412interpretation tcb_sched_action_extended: is_extended' "tcb_sched_action f a"
2413  by (unfold_locales)
2414
2415lemma domain_time_corres:
2416  "corres (=) \<top> \<top> (gets domain_time) getDomainTime"
2417  by (simp add: getDomainTime_def state_relation_def)
2418
2419lemma next_domain_corres:
2420  "corres dc \<top> \<top> next_domain nextDomain"
2421  apply (simp add: next_domain_def nextDomain_def)
2422  apply (rule corres_modify)
2423  apply (simp add: state_relation_def Let_def dschLength_def dschDomain_def)
2424  done
2425
2426lemma valid_queues'_ksCurDomain[simp]:
2427  "valid_queues' (ksCurDomain_update f s) = valid_queues' s"
2428  by (simp add: valid_queues'_def)
2429
2430lemma valid_queues'_ksDomScheduleIdx[simp]:
2431  "valid_queues' (ksDomScheduleIdx_update f s) = valid_queues' s"
2432  by (simp add: valid_queues'_def)
2433
2434lemma valid_queues'_ksDomSchedule[simp]:
2435  "valid_queues' (ksDomSchedule_update f s) = valid_queues' s"
2436  by (simp add: valid_queues'_def)
2437
2438lemma valid_queues'_ksDomainTime[simp]:
2439  "valid_queues' (ksDomainTime_update f s) = valid_queues' s"
2440  by (simp add: valid_queues'_def)
2441
2442lemma valid_queues'_ksWorkUnitsCompleted[simp]:
2443  "valid_queues' (ksWorkUnitsCompleted_update f s) = valid_queues' s"
2444  by (simp add: valid_queues'_def)
2445
2446lemma valid_queues_ksCurDomain[simp]:
2447  "Invariants_H.valid_queues (ksCurDomain_update f s) = Invariants_H.valid_queues s"
2448  by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs)
2449
2450lemma valid_queues_ksDomScheduleIdx[simp]:
2451  "Invariants_H.valid_queues (ksDomScheduleIdx_update f s) = Invariants_H.valid_queues s"
2452  by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs)
2453
2454lemma valid_queues_ksDomSchedule[simp]:
2455  "Invariants_H.valid_queues (ksDomSchedule_update f s) = Invariants_H.valid_queues s"
2456  by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs)
2457
2458lemma valid_queues_ksDomainTime[simp]:
2459  "Invariants_H.valid_queues (ksDomainTime_update f s) = Invariants_H.valid_queues s"
2460  by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs)
2461
2462lemma valid_queues_ksWorkUnitsCompleted[simp]:
2463  "Invariants_H.valid_queues (ksWorkUnitsCompleted_update f s) = Invariants_H.valid_queues s"
2464  by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs)
2465
2466lemma valid_irq_node'_ksCurDomain[simp]:
2467  "valid_irq_node' w (ksCurDomain_update f s) = valid_irq_node' w s"
2468  by (simp add: valid_irq_node'_def)
2469
2470lemma valid_irq_node'_ksDomScheduleIdx[simp]:
2471  "valid_irq_node' w (ksDomScheduleIdx_update f s) = valid_irq_node' w s"
2472  by (simp add: valid_irq_node'_def)
2473
2474lemma valid_irq_node'_ksDomSchedule[simp]:
2475  "valid_irq_node' w (ksDomSchedule_update f s) = valid_irq_node' w s"
2476  by (simp add: valid_irq_node'_def)
2477
2478lemma valid_irq_node'_ksDomainTime[simp]:
2479  "valid_irq_node' w (ksDomainTime_update f s) = valid_irq_node' w s"
2480  by (simp add: valid_irq_node'_def)
2481
2482lemma valid_irq_node'_ksWorkUnitsCompleted[simp]:
2483  "valid_irq_node' w (ksWorkUnitsCompleted_update f s) = valid_irq_node' w s"
2484  by (simp add: valid_irq_node'_def)
2485
2486lemma sch_act_wf_ksCurDomain [simp]:
2487  "sa = ChooseNewThread \<Longrightarrow> sch_act_wf sa (ksCurDomain_update f s) = sch_act_wf sa s"
2488  apply (cases sa)
2489  apply (simp_all add: ct_in_state'_def  tcb_in_cur_domain'_def)
2490  done
2491
2492lemma next_domain_valid_sched[wp]:
2493  "\<lbrace> valid_sched and (\<lambda>s. scheduler_action s  = choose_new_thread)\<rbrace> next_domain \<lbrace> \<lambda>_. valid_sched \<rbrace>"
2494  apply (simp add: next_domain_def Let_def)
2495  apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def)
2496  apply (simp add:valid_blocked_2_def)
2497  done
2498
2499lemma nextDomain_invs_no_cicd':
2500  "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> nextDomain \<lbrace> \<lambda>_. invs_no_cicd' \<rbrace>"
2501  apply (simp add: nextDomain_def Let_def dschLength_def dschDomain_def)
2502  apply wp
2503  apply (clarsimp simp: invs'_def valid_state'_def valid_machine_state'_def
2504                        ct_not_inQ_def cur_tcb'_def ct_idle_or_in_cur_domain'_def dschDomain_def
2505                        all_invs_but_ct_idle_or_in_cur_domain'_def)
2506  done
2507
2508lemma bind_dummy_ret_val:
2509  "do y \<leftarrow> a;
2510      b
2511   od = do a; b od"
2512  by simp
2513
2514lemma schedule_ChooseNewThread_fragment_corres:
2515  "corres dc (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread))
2516     (do _ \<leftarrow> when (domainTime = 0) next_domain;
2517         choose_thread
2518      od)
2519     (do _ \<leftarrow> when (domainTime = 0) nextDomain;
2520          chooseThread
2521      od)"
2522  apply (subst bind_dummy_ret_val)
2523  apply (subst bind_dummy_ret_val)
2524  apply (rule corres_guard_imp)
2525    apply (rule corres_split[OF _ corres_when])
2526        apply simp
2527        apply (rule chooseThread_corres)
2528       apply simp
2529      apply (rule next_domain_corres)
2530     apply (wp nextDomain_invs_no_cicd')+
2531   apply (clarsimp simp: valid_sched_def invs'_def valid_state'_def all_invs_but_ct_idle_or_in_cur_domain'_def)+
2532  done
2533
2534lemma schedule_switch_thread_fastfail_corres:
2535  "\<lbrakk> ct \<noteq> it \<longrightarrow> (tp = tp' \<and> cp = cp') ; ct = ct' ; it = it' \<rbrakk> \<Longrightarrow>
2536   corres ((=)) (is_etcb_at ct) (tcb_at' ct)
2537     (schedule_switch_thread_fastfail ct it cp tp)
2538     (scheduleSwitchThreadFastfail ct' it' cp' tp')"
2539  by (clarsimp simp: schedule_switch_thread_fastfail_def scheduleSwitchThreadFastfail_def)
2540
2541lemma gets_is_highest_prio_expand:
2542  "gets (is_highest_prio d p) \<equiv> do
2543    q \<leftarrow> gets (\<lambda>s. ready_queues s d);
2544    return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)
2545   od"
2546  by (clarsimp simp: is_highest_prio_def gets_def)
2547
2548lemma isHighestPrio_corres:
2549  assumes "d' = d"
2550  assumes "p' = p"
2551  shows
2552    "corres ((=)) \<top> valid_queues
2553      (gets (is_highest_prio d p))
2554      (isHighestPrio d' p')"
2555  using assms
2556  apply (clarsimp simp: gets_is_highest_prio_expand isHighestPrio_def)
2557  apply (subst getHighestPrio_def')
2558  apply (rule corres_guard_imp)
2559    apply (rule corres_split[OF _ corres_gets_queues_getReadyQueuesL1Bitmap])
2560      apply (rule corres_if_r'[where P'="\<lambda>_. True",rotated])
2561       apply (rule_tac corres_symb_exec_r)
2562              apply (rule_tac
2563                       P="\<lambda>s. q = ready_queues s d
2564                              " and
2565                       P'="\<lambda>s. valid_queues s \<and>
2566                               l1 = ksReadyQueuesL1Bitmap s d \<and>
2567                               l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s" and
2568                       F="hprio = Max {prio. q prio \<noteq> []}" in corres_req)
2569              apply (elim conjE)
2570              apply (clarsimp simp: valid_queues_def)
2571              apply (subst lookupBitmapPriority_Max_eqI; blast?)
2572              apply (fastforce simp: ready_queues_relation_def dest!: state_relationD)
2573             apply fastforce
2574         apply (wpsimp simp: if_apply_def2 wp: hoare_drop_imps ksReadyQueuesL1Bitmap_return_wp)+
2575  done
2576
2577crunch valid_idle_etcb[wp]: set_scheduler_action valid_idle_etcb
2578
2579crunch inv[wp]: isHighestPrio P
2580crunch inv[wp]: curDomain P
2581crunch inv[wp]: schedule_switch_thread_fastfail P
2582crunch inv[wp]: scheduleSwitchThreadFastfail P
2583
2584lemma setSchedulerAction_invs': (* not in wp set, clobbered by ssa_wp *)
2585  "\<lbrace>\<lambda>s. invs' s \<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>_. invs' \<rbrace>"
2586  by (wpsimp simp: invs'_def cur_tcb'_def valid_state'_def valid_irq_node'_def ct_not_inQ_def
2587                   valid_queues_def valid_queues_no_bitmap_def valid_queues'_def
2588                   ct_idle_or_in_cur_domain'_def)
2589
2590lemma thread_get_tcb_state_wp:
2591  "\<lbrace>\<lambda>s. st_tcb_at (\<lambda>t. P (f t) s) ptr s\<rbrace> thread_get (\<lambda>tcb. f (tcb_state tcb)) ptr \<lbrace>P\<rbrace>"
2592  unfolding ethread_get_def
2593  by (wp | clarsimp simp add: thread_get_def st_tcb_at_def get_tcb_def obj_at_def)+
2594
2595lemma scheduleChooseNewThread_corres:
2596  "corres dc
2597    (\<lambda>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread)
2598    (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread)
2599           schedule_choose_new_thread scheduleChooseNewThread"
2600  unfolding schedule_choose_new_thread_def scheduleChooseNewThread_def
2601  apply (rule corres_guard_imp)
2602    apply (rule corres_split[OF _ domain_time_corres], clarsimp)
2603      apply (rule corres_split[OF _ schedule_ChooseNewThread_fragment_corres, simplified bind_assoc])
2604        apply (rule set_sa_corres)
2605        apply (wp | simp)+
2606    apply (wp | simp add: getDomainTime_def)+
2607   apply auto
2608  done
2609
2610crunch static_inv[wp]: guarded_switch_to "\<lambda>_. P"
2611
2612(* ethread_get_when only corresponds with a non-when version if its condition holds *)
2613lemma ethread_get_when_corres':
2614  assumes x: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> r (f etcb) (f' tcb')"
2615  shows      "corres r (is_etcb_at t and K b) (tcb_at' t and K b)
2616                (ethread_get_when b f t) (threadGet f' t)"
2617  apply (clarsimp simp: ethread_get_when_def)
2618  apply (rule corres_guard_imp, rule ethreadget_corres; simp add: x)
2619  done
2620
2621lemma ethread_get_when_corres:
2622  assumes x: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> r (f etcb) (f' tcb')"
2623  shows      "corres (\<lambda>rv rv'. b \<longrightarrow> r rv rv') (is_etcb_at t) (tcb_at' t)
2624                (ethread_get_when b f t) (threadGet f' t)"
2625  apply (clarsimp simp: ethread_get_when_def)
2626  apply (rule conjI; clarsimp)
2627  apply (rule corres_guard_imp, rule ethreadget_corres; simp add: x)
2628  apply (clarsimp simp: threadGet_def)
2629  apply (rule corres_noop)
2630  apply wpsimp+
2631  done
2632
2633lemma schedule_switch_thread_fastfail_wp:
2634  "\<lbrace> P (ct \<noteq> it \<longrightarrow> tp < cp) \<rbrace> schedule_switch_thread_fastfail ct it cp tp \<lbrace>\<lambda>rv. P rv\<rbrace>"
2635  unfolding schedule_switch_thread_fastfail_def
2636  by wpsimp auto
2637
2638lemma schedule_corres:
2639  "corres dc (invs and valid_sched and valid_list) invs' (Schedule_A.schedule) ThreadDecls_H.schedule"
2640  supply ethread_get_wp[wp del]
2641  supply ssa_wp[wp del]
2642  supply tcbSchedEnqueue_invs'[wp del]
2643  supply tcbSchedEnqueue_invs'_not_ResumeCurrentThread[wp del]
2644  supply setSchedulerAction_direct[wp]
2645  supply if_split[split del]
2646
2647  apply (clarsimp simp: Schedule_A.schedule_def Thread_H.schedule_def)
2648  apply (subst thread_get_test)
2649  apply (subst thread_get_comm)
2650  apply (subst schact_bind_inside)
2651  apply (rule corres_guard_imp)
2652    apply (rule corres_split[OF _ gct_corres[THEN corres_rel_imp[where r="\<lambda>x y. y = x"],simplified]])
2653        apply (rule corres_split[OF _ get_sa_corres])
2654          apply (rule corres_split_sched_act,assumption)
2655            apply (rule_tac P="tcb_at ct" in corres_symb_exec_l')
2656              apply (rule_tac corres_symb_exec_l)
2657                apply simp
2658                apply (rule corres_assert_ret)
2659               apply ((wpsimp wp: thread_get_wp' gets_exs_valid)+)
2660         prefer 2
2661         (* choose thread *)
2662         apply clarsimp
2663          apply (rule corres_split[OF _ thread_get_isRunnable_corres])
2664            apply (rule corres_split[OF _ corres_when])
2665             apply (rule scheduleChooseNewThread_corres, simp)
2666              apply (rule tcbSchedEnqueue_corres, simp)
2667           apply (wp thread_get_wp' tcbSchedEnqueue_invs' hoare_vcg_conj_lift hoare_drop_imps
2668                  | clarsimp)+
2669        (* switch to thread *)
2670        apply (rule corres_split[OF _ thread_get_isRunnable_corres],
2671                rename_tac was_running wasRunning)
2672          apply (rule corres_split[OF _ corres_when])
2673              apply (rule corres_split[OF _ git_corres], rename_tac it it')
2674                apply (rule_tac F="was_running \<longrightarrow> ct \<noteq> it" in corres_gen_asm)
2675                apply (rule corres_split[OF _ ethreadget_corres[where r="(=)"]],
2676                       rename_tac tp tp')
2677                   apply (rule corres_split[OF _ ethread_get_when_corres[where r="(=)"]],
2678                           rename_tac cp cp')
2679                      apply (rule corres_split[OF _ schedule_switch_thread_fastfail_corres])
2680                           apply (rule corres_split[OF _ curDomain_corres])
2681                             apply (rule corres_split[OF _ isHighestPrio_corres]; simp only:)
2682                               apply (rule corres_if, simp)
2683                                apply (rule corres_split[OF _ tcbSchedEnqueue_corres])
2684                                  apply (simp, fold dc_def)
2685                                  apply (rule corres_split[OF _ set_sa_corres])
2686                                     apply (rule scheduleChooseNewThread_corres, simp)
2687
2688                                   apply (wp | simp)+
2689                                   apply (simp add: valid_sched_def)
2690                                   apply wp
2691                                   apply (rule hoare_vcg_conj_lift)
2692                                    apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked')
2693                                   apply (wpsimp wp: setSchedulerAction_invs')+
2694                                 apply (wp tcb_sched_action_enqueue_valid_blocked hoare_vcg_all_lift enqueue_thread_queued)
2695                                apply (wp tcbSchedEnqueue_invs'_not_ResumeCurrentThread)
2696
2697                               apply (rule corres_if, fastforce)
2698
2699                                apply (rule corres_split[OF _ tcbSchedAppend_corres])
2700                                  apply (simp, fold dc_def)
2701                                  apply (rule corres_split[OF _ set_sa_corres])
2702                                     apply (rule scheduleChooseNewThread_corres, simp)
2703
2704                                   apply (wp | simp)+
2705                                   apply (simp add: valid_sched_def)
2706                                   apply wp
2707                                   apply (rule hoare_vcg_conj_lift)
2708                                    apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked')
2709                                   apply (wpsimp wp: setSchedulerAction_invs')+
2710                                 apply (wp tcb_sched_action_append_valid_blocked hoare_vcg_all_lift append_thread_queued)
2711                                apply (wp tcbSchedAppend_invs'_not_ResumeCurrentThread)
2712
2713                               apply (rule corres_split[OF _ guarded_switch_to_corres], simp)
2714                                 apply (rule set_sa_corres[simplified dc_def])
2715                                 apply (wp | simp)+
2716
2717                             (* isHighestPrio *)
2718                             apply (clarsimp simp: if_apply_def2)
2719                             apply ((wp_once hoare_drop_imp)+)[1]
2720
2721                            apply (simp add: if_apply_def2)
2722                             apply ((wp_once hoare_drop_imp)+)[1]
2723                           apply wpsimp+
2724                     apply (wpsimp simp: etcb_relation_def)+
2725            apply (rule tcbSchedEnqueue_corres)
2726           apply wpsimp+
2727
2728           apply (clarsimp simp: conj_ac cong: conj_cong)
2729           apply wp
2730           apply (rule_tac Q="\<lambda>_ s. valid_blocked_except t s \<and> scheduler_action s = switch_thread t"
2731                    in hoare_post_imp, fastforce)
2732           apply (wp add: tcb_sched_action_enqueue_valid_blocked_except
2733                          tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp
2734                     del: gets_wp)+
2735       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets)
2736       apply (wp gets_wp)+
2737
2738   (* abstract final subgoal *)
2739   apply clarsimp
2740
2741   subgoal for s
2742     apply (clarsimp split: Deterministic_A.scheduler_action.splits
2743                     simp: invs_psp_aligned invs_distinct invs_valid_objs invs_arch_state
2744                           invs_vspace_objs[simplified] tcb_at_invs)
2745     apply (rule conjI, clarsimp)
2746      apply (fastforce simp: invs_def
2747                            valid_sched_def valid_sched_action_def is_activatable_def
2748                            st_tcb_at_def obj_at_def valid_state_def only_idle_def
2749                            )
2750     apply (rule conjI, clarsimp)
2751      subgoal for candidate
2752        apply (clarsimp simp: valid_sched_def invs_def valid_state_def cur_tcb_def
2753                               valid_arch_caps_def valid_sched_action_def
2754                               weak_valid_sched_action_def tcb_at_is_etcb_at
2755                               tcb_at_is_etcb_at[OF st_tcb_at_tcb_at[rotated]]
2756                               valid_blocked_except_def valid_blocked_def)
2757        apply (clarsimp simp add: pred_tcb_at_def obj_at_def is_tcb valid_idle_def)
2758        done
2759     (* choose new thread case *)
2760     apply (intro impI conjI allI tcb_at_invs
2761            | fastforce simp: invs_def cur_tcb_def valid_etcbs_def
2762                              valid_sched_def  st_tcb_at_def obj_at_def valid_state_def
2763                              weak_valid_sched_action_def not_cur_thread_def)+
2764     apply (simp add: valid_sched_def valid_blocked_def valid_blocked_except_def)
2765     done
2766
2767  (* haskell final subgoal *)
2768  apply (clarsimp simp: if_apply_def2 invs'_def valid_state'_def
2769                  cong: imp_cong  split: scheduler_action.splits)
2770  apply (fastforce simp: cur_tcb'_def valid_pspace'_def)
2771  done
2772
2773lemma ssa_all_invs_but_ct_not_inQ':
2774  "\<lbrace>all_invs_but_ct_not_inQ' and sch_act_wf sa and
2775   (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
2776   setSchedulerAction sa \<lbrace>\<lambda>rv. all_invs_but_ct_not_inQ'\<rbrace>"
2777proof -
2778  have obj_at'_sa: "\<And>P addr f s.
2779       obj_at' P addr (ksSchedulerAction_update f s) = obj_at' P addr s"
2780    by (fastforce intro: obj_at'_pspaceI)
2781  have valid_pspace'_sa: "\<And>f s.
2782       valid_pspace' (ksSchedulerAction_update f s) = valid_pspace' s"
2783    by (rule valid_pspace'_ksPSpace, simp)
2784  have iflive_sa: "\<And>f s.
2785       if_live_then_nonz_cap' (ksSchedulerAction_update f s)
2786         = if_live_then_nonz_cap' s"
2787    by (fastforce intro: if_live_then_nonz_cap'_pspaceI)
2788  have ifunsafe_sa[simp]: "\<And>f s.
2789       if_unsafe_then_cap' (ksSchedulerAction_update f s) = if_unsafe_then_cap' s"
2790    by fastforce
2791  have idle_sa[simp]: "\<And>f s.
2792       valid_idle' (ksSchedulerAction_update f s) = valid_idle' s"
2793    by fastforce
2794  show ?thesis
2795    apply (simp add: setSchedulerAction_def)
2796    apply wp
2797    apply (clarsimp simp add: invs'_def valid_state'_def cur_tcb'_def
2798                              obj_at'_sa valid_pspace'_sa Invariants_H.valid_queues_def
2799                              state_refs_of'_def iflive_sa ps_clear_def
2800                              valid_irq_node'_def valid_queues'_def
2801                              tcb_in_cur_domain'_def ct_idle_or_in_cur_domain'_def
2802                              bitmapQ_defs valid_queues_no_bitmap_def
2803                        cong: option.case_cong)
2804    done
2805qed
2806
2807lemma ssa_ct_not_inQ:
2808  "\<lbrace>\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
2809   setSchedulerAction sa \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace>"
2810  by (simp add: setSchedulerAction_def ct_not_inQ_def, wp, clarsimp)
2811
2812lemma ssa_all_invs_but_ct_not_inQ''[simplified]:
2813  "\<lbrace>\<lambda>s. (all_invs_but_ct_not_inQ' s \<and> sch_act_wf sa s)
2814    \<and> (sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)
2815    \<and> (sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)\<rbrace>
2816   setSchedulerAction sa \<lbrace>\<lambda>rv. invs'\<rbrace>"
2817  apply (simp only: all_invs_but_not_ct_inQ_check' [symmetric])
2818  apply (rule hoare_elim_pred_conj)
2819  apply (wp hoare_vcg_conj_lift [OF ssa_all_invs_but_ct_not_inQ' ssa_ct_not_inQ])
2820  apply (clarsimp)
2821  done
2822
2823lemma ssa_invs':
2824  "\<lbrace>invs' and sch_act_wf sa and
2825    (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) and
2826    (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)\<rbrace>
2827   setSchedulerAction sa \<lbrace>\<lambda>rv. invs'\<rbrace>"
2828  apply (wp ssa_all_invs_but_ct_not_inQ'')
2829  apply (clarsimp simp add: invs'_def valid_state'_def)
2830  done
2831
2832lemma getDomainTime_wp[wp]: "\<lbrace>\<lambda>s. P (ksDomainTime s) s \<rbrace> getDomainTime \<lbrace> P \<rbrace>"
2833  unfolding getDomainTime_def
2834  by wp
2835
2836lemma switchToThread_ct_not_queued_2:
2837  "\<lbrace>invs_no_cicd' and tcb_at' t\<rbrace> switchToThread t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>"
2838  (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>")
2839  apply (simp add: Thread_H.switchToThread_def)
2840  apply (wp)
2841    apply (simp add: X64_H.switchToThread_def setCurThread_def)
2842    apply (wp tcbSchedDequeue_not_tcbQueued | simp )+
2843  done
2844
2845lemma hd_ksReadyQueues_runnable_2:
2846  "\<lbrakk>Invariants_H.valid_queues s; ksReadyQueues s (d, p) = a # as\<rbrakk>
2847     \<Longrightarrow> st_tcb_at' runnable' a s"
2848   apply( rule valid_queues_running)
2849   apply(rule suffix_Cons_mem)
2850   apply(simp add: suffix_def)
2851   apply(rule exI)
2852   apply(rule eq_Nil_appendI)
2853   by auto
2854
2855lemma setCurThread_obj_at':
2856  "\<lbrace> obj_at' P t \<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s \<rbrace>"
2857proof -
2858  have obj_at'_ct: "\<And>P addr f s.
2859       obj_at' P addr (ksCurThread_update f s) = obj_at' P addr s"
2860    by (fastforce intro: obj_at'_pspaceI)
2861  show ?thesis
2862    apply (simp add: setCurThread_def)
2863    apply wp
2864    apply (simp add: ct_in_state'_def st_tcb_at'_def obj_at'_ct)
2865    done
2866qed
2867
2868lemma switchToIdleThread_ct_not_queued_no_cicd':
2869  "\<lbrace> invs_no_cicd' \<rbrace> switchToIdleThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<rbrace>"
2870  apply (simp add: Thread_H.switchToIdleThread_def)
2871  apply (wp setCurThread_obj_at')
2872  apply (rule idle'_not_tcbQueued')
2873  apply (simp add: invs_no_cicd'_def)+
2874  done
2875
2876lemma switchToIdleThread_activatable_2[wp]:
2877  "\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>"
2878  apply (simp add: Thread_H.switchToIdleThread_def
2879                   X64_H.switchToIdleThread_def)
2880  apply (wp setCurThread_ct_in_state)
2881  apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_idle'_def
2882                        pred_tcb_at'_def obj_at'_def)
2883  done
2884
2885lemma switchToThread_tcb_in_cur_domain':
2886  "\<lbrace>tcb_in_cur_domain' thread\<rbrace> ThreadDecls_H.switchToThread thread
2887  \<lbrace>\<lambda>y s. tcb_in_cur_domain' (ksCurThread s) s\<rbrace>"
2888  apply (simp add: Thread_H.switchToThread_def)
2889  apply (rule hoare_pre)
2890  apply (wp)
2891    apply (simp add: X64_H.switchToThread_def setCurThread_def)
2892    apply (wp tcbSchedDequeue_not_tcbQueued | simp )+
2893   apply (simp add:tcb_in_cur_domain'_def)
2894   apply (wp tcbSchedDequeue_tcbDomain | wps)+
2895  apply (clarsimp simp:tcb_in_cur_domain'_def)
2896  done
2897
2898lemma chooseThread_invs_no_cicd'_posts: (* generic version *)
2899  "\<lbrace> invs_no_cicd' \<rbrace> chooseThread
2900   \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and>
2901           ct_in_state' activatable' s \<and>
2902           (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) \<rbrace>"
2903    (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>")
2904proof -
2905  note switchToThread_invs[wp del]
2906  note switchToThread_invs_no_cicd'[wp del]
2907  note switchToThread_lookupBitmapPriority_wp[wp]
2908  note assert_wp[wp del]
2909
2910  show ?thesis
2911    unfolding chooseThread_def Let_def numDomains_def curDomain_def
2912    apply (simp only: return_bind, simp)
2913    apply (rule hoare_seq_ext[where B="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
2914     apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
2915                               rv = ksReadyQueuesL1Bitmap s curdom" in hoare_seq_ext)
2916      apply (rename_tac l1)
2917      apply (case_tac "l1 = 0")
2918       (* switch to idle thread *)
2919       apply simp
2920       apply (rule hoare_pre)
2921        apply (wp_once switchToIdleThread_ct_not_queued_no_cicd')
2922        apply (wp_once)
2923        apply ((wp hoare_disjI1 switchToIdleThread_curr_is_idle)+)[1]
2924       apply simp
2925      (* we have a thread to switch to *)
2926      apply (clarsimp simp: bitmap_fun_defs)
2927      apply (wp assert_inv switchToThread_ct_not_queued_2 assert_inv hoare_disjI2
2928                switchToThread_tcb_in_cur_domain')
2929      apply clarsimp
2930      apply (clarsimp dest!: invs_no_cicd'_queues
2931                      simp: valid_queues_def lookupBitmapPriority_def[symmetric])
2932      apply (drule (3) lookupBitmapPriority_obj_at')
2933      apply normalise_obj_at'
2934      apply (fastforce simp: tcb_in_cur_domain'_def inQ_def elim: obj_at'_weaken)
2935     apply (wp | simp add: bitmap_fun_defs curDomain_def)+
2936    done
2937qed
2938
2939lemma chooseThread_activatable_2:
2940  "\<lbrace>invs_no_cicd'\<rbrace> chooseThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>"
2941  apply (rule hoare_pre, rule hoare_strengthen_post)
2942    apply (rule chooseThread_invs_no_cicd'_posts)
2943   apply simp+
2944  done
2945
2946lemma chooseThread_activatable:
2947  "\<lbrace>invs'\<rbrace> chooseThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>"
2948  apply (rule hoare_pre, rule chooseThread_activatable_2)
2949  apply (simp add: invs'_to_invs_no_cicd'_def)
2950  done
2951
2952lemma chooseThread_ct_not_queued_2:
2953  "\<lbrace> invs_no_cicd'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>"
2954    (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>")
2955  apply (rule hoare_pre, rule hoare_strengthen_post)
2956    apply (rule chooseThread_invs_no_cicd'_posts)
2957   apply simp+
2958  done
2959
2960lemma chooseThread_invs_no_cicd':
2961  "\<lbrace> invs_no_cicd' \<rbrace> chooseThread \<lbrace>\<lambda>rv. invs' \<rbrace>"
2962proof -
2963  note switchToThread_invs[wp del]
2964  note switchToThread_invs_no_cicd'[wp del]
2965  note switchToThread_lookupBitmapPriority_wp[wp]
2966  note assert_wp[wp del]
2967
2968  (* FIXME this is almost identical to the chooseThread_invs_no_cicd'_posts proof, can generalise? *)
2969  show ?thesis
2970    unfolding chooseThread_def Let_def numDomains_def curDomain_def
2971    apply (simp only: return_bind, simp)
2972    apply (rule hoare_seq_ext[where B="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
2973     apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
2974                               rv = ksReadyQueuesL1Bitmap s curdom" in hoare_seq_ext)
2975      apply (rename_tac l1)
2976      apply (case_tac "l1 = 0")
2977       (* switch to idle thread *)
2978       apply (simp, wp_once switchToIdleThread_invs_no_cicd', simp)
2979      (* we have a thread to switch to *)
2980      apply (clarsimp simp: bitmap_fun_defs)
2981      apply (wp assert_inv)
2982      apply (clarsimp dest!: invs_no_cicd'_queues simp: valid_queues_def)
2983      apply (fastforce elim: bitmapQ_from_bitmap_lookup simp: lookupBitmapPriority_def)
2984     apply (wp | simp add: bitmap_fun_defs curDomain_def)+
2985    done
2986qed
2987
2988lemma chooseThread_in_cur_domain':
2989  "\<lbrace> invs_no_cicd' \<rbrace> chooseThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s\<rbrace>"
2990  apply (rule hoare_pre, rule hoare_strengthen_post)
2991    apply (rule chooseThread_invs_no_cicd'_posts, simp_all)
2992  done
2993
2994lemma scheduleChooseNewThread_invs':
2995  "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) \<rbrace>
2996   scheduleChooseNewThread
2997   \<lbrace> \<lambda>_ s. invs' s \<rbrace>"
2998  unfolding scheduleChooseNewThread_def
2999  apply (wpsimp wp: ssa_invs' chooseThread_invs_no_cicd' chooseThread_ct_not_queued_2
3000                    chooseThread_activatable_2 chooseThread_invs_no_cicd'
3001                    chooseThread_in_cur_domain' nextDomain_invs_no_cicd' chooseThread_ct_not_queued_2)
3002  apply (clarsimp simp: invs'_to_invs_no_cicd'_def)
3003  done
3004
3005lemma schedule_invs':
3006  "\<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. invs'\<rbrace>"
3007  supply ssa_wp[wp del]
3008  apply (simp add: schedule_def)
3009  apply (rule_tac hoare_seq_ext, rename_tac t)
3010   apply (wp, wpc)
3011      \<comment> \<open>action = ResumeCurrentThread\<close>
3012      apply (wp)[1]
3013     \<comment> \<open>action = ChooseNewThread\<close>
3014     apply (wp scheduleChooseNewThread_invs')
3015    \<comment> \<open>action = SwitchToThread candidate\<close>
3016    apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs'
3017                      chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct
3018                      switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2
3019           | wp hoare_disjI2[where Q="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
3020           | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
3021           | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
3022           | strengthen invs_invs_no_cicd'
3023           | wp hoare_vcg_imp_lift)+
3024  apply (frule invs_sch_act_wf')
3025  apply (auto simp: invs_sch_act_wf' obj_at'_activatable_st_tcb_at'
3026                     st_tcb_at'_runnable_is_activatable)
3027  done
3028
3029lemma setCurThread_nosch:
3030  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
3031  setCurThread t
3032  \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
3033  apply (simp add: setCurThread_def)
3034  apply wp
3035  apply simp
3036  done
3037
3038lemma stt_nosch:
3039  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
3040  switchToThread t
3041  \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
3042  apply (simp add: Thread_H.switchToThread_def X64_H.switchToThread_def storeWordUser_def)
3043  apply (wp setCurThread_nosch hoare_drop_imp |simp)+
3044  done
3045
3046lemma stit_nosch[wp]:
3047  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
3048    switchToIdleThread
3049   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
3050  apply (simp add: Thread_H.switchToIdleThread_def
3051                   X64_H.switchToIdleThread_def  storeWordUser_def)
3052  apply (wp setCurThread_nosch | simp add: getIdleThread_def)+
3053  done
3054
3055lemma chooseThread_nosch:
3056  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
3057  chooseThread
3058  \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
3059  unfolding chooseThread_def Let_def numDomains_def curDomain_def
3060  apply (simp only: return_bind, simp)
3061  apply (wp findM_inv | simp)+
3062  apply (case_tac queue)
3063  apply (wp stt_nosch | simp add: curDomain_def bitmap_fun_defs)+
3064  done
3065
3066lemma schedule_sch:
3067  "\<lbrace>\<top>\<rbrace> schedule \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>"
3068  by (wp setSchedulerAction_direct | wpc| simp add: schedule_def scheduleChooseNewThread_def)+
3069
3070lemma schedule_sch_act_simple:
3071  "\<lbrace>\<top>\<rbrace> schedule \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>"
3072  apply (rule hoare_strengthen_post [OF schedule_sch])
3073  apply (simp add: sch_act_simple_def)
3074  done
3075
3076lemma ssa_ct:
3077  "\<lbrace>ct_in_state' P\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>"
3078proof -
3079  have obj_at'_sa: "\<And>P addr f s.
3080       obj_at' P addr (ksSchedulerAction_update f s) = obj_at' P addr s"
3081    by (fastforce intro: obj_at'_pspaceI)
3082  show ?thesis
3083    apply (unfold setSchedulerAction_def)
3084    apply wp
3085    apply (clarsimp simp add: ct_in_state'_def pred_tcb_at'_def obj_at'_sa)
3086    done
3087qed
3088
3089lemma scheduleChooseNewThread_ct_activatable'[wp]:
3090  "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) \<rbrace>
3091   scheduleChooseNewThread
3092   \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>"
3093  unfolding scheduleChooseNewThread_def
3094  by (wpsimp simp: ct_in_state'_def
3095                wp: ssa_invs' nextDomain_invs_no_cicd'
3096                    chooseThread_activatable_2[simplified ct_in_state'_def]
3097         | (rule hoare_lift_Pf[where f=ksCurThread], solves wp)
3098         | strengthen invs_invs_no_cicd')+
3099
3100lemma schedule_ct_activatable'[wp]:
3101  "\<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>"
3102  supply ssa_wp[wp del]
3103  apply (simp add: schedule_def)
3104  apply (rule_tac hoare_seq_ext, rename_tac t)
3105   apply (wp, wpc)
3106      \<comment> \<open>action = ResumeCurrentThread\<close>
3107      apply (wp)[1]
3108     \<comment> \<open>action = ChooseNewThread\<close>
3109     apply wpsimp
3110    \<comment> \<open>action = SwitchToThread\<close>
3111    apply (wpsimp wp: ssa_invs' setSchedulerAction_direct ssa_ct
3112           | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
3113           | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
3114           | strengthen invs_invs_no_cicd'
3115           | wp hoare_vcg_imp_lift)+
3116  apply (fastforce dest: invs_sch_act_wf' elim: pred_tcb'_weakenE
3117                   simp: sch_act_wf obj_at'_activatable_st_tcb_at')
3118  done
3119
3120lemma threadSet_sch_act_sane:
3121  "\<lbrace>sch_act_sane\<rbrace> threadSet f t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
3122  by (wp sch_act_sane_lift)
3123
3124lemma rescheduleRequired_sch_act_sane[wp]:
3125  "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>"
3126  apply (simp add: rescheduleRequired_def sch_act_sane_def
3127                   setSchedulerAction_def)
3128  by (wp | wpc | clarsimp)+
3129
3130lemma tcbSchedDequeue_sch_act_sane[wp]:
3131  "\<lbrace>sch_act_sane\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
3132  by (wp sch_act_sane_lift)
3133
3134lemma sts_sch_act_sane:
3135  "\<lbrace>sch_act_sane\<rbrace> setThreadState st t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
3136  apply (simp add: setThreadState_def)
3137  including no_pre
3138  apply (wp hoare_drop_imps
3139           | simp add: threadSet_sch_act_sane sane_update)+
3140  done
3141
3142lemma sbn_sch_act_sane:
3143  "\<lbrace>sch_act_sane\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
3144  apply (simp add: setBoundNotification_def)
3145  apply (wp | simp add: threadSet_sch_act_sane sane_update)+
3146  done
3147
3148lemma possibleSwitchTo_corres:
3149  "corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t)
3150    (Invariants_H.valid_queues and valid_queues' and
3151    (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs')
3152      (possible_switch_to t)
3153      (possibleSwitchTo t)"
3154  supply ethread_get_wp[wp del]
3155  apply (simp add: possible_switch_to_def possibleSwitchTo_def cong: if_cong)
3156  apply (rule corres_guard_imp)
3157    apply (rule corres_split[OF _ curDomain_corres], simp)
3158      apply (rule corres_split[OF _ ethreadget_corres[where r="(=)"]])
3159         apply (rule corres_split[OF _ get_sa_corres])
3160           apply (rule corres_if, simp)
3161            apply (rule tcbSchedEnqueue_corres)
3162           apply (rule corres_if, simp)
3163             apply (case_tac action; simp)
3164            apply (rule corres_split[OF _ rescheduleRequired_corres])
3165              apply (rule tcbSchedEnqueue_corres)
3166             apply (wp rescheduleRequired_valid_queues'_weak)+
3167           apply (rule set_sa_corres, simp)
3168          apply (wpsimp simp: etcb_relation_def if_apply_def2
3169                        wp: hoare_drop_imp[where f="ethread_get a b" for a b])+
3170      apply (wp hoare_drop_imps)[1]
3171     apply wp+
3172   apply (fastforce simp: valid_sched_def invs_def valid_state_def cur_tcb_def
3173                          valid_sched_action_def weak_valid_sched_action_def
3174                          tcb_at_is_etcb_at[OF st_tcb_at_tcb_at[rotated]])
3175  apply (simp add: tcb_at_is_etcb_at)
3176  done
3177
3178lemma possibleSwitchTo_corres_runnable_abs:
3179  "corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t)
3180    (Invariants_H.valid_queues and valid_queues' and
3181    (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and valid_objs')
3182      (possible_switch_to t)
3183      (possibleSwitchTo t)"
3184  apply (rule stronger_corres_guard_imp, rule possibleSwitchTo_corres)
3185   apply clarsimp
3186  apply (clarsimp simp: st_tcb_at_runnable_coerce_concrete)
3187  done
3188
3189end
3190end
3191