1(*
2 * Copyright 2014, NICTA
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(NICTA_GPL)
9 *)
10
11theory Finalise_DR
12imports
13  KHeap_DR
14  "AInvs.VSpaceEntries_AI"
15begin
16
17context begin interpretation Arch . (*FIXME: arch_split*)
18
19definition
20 "transform_pd_slot_ref x
21     = (x && ~~ mask pd_bits,
22        unat ((x && mask pd_bits) >> 2))"
23definition
24 "transform_pt_slot_ref x
25     = (x && ~~ mask pt_bits,
26        unat ((x && mask pt_bits) >> 2))"
27
28lemma trancl_image:
29  assumes inj: "inj_on f (Domain S \<union> Range S)"
30  shows "trancl ((\<lambda>(x, y). (f x, f y)) ` S) = (\<lambda>(x, y). (f x, f y)) ` trancl S"
31  (is "?lhs = ?rhs")
32  apply safe
33   apply (erule trancl.induct)
34    apply clarsimp
35    apply (erule image_eqI[rotated, OF r_into_trancl])
36    apply simp
37   apply (clarsimp simp: inj_on_eq_iff[OF inj]
38                         RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]]
39                         DomainI)
40   apply (erule(1) image_eqI[rotated, OF trancl_into_trancl])
41   apply simp
42  apply (erule trancl.induct)
43   apply (rule r_into_trancl, erule image_eqI[rotated])
44   apply simp
45  apply (erule trancl_into_trancl)
46  apply (erule image_eqI[rotated])
47  apply simp
48  done
49
50lemma descendants_of_eqv:
51  assumes cte_at: "mdb_cte_at (swp (cte_wp_at P) s) (cdt s)"
52    and cte_at_p: "cte_at p s"
53  shows "KHeap_D.descendants_of (transform_cslot_ptr p) (transform s)
54           = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s)"
55proof -
56  note inj = transform_cdt_slot_inj_on_mdb_cte_at[OF cte_at]
57  have P: "{(x, y). KHeap_D.is_cdt_parent (transform s) x y}
58              = (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y))
59                      ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}"
60    apply (simp add: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def)
61    apply (simp add: transform_def transform_cdt_def map_lift_over_eq_Some
62                     inj)
63    apply auto
64    done
65  have inj': "inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s))"
66    using cte_at_p mdb_cte_atD[OF _ cte_at]
67    apply -
68    apply (rule transform_cdt_slot_inj_on_cte_at[where P=\<top> and s=s])
69    apply (fastforce simp: cte_wp_at_caps_of_state elim!: ranE)
70    done
71  show ?thesis
72    apply (simp add: KHeap_D.descendants_of_def CSpaceAcc_A.descendants_of_def
73                     KHeap_D.cdt_parent_rel_def CSpaceAcc_A.cdt_parent_rel_def)
74    apply (simp add: P)
75    apply (subst trancl_image)
76     apply (rule subset_inj_on[OF inj])
77     apply (auto simp: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def)[1]
78    apply safe
79     apply (subst(asm) inj_on_eq_iff[OF inj'], simp_all)
80     apply (drule DomainI[THEN eqset_imp_iff[OF trancl_domain, THEN iffD1]])
81     apply (auto simp: CSpaceAcc_A.is_cdt_parent_def)
82    done
83qed
84
85(*
86(* Fast finalise is done in TCB_DR, this file only deals with finalise *)
87lemma dcorres_unmap_page_empty:
88  "dcorres dc \<top> \<top> (PageTableUnmap_D.unmap_page x) (return a)"
89  apply (simp add:PageTableUnmap_D.unmap_page_def)
90  apply (rule corres_symb_exec_l)
91    apply (rule corres_guard_imp)
92    apply (rule_tac x = "[]" in select_pick_corres)
93      apply (clarsimp simp:mapM_x_def sequence_x_def del:hoare_post_taut)
94prefer 4
95  apply (rule hoare_post_taut)
96  apply simp_all
97  apply (simp add:exs_valid_def slots_with_def gets_def has_slots_def get_def bind_def return_def )
98done
99*)
100
101lemma dcorres_revoke_cap_no_descendants:
102  "slot' = transform_cslot_ptr slot \<Longrightarrow>
103  dcorres dc \<top> (\<lambda>s. valid_mdb s \<and> cte_at slot s \<and>  CSpaceAcc_A.descendants_of slot (cdt s) = {})
104    (revoke_cap_simple slot')
105    (return x)"
106  apply (rule dcorres_revoke_cap_simple_helper)
107  apply (simp add:gets_def)
108  apply (rule dcorres_absorb_get_l)
109  apply (subgoal_tac "(KHeap_D.descendants_of slot' (transform s')) = {}")
110   apply clarsimp
111   apply (rule dcorres_absorb_get_l)
112   apply clarsimp
113  apply (clarsimp simp:descendants_of_eqv valid_mdb_def)
114  done
115
116lemma dcorres_revoke_cap_unnecessary:
117  "dcorres dc \<top> (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr
118    and cte_at (ptr,tcb_cnode_index 2) and not_idle_thread ptr and valid_idle)
119    (revoke_cap_simple (ptr, tcb_replycap_slot))
120    (return x)"
121  apply (subst transform_tcb_slot_simp[symmetric])
122  apply (rule corres_guard_imp)
123  apply (rule dcorres_revoke_cap_no_descendants)
124  apply (simp add:transform_tcb_slot_simp[symmetric])+
125  apply (rule not_waiting_reply_slot_no_descendants)
126    apply simp_all
127done
128
129lemma descendants_exist_in_cdt:
130  "\<lbrakk> a \<in> descendants_of p (cdt s) \<rbrakk>
131        \<Longrightarrow> cdt s a \<noteq> None"
132  apply (simp add: descendants_of_def cdt_parent_rel_def)
133  apply (frule RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]])
134  apply (clarsimp simp: is_cdt_parent_def)
135  done
136
137lemma descendants_exist_in_cdl_cdt:
138  "\<lbrakk> a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk>
139        \<Longrightarrow> cdl_cdt (transform s) a \<noteq> None"
140  apply (simp add: KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def)
141  apply (frule RangeI)
142  apply (frule DomainI)
143  apply (clarsimp simp: KHeap_D.is_cdt_parent_def)
144done
145
146lemma cdl_cdt_parent_cte_at_lift:
147  "\<lbrakk> mdb_cte_at (swp (cte_wp_at P) s) (cdt s) ; a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk>
148    \<Longrightarrow> (\<exists>slot. cte_at slot s \<and>  p = transform_cslot_ptr slot)"
149  apply (simp add:KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def)
150  apply (frule DomainI)
151  apply (clarsimp simp:KHeap_D.is_cdt_parent_def)
152  apply (simp add:transform_def transform_cdt_def)
153  apply (clarsimp simp:transform_cdt_slot_inj_on_mdb_cte_at map_lift_over_eq_Some split:if_splits)
154  apply (rule_tac x = ab in exI,rule_tac x = bb in exI)
155    apply (drule(1) mdb_cte_atD)
156  apply (clarsimp simp :cte_wp_at_cte_at)
157done
158
159lemma descendants_not_null_cap:
160  "\<lbrakk> a \<in> descendants_of p (cdt s); mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<rbrakk>
161        \<Longrightarrow> cte_wp_at P a s"
162  apply (drule descendants_exist_in_cdt)
163  apply clarsimp
164  apply (drule(1) mdb_cte_atD)
165  apply simp
166  done
167
168lemma descendants_in_cte_wp_set:
169  "mdb_cte_at (swp (cte_wp_at P ) s) (cdt s)
170  \<Longrightarrow> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> Collect (\<lambda>x. cte_wp_at (P) x s)"
171  by (auto simp:descendants_not_null_cap)
172
173lemma ex_in_none_empty_set:
174  "a\<noteq>{} \<Longrightarrow> \<exists>x. x\<in>a"
175  by auto
176
177lemma finite_descendants_if_from_transform:
178  " mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s))"
179  apply (case_tac "KHeap_D.descendants_of x (transform s) = {}")
180   apply simp
181  apply (drule ex_in_none_empty_set)
182  apply clarsimp
183  apply (frule(1) cdl_cdt_parent_cte_at_lift)
184  apply clarsimp
185  apply (frule(1) descendants_of_eqv)
186  apply clarsimp
187  apply (rule finite_imageI)
188  apply (rule finite_subset)
189  apply (rule descendants_in_cte_wp_set)
190    apply simp
191  apply (simp add:cte_wp_at_set_finite)
192done
193
194lemma delete_cdt_slot_shrink_descendants:
195  "\<lbrace>\<lambda>s. valid_mdb s \<and> x = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p x \<and> x = y \<rbrace>
196    set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
197    \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and>
198    CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p y \<rbrace>"
199  apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def)
200  apply (rule conjI)
201    apply (subgoal_tac "mdb_empty_abs s")
202    apply (clarsimp simp:mdb_empty_abs.descendants mdb_empty_abs_def vmdb_abs_def)+
203done
204
205lemma delete_cap_one_shrink_descendants:
206  "\<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace> cap_delete_one slot
207    \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and>
208    CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace>"
209  including no_pre
210  apply (simp add:cap_delete_one_def unless_def)
211  apply wp
212     apply (clarsimp simp add:empty_slot_def)
213     apply (wp dxo_wp_weak)
214         apply simp
215        apply (rule_tac P="\<lambda>s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s)
216          \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
217          in hoare_vcg_precond_imp)
218         apply (rule_tac Q ="\<lambda>r s. Q r s \<and>  (mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))" for Q in hoare_strengthen_post)
219          apply (rule hoare_vcg_conj_lift)
220           apply (rule delete_cdt_slot_shrink_descendants[where y= "cdt pres" and p = p])
221          apply (rule_tac Q="\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s ) xa" in hoare_vcg_precond_imp)
222           apply (case_tac slot)
223           apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def mdb_cte_at_def)
224          apply (assumption)
225         apply clarsimp+
226       apply wp+
227     apply (rule hoare_vcg_conj_lift[where P="\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s) (cdt s)"])
228      prefer 2
229      apply (rule hoare_drop_imp)
230      apply wp
231     apply (clarsimp simp:valid_def in_get_cap_cte_wp_at)
232     apply (drule sym)
233     apply clarsimp
234     apply (drule descendants_not_null_cap)
235      apply simp
236     apply (simp add:cte_wp_at_def)
237    apply (wp|simp)+
238    apply (rule hoare_vcg_conj_lift)
239     apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise])
240     apply (clarsimp simp:valid_mdb_def swp_def)
241    apply wp
242    apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise])
243    apply (clarsimp simp:valid_mdb_def swp_def)
244   apply wp
245  apply (clarsimp simp:valid_def in_get_cap_cte_wp_at)
246  apply (clarsimp simp:invs_def valid_mdb_def valid_state_def)
247  apply (drule descendants_not_null_cap)
248   apply simp
249  apply (clarsimp simp:cte_wp_at_def)
250done
251
252lemma invs_emptyable_descendants:
253  "\<lbrakk>invs s;CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}\<rbrakk>
254              \<Longrightarrow> emptyable (a, b) s"
255  apply (clarsimp simp:emptyable_def)
256  apply (frule reply_slot_not_descendant)
257    apply simp
258  apply fastforce
259done
260
261lemma cap_delete_one_cte_at:
262  "\<lbrace>invs and emptyable sl and cte_at x\<rbrace> cap_delete_one sl \<lbrace>\<lambda>_. cte_at x\<rbrace>"
263  apply (simp add:cap_delete_one_def)
264    apply wp
265    apply (clarsimp simp:unless_def when_def | rule conjI)+
266    apply (wp|clarsimp)+
267done
268
269lemma nat_to_bl_zero_zero:
270  "(nat_to_bl 0 0) = (Some [])"
271  by (clarsimp simp: nat_to_bl_def)
272
273lemma caps_of_state_transform_opt_cap_no_idle:
274  "\<lbrakk>caps_of_state s p = Some cap; valid_etcbs s\<rbrakk>
275   \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s)
276          = Some (transform_cap cap) \<or>
277      opt_cap (transform_cslot_ptr p) (transform s)
278          = None"
279  apply (frule caps_of_state_cteD)
280  apply (cases p)
281  apply (erule cte_wp_atE)
282   apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def object_slots_def
283                         slots_of_def opt_object_def transform_def transform_objects_def
284                         transform_cnode_contents_def well_formed_cnode_n_def
285                         restrict_map_def
286                   split: option.splits if_split_asm nat.splits)
287    apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI])
288    apply (simp add: nat_to_bl_zero_zero option_map_join_def)
289   apply clarsimp
290   apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI])
291   apply (simp add: option_map_join_def nat_to_bl_dest)
292   apply (clarsimp simp: cap_installed_at_irq_def valid_irq_node_def
293                         obj_at_def is_cap_table_def well_formed_cnode_n_def
294                         length_set_helper word_bl.Abs_inverse
295                         object_slots_def nat_bl_to_bin_lt2p)
296  apply (frule(1) valid_etcbs_tcb_etcb)
297  by (clarsimp simp: opt_cap_def transform_cslot_ptr_def
298                        slots_of_def opt_object_def restrict_map_def
299                        transform_def object_slots_def transform_objects_def
300                        valid_irq_node_def obj_at_def is_cap_table_def tcb_cap_cases_def
301                        transform_tcb_def tcb_slot_defs infer_tcb_bound_notification_def
302                        bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
303                 split: if_split_asm option.splits)
304
305lemma transform_cap_Null [simp]:
306  "(transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap)"
307  apply (cases cap, simp_all)
308  apply (rename_tac arch_cap)
309  apply (case_tac arch_cap, simp_all)
310  done
311
312lemma dcorres_revoke_the_cap_corres:
313  "dcorres dc \<top>
314    (invs and cte_at slot and valid_etcbs)
315    (revoke_cap_simple (transform_cslot_ptr slot))
316    (do descs \<leftarrow> gets (CSpaceAcc_A.descendants_of slot \<circ> cdt);
317        when (descs \<noteq> {}) (do y \<leftarrow> assert (\<exists>a b. descs = {(a, b)});
318                          select descs >>= cap_delete_one
319                          od)
320    od)"
321  apply (rule dcorres_revoke_cap_simple_helper)
322  apply (simp add:gets_def)
323  apply (rule dcorres_absorb_get_l)
324  apply (rule dcorres_absorb_get_r)
325  apply (subgoal_tac "finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'))")
326   apply (clarsimp simp: finite_descendants_if_from_transform valid_mdb_def
327                         invs_def valid_state_def descendants_of_eqv)
328   apply (rule dcorres_absorb_get_l)
329   apply (clarsimp simp: when_def assert_def corres_free_fail)
330   apply (subgoal_tac "cte_wp_at ((\<noteq>) cap.NullCap) (a,b) s'")
331    prefer 2
332    apply (erule descendants_not_null_cap [rotated])
333    apply fastforce
334   apply (rule conjI)
335    prefer 2
336    apply (clarsimp simp: cte_wp_at_caps_of_state)
337    apply (subgoal_tac "a \<noteq> idle_thread s'")
338     apply (drule_tac p="(a,b)" in caps_of_state_transform_opt_cap)
339      apply clarsimp
340     apply clarsimp
341    apply clarsimp
342   apply clarsimp
343    apply (erule notE, rule sym)
344    apply (erule (4) valid_idle_has_null_cap)
345   apply clarsimp
346    apply (rule corres_dummy_return_r)
347    apply (rule corres_guard_imp)
348      apply (rule corres_split[OF dcorres_revoke_cap_no_descendants])
349        apply simp
350        apply (rule delete_cap_simple_corres)
351        apply (wp cap_delete_one_cte_at)+
352      apply (rule_tac pres1 = s' and  p1 = slot in hoare_strengthen_post[OF delete_cap_one_shrink_descendants])
353    apply (simp_all add:invs_def valid_state_def valid_mdb_def)
354    apply fastforce
355    apply (rule conjI)
356      apply (rule ccontr)
357      apply (subgoal_tac "cte_wp_at ((\<noteq>)cap.NullCap) (a,b) s")
358        apply (clarsimp simp: cte_wp_at_caps_of_state)
359        apply (drule valid_idle_has_null_cap)
360        apply (simp add:not_idle_thread_def)+
361     apply (rule invs_emptyable_descendants)
362    apply (simp add:invs_def valid_state_def valid_mdb_def)+
363  apply (clarsimp simp:finite_descendants_if_from_transform)
364  done
365
366lemma valid_ntfn_after_remove_slot:
367  "\<lbrakk>valid_ntfn ntfn s'; ntfn_obj ntfn = (Structures_A.ntfn.WaitingNtfn list)\<rbrakk>
368   \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn
369           (case remove1 ptr list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn
370                            | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 ptr list))) s'"
371  apply (clarsimp simp: valid_ntfn_def
372                 split: ntfn.splits list.split_asm list.splits option.splits)
373  by (metis (mono_tags) distinct.simps(2) distinct_length_2_or_more distinct_remove1 set_remove1)
374
375lemma finalise_cancel_ipc:
376  "dcorres dc \<top> (not_idle_thread ptr and invs and valid_etcbs)
377    (CSpace_D.cancel_ipc ptr)
378    (cancel_ipc ptr)"
379  apply (simp add:CSpace_D.cancel_ipc_def cancel_ipc_def get_thread_state_def thread_get_def)
380  apply (rule dcorres_gets_the)
381   apply (simp add:opt_object_tcb not_idle_thread_def transform_tcb_def, clarsimp)
382   apply (frule(1) valid_etcbs_get_tcb_get_etcb)
383   apply (clarsimp simp: opt_cap_tcb tcb_pending_op_slot_def
384                         tcb_caller_slot_def tcb_cspace_slot_def tcb_ipcbuffer_slot_def
385                         tcb_replycap_slot_def tcb_vspace_slot_def assert_opt_def)
386   apply (case_tac "tcb_state obj'")
387          apply (simp_all add:not_idle_thread_def infer_tcb_pending_op_def
388            tcb_pending_op_slot_def[symmetric] tcb_replycap_slot_def[symmetric])
389      apply (simp add:blocked_cancel_ipc_def)
390      apply (rule corres_guard_imp)
391        apply (rule corres_symb_exec_r)
392           apply (rule corres_symb_exec_r)
393              apply (rule corres_symb_exec_r)
394                 apply (rule corres_dummy_return_pl)
395                 apply (rule corres_split[ OF _ corres_dummy_set_sync_ep])
396                   apply clarsimp
397                   apply (rule corres_dummy_return_pr)
398                   apply (rule corres_split [OF _ dcorres_revoke_cap_unnecessary])
399                     apply (simp add: when_def dc_def[symmetric])
400                     apply (rule set_thread_state_corres)
401                    apply (wp sts_only_idle sts_st_tcb_at' valid_ep_queue_subset
402                        | clarsimp simp:not_idle_thread_def a_type_def)+
403          apply (simp add:get_blocking_object_def | wp)+
404      apply (clarsimp dest!:get_tcb_rev simp:invs_def ep_at_def2[symmetric, simplified])
405      apply (frule(1) valid_tcb_if_valid_state)
406      apply (clarsimp simp:valid_tcb_def valid_tcb_state_def
407       valid_state_def valid_pspace_def infer_tcb_pending_op_def
408       st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD)
409      apply (rule tcb_at_cte_at_2,clarsimp simp:tcb_at_def dest!:get_tcb_rev,simp)
410     apply (simp add:blocked_cancel_ipc_def)
411     apply (rule corres_guard_imp)
412       apply (rule corres_symb_exec_r)
413          apply (rule corres_symb_exec_r)
414             apply (rule corres_symb_exec_r)
415                apply (rule corres_dummy_return_pl)
416                apply (rule corres_split[ OF _ corres_dummy_set_sync_ep])
417                  apply clarsimp
418                  apply (rule corres_dummy_return_pr)
419                  apply (rule corres_split [OF _ dcorres_revoke_cap_unnecessary])
420                    unfolding K_bind_def
421                    apply (rule set_thread_state_corres)
422                   apply (wp sts_only_idle sts_st_tcb_at' valid_ep_queue_subset
423                     | clarsimp simp:not_idle_thread_def a_type_def)+
424         apply (simp add:get_blocking_object_def | wp)+
425     apply (clarsimp dest!:get_tcb_rev simp:invs_def ep_at_def2[symmetric, simplified])
426     apply (frule(1) valid_tcb_if_valid_state)
427     apply (clarsimp simp:valid_tcb_def valid_tcb_state_def
428           valid_state_def valid_pspace_def infer_tcb_pending_op_def
429           st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD)
430     apply (rule tcb_at_cte_at_2,clarsimp simp:tcb_at_def dest!:get_tcb_rev,simp)
431    apply (simp add:reply_cancel_ipc_def)
432    apply (rule corres_guard_imp)
433      apply (rule corres_split[OF _ thread_set_fault_corres])
434         apply (rule corres_symb_exec_r)
435            apply (simp add: revoke_cap_simple.simps)
436            apply (subst transform_tcb_slot_simp[symmetric])
437            apply (rule dcorres_revoke_the_cap_corres)
438           apply (wp thread_set_invs_trivial[OF ball_tcb_cap_casesI]
439                     thread_set_cte_at|clarsimp)+
440    apply (clarsimp simp: not_idle_thread_def
441      tcb_at_cte_at_2[unfolded tcb_at_def])
442   apply (simp add:cancel_signal_def)
443   apply (rule corres_guard_imp)
444     apply (rule_tac Q'="\<lambda>r. valid_ntfn r and (=) s'" in corres_symb_exec_r)
445        apply (rule corres_symb_exec_r)
446           apply (rule corres_dummy_return_pl)
447           apply (rule corres_split[ OF _ corres_dummy_set_notification])
448             unfolding K_bind_def
449             apply (rule corres_dummy_return_pr)
450             apply (rule corres_split[OF _ dcorres_revoke_cap_unnecessary])
451               unfolding K_bind_def
452               apply (rule set_thread_state_corres)
453              including no_pre
454              apply (wpsimp wp: set_simple_ko_valid_objs simp: not_idle_thread_def a_type_def)+
455           apply (clarsimp simp:valid_def fail_def return_def split:Structures_A.ntfn.splits)+
456           apply (clarsimp simp:invs_def ntfn_at_def2[symmetric, simplified])
457           apply (frule(1) valid_tcb_if_valid_state)
458           apply (clarsimp simp:valid_tcb_def tcb_at_cte_at_2
459             valid_tcb_state_def invs_def valid_state_def valid_pspace_def
460             st_tcb_at_def generates_pending_def obj_at_def infer_tcb_pending_op_def
461             dest!:get_tcb_SomeD)
462           apply (simp add:valid_ntfn_after_remove_slot)
463          apply (wp | clarsimp split:Structures_A.ntfn.splits)+
464   apply (clarsimp simp:invs_def, frule(1) valid_tcb_if_valid_state)
465   apply (clarsimp simp:valid_tcb_def tcb_at_cte_at_2 valid_tcb_state_def invs_def valid_state_def valid_pspace_def
466        st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD)
467  apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb)
468  apply (clarsimp simp:opt_object_tcb opt_cap_tcb)
469  done
470
471lemma dcorres_get_irq_slot:
472  "dcorres (\<lambda>r r'. r = transform_cslot_ptr r') \<top> \<top> (gets (CSpace_D.get_irq_slot x)) (KHeap_A.get_irq_slot x)"
473  apply (simp add:gets_def CSpace_D.get_irq_slot_def KHeap_A.get_irq_slot_def)
474  apply (rule dcorres_absorb_get_l)
475  apply (rule dcorres_absorb_get_r)
476  apply (clarsimp simp: return_def transform_def corres_underlying_def transform_cslot_ptr_def)
477done
478
479lemma dcorres_deleting_irq_handler:
480  "dcorres dc \<top> (invs and valid_etcbs)
481     (CSpace_D.deleting_irq_handler word)
482     (CSpace_A.deleting_irq_handler word)"
483  apply (simp add:CSpace_D.deleting_irq_handler_def CSpace_A.deleting_irq_handler_def)
484  apply (rule corres_guard_imp)
485  apply (rule corres_split[OF _ dcorres_get_irq_slot])
486    apply (simp, rule delete_cap_simple_corres,simp)
487    apply (rule hoare_vcg_precond_imp [where Q="invs and valid_etcbs"])
488    including no_pre
489    apply (wpsimp simp:get_irq_slot_def)+
490    apply (rule irq_node_image_not_idle)
491    apply (simp add:invs_def valid_state_def)+
492done
493
494lemma do_machine_op_wp:
495  "\<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
496    \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op mop \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>"
497  apply (clarsimp simp:do_machine_op_def gets_def get_def return_def bind_def select_f_def simpler_modify_def)
498  apply (clarsimp simp:valid_def)
499  apply (drule_tac x = "(machine_state s)" in spec)
500  apply (drule_tac x = "(a,b)" in bspec)
501    apply simp
502  apply clarsimp
503  apply (clarsimp simp:transform_def transform_current_thread_def)
504  apply (simp add: transform_objects_def2)
505  done
506
507lemmas dmo_dwp = do_machine_op_wp [OF allI]
508
509lemma machine_op_lift[wp]:
510  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> machine_op_lift x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
511  apply (clarsimp simp:machine_rest_lift_def ignore_failure_def machine_op_lift_def)
512  apply (wpsimp simp:simpler_modify_def valid_def)
513  done
514
515lemma invalidateLocalTLB_ASID_underlying_memory[wp]:
516  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID a \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
517  apply (clarsimp simp: invalidateLocalTLB_ASID_def, wp)
518  done
519
520lemma dsb_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> dsb \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
521  apply (clarsimp simp: dsb_def, wp)
522done
523
524lemma invalidate_I_PoU_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidate_I_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
525  apply (clarsimp simp: invalidate_I_PoU_def , wp)
526done
527
528lemma clean_D_PoU_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>clean_D_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
529  apply (clarsimp simp: clean_D_PoU_def , wp)
530done
531
532lemma cleanCachesPoU_underlying_memory[wp]:
533  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
534   apply (clarsimp simp: cleanCaches_PoU_def, wp)
535done
536
537lemma flush_space_dwp[wp]:
538  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> flush_space x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>"
539  apply (clarsimp simp:flush_space_def)
540  apply (wp|wpc)+
541     apply (clarsimp split:option.splits)
542     apply (rule do_machine_op_wp)
543     apply clarsimp
544     apply (wp static_imp_wp)+
545     apply (rule do_machine_op_wp)
546     apply clarsimp
547     apply wp
548    apply (rule hoare_allI)
549    apply (rule hoare_drop_imp)
550    apply (rule do_machine_op_wp)
551    apply clarsimp
552    apply wp
553   apply (rule hoare_conjI)
554    apply (rule hoare_drop_imp)
555    apply (clarsimp simp:load_hw_asid_def)
556    apply wp
557   apply (clarsimp simp:load_hw_asid_def)
558   apply wp
559  apply assumption
560  done
561
562lemma invalidate_asid_dwp[wp]:
563  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>x ps. transform ps = cs\<rbrace>"
564  apply (clarsimp simp:invalidate_asid_def)
565  apply wp
566  apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
567  done
568
569lemma invalidate_asid_entry_dwp[wp]:
570  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid_entry x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>"
571  apply (clarsimp simp:invalidate_asid_entry_def)
572  apply wp
573     apply (clarsimp simp:invalidate_asid_def)
574     apply wp+
575    apply (clarsimp simp:invalidate_hw_asid_entry_def)
576    apply wp+
577   apply (clarsimp simp:load_hw_asid_def)
578   apply wp
579  apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
580  done
581
582lemma invalidate_hw_asid_entry_dwp[wp]:
583  "\<lbrace>\<lambda>s. transform s = cs\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>"
584  apply (clarsimp simp:invalidate_hw_asid_entry_def)
585  apply wp
586  apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
587done
588
589lemma set_current_pd_dwp[wp]:
590  " \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> set_current_pd (addrFromPPtr x) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
591  by (clarsimp simp:set_current_pd_def writeTTBR0_def isb_def dsb_def,wp)
592
593lemma set_hardware_asid_dwp[wp]:
594  " \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setHardwareASID hw_asid \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
595  by (clarsimp simp:setHardwareASID_def,wp)
596
597
598lemma store_hardware_asid_dwp[wp]:
599  "\<lbrace>\<lambda>s. transform s = cs\<rbrace> store_hw_asid a xa \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>"
600  apply (clarsimp simp:store_hw_asid_def)
601  apply wp
602  apply (simp add:find_pd_for_asid_assert_def)
603  apply wp
604  apply (simp add:find_pd_for_asid_def)
605  apply (wp|wpc)+
606  apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def)
607done
608
609lemma  transform_arch_state:
610  "\<lbrakk> arm_globals_frame (arch_state a) = arm_globals_frame x;
611       arm_asid_table (arch_state a) = arm_asid_table x \<rbrakk>
612    \<Longrightarrow> transform (a\<lparr>arch_state := x \<rparr>) = transform a"
613  by (clarsimp simp:transform_def transform_objects_def2 transform_cdt_def
614    transform_current_thread_def transform_asid_table_def)
615
616lemma find_free_hw_asid_dwp[wp]:
617  "\<lbrace>\<lambda>s. transform s = cs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>xa s. transform s = cs\<rbrace>"
618  apply (clarsimp simp:find_free_hw_asid_def)
619  apply (wp|wpc)+
620  apply (clarsimp simp:transform_arch_state)
621  apply (wp do_machine_op_wp |clarsimp simp:)+
622done
623
624lemma arch_obj_not_idle:
625  "\<lbrakk>valid_idle s;kheap s ptr = Some (ArchObj x )\<rbrakk> \<Longrightarrow> not_idle_thread ptr s"
626  by (clarsimp simp:not_idle_thread_def valid_idle_def obj_at_def pred_tcb_at_def)
627
628lemma asid_pool_at_rev:
629  "\<lbrakk> kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow> asid_pool_at a s"
630  apply (clarsimp simp: obj_at_def valid_idle_def st_tcb_at_def)
631  apply (clarsimp simp: a_type_def
632                 split: arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits)
633  done
634
635lemma asid_pool_not_idle:
636  "\<lbrakk> valid_idle s; asid_pool_at a s \<rbrakk> \<Longrightarrow> not_idle_thread a s"
637  apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def)
638  apply (clarsimp simp: not_idle_thread_def
639                 split: if_splits)
640  done
641
642lemma opt_object_asid_pool:
643  "\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow>
644     opt_object a (transform s) = Some (cdl_object.AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents fun\<rparr>)"
645  apply (frule asid_pool_at_rev)
646  apply (frule(1) asid_pool_not_idle)
647  apply (clarsimp simp:transform_objects_def opt_object_def transform_def
648    not_idle_thread_def restrict_map_def)
649done
650
651lemma transform_asid_pool_contents_upd:
652  "transform_asid_pool_contents (pool(ucast asid := pd)) =
653   transform_asid_pool_contents pool(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)"
654  apply (clarsimp simp:transform_asid_pool_contents_def transform_asid_def)
655  apply (rule ext)
656  apply (case_tac x)
657   apply (clarsimp simp:unat_eq_0 unat_map_def)
658  apply (safe | clarsimp)+
659  apply (safe | clarsimp simp:unat_map_def)+
660  apply (subst (asm) of_nat_Suc[symmetric])
661  apply (rule_tac P="Suc nat = unat (ucast asid)" in notE, simp)
662  apply (cut_tac x="Suc nat" and y="unat (ucast asid :: 10 word)" in word_unat.Abs_inject[symmetric, where 'a=10])
663    apply (simp add:unats_def)+
664   apply (rule unat_lt2p[where x="ucast asid :: 10 word", simplified])
665  apply simp
666  done
667
668lemma dcorres_set_asid_pool:
669  "\<lbrakk> pool' = pool (ucast asid := pd); slot = snd (transform_asid asid);
670     cap = transform_asid_pool_entry pd \<rbrakk> \<Longrightarrow>
671    dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) a)
672    (KHeap_D.set_cap (a, slot) cap)
673    (set_asid_pool a pool')"
674  apply (simp add:KHeap_D.set_cap_def set_asid_pool_def get_object_def gets_the_def
675                  gets_def bind_assoc)
676  apply (rule dcorres_absorb_get_l)
677  apply (clarsimp simp:obj_at_def opt_object_asid_pool assert_opt_def has_slots_def)
678  apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def
679                       corres_underlying_def update_slots_def return_def object_slots_def)
680  apply (clarsimp simp:KHeap_A.set_object_def get_def put_def bind_def return_def)
681  apply (clarsimp simp:transform_def transform_current_thread_def)
682  apply (drule(1) arch_obj_not_idle)
683  apply (rule ext)
684  apply (clarsimp simp:not_idle_thread_def transform_objects_def restrict_map_def map_add_def)
685  apply (rule transform_asid_pool_contents_upd)
686  done
687
688lemma dcorres_set_vm_root:
689  "dcorres dc \<top> \<top> (return x) (set_vm_root rvd)"
690  apply (clarsimp simp: set_vm_root_def)
691  apply (rule dcorres_symb_exec_r)+
692    apply (clarsimp simp:catch_def throwError_def)
693    apply (rule corres_dummy_return_r)
694    apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]])+
695     apply wp+
696      apply wpc
697       apply (wp do_machine_op_wp | clarsimp)+
698     apply (rule_tac Q = "\<lambda>_ s. transform s = cs" in hoare_post_imp)
699      apply simp
700     apply (wpsimp wp: hoare_whenE_wp do_machine_op_wp [OF allI] hoare_drop_imps find_pd_for_asid_inv
701                simp: arm_context_switch_def get_hw_asid_def load_hw_asid_def if_apply_def2)+
702  done
703
704lemma dcorres_delete_asid_pool:
705  "dcorres dc \<top> \<top>
706    (CSpace_D.delete_asid_pool (unat (asid_high_bits_of asid)) oid)
707    (ARM_A.delete_asid_pool asid oid)"
708  apply (simp add:CSpace_D.delete_asid_pool_def ARM_A.delete_asid_pool_def)
709  apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified])
710   apply (clarsimp simp:gets_def)
711   apply (rule dcorres_absorb_get_r)
712   apply (clarsimp simp:when_def)
713   apply (rule conjI)
714    prefer 2
715    apply (clarsimp, rule corres_alternate2)
716    apply (clarsimp)
717   apply clarsimp
718   apply (rule corres_alternate1)
719   apply (rule dcorres_absorb_get_l)
720   apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified])
721    apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified])
722     apply (rule corres_dummy_return_l)
723     apply (rule corres_underlying_split[where r'=dc and P="\<lambda>rv. \<top>" and P'="\<lambda>rv. \<top>", simplified])
724      prefer 2
725      apply clarsimp
726      apply (rule dcorres_absorb_get_r)
727      apply (rule corres_guard_imp)
728        apply (rule dcorres_set_vm_root)
729       apply clarsimp+
730     apply (rule corres_guard_imp[where Q=\<top> and Q'=\<top>, simplified])
731     apply (clarsimp simp:simpler_modify_def put_def bind_def corres_underlying_def)
732     apply (clarsimp simp:transform_def transform_objects_def transform_cdt_def
733                          transform_current_thread_def)
734     apply (clarsimp simp:transform_asid_table_def)
735     apply (rule ext)
736     apply (clarsimp simp:unat_map_def asid_high_bits_of_def
737                          transform_asid_table_entry_def transform_asid_def)
738     apply safe
739       apply (drule unat_cong)
740       apply (subst (asm) word_unat.Abs_inverse)
741        apply (clarsimp simp:unats_def unat_ucast)+
742    apply (rule mapM_wp)
743     apply clarsimp
744     apply wp
745    apply fastforce
746   apply wpsimp+
747done
748
749lemma descendants_of_page:
750  "\<lbrakk>valid_mdb s;page_table_at oid s\<rbrakk>\<Longrightarrow> KHeap_D.descendants_of (oid, 0) (transform s) = {}"
751  apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def)
752  apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits)
753  apply (rule ccontr)
754  apply (clarsimp simp:valid_mdb_def dest!:not_emptyI)
755  apply (frule(1) cdl_cdt_parent_cte_at_lift)
756  apply clarsimp
757  apply (simp add:descendants_of_eqv cte_at_cases)
758  apply (clarsimp simp:transform_cslot_ptr_def)
759done
760
761lemma page_table_aligned:
762  "\<lbrakk>pspace_aligned s;page_table_at oid s\<rbrakk> \<Longrightarrow>
763         (oid && ~~ mask pt_bits) = oid"
764  apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def)
765  apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits)
766  apply (drule_tac x = oid in bspec)
767    apply clarsimp
768  apply (clarsimp simp:obj_bits_def arch_kobj_size_def pt_bits_def pageBits_def)
769done
770
771lemma invalidateLocalTLB_VAASID_underlying_memory[wp]:
772  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_VAASID word \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
773  by (clarsimp simp: invalidateLocalTLB_VAASID_def, wp)
774
775lemma dcorres_flush_page:
776  "dcorres dc \<top> \<top>  (return x) (flush_page aa a b word)"
777  apply (rule corres_dummy_return_r)
778  apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]])
779   apply wp
780  apply (simp add:flush_page_def)
781  apply wp
782        apply (rule dcorres_to_wp[OF dcorres_set_vm_root])
783       apply wp
784      apply clarsimp
785      apply (wp do_machine_op_wp, clarsimp)
786      apply (wp)
787     apply (simp add:load_hw_asid_def)
788     apply wp
789    apply (clarsimp simp:set_vm_root_for_flush_def)
790    apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+
791         apply (wpc)
792          apply wp+
793        apply (rule hoare_conjI,rule hoare_drop_imp)
794         apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+
795      apply (wpc|wp)+
796     apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post)
797      apply (wp|clarsimp)+
798done
799
800lemma dcorres_flush_table:
801  "dcorres dc \<top> \<top>  (return x) (flush_table aa a b word)"
802  apply (rule corres_dummy_return_r)
803  apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]])
804   apply wp
805  apply (simp add:flush_table_def)
806  apply wp
807        apply (rule dcorres_to_wp[OF dcorres_set_vm_root])
808       apply wp
809      apply clarsimp
810      apply (wp do_machine_op_wp|clarsimp)+
811     apply (clarsimp simp:load_hw_asid_def)
812     apply wp
813    apply (clarsimp simp:set_vm_root_for_flush_def)
814    apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+
815         apply wpc
816          apply wp+
817        apply (rule hoare_conjI,rule hoare_drop_imp)
818         apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+
819      apply (wpc|wp)+
820     apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post)
821      apply (wp|clarsimp)+
822done
823
824lemma flush_table_exec:
825  "\<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow>dcorres dc R P h ((flush_table aa a b word) >>= g)"
826  apply (rule corres_dummy_return_pl)
827  apply (rule corres_guard_imp)
828  apply (rule corres_split[OF _ dcorres_flush_table])
829  apply (simp|wp)+
830  done
831
832
833lemma transform_cap_not_new_invented:
834  "transform_cap z \<noteq> cdl_cap.PageTableCap word Fake asid"
835  by (auto simp:transform_cap_def split:arch_cap.splits cap.splits)
836
837lemma page_table_not_idle:
838  "\<lbrakk>valid_idle s;page_table_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s"
839  apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def)
840  apply (clarsimp simp: not_idle_thread_def split: if_splits)
841  done
842
843lemma page_directory_not_idle:
844  "\<lbrakk>valid_idle s;page_directory_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s"
845  apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def)
846  apply (clarsimp simp: not_idle_thread_def split: if_splits)
847  done
848
849lemma page_table_at_rev:
850  "\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> page_table_at a s"
851  apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def)
852  apply (clarsimp simp:a_type_def split: if_splits)
853  done
854
855lemma page_directory_at_rev:
856  "\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> \<Longrightarrow> page_directory_at a s"
857  apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def)
858  apply (clarsimp simp:a_type_def split: if_splits)
859  done
860
861lemma mask_pd_bits_less':
862  "uint ((ptr::word32) && mask pd_bits >> (2::nat)) < (4096::int)"
863  apply (clarsimp simp:pd_bits_def pageBits_def)
864  using shiftr_less_t2n'[where m = 12 and x ="(ptr && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
865  apply (clarsimp simp:mask_twice)
866  done
867
868lemma mask_pd_bits_less:
869  "nat (uint ((y::word32) && mask pd_bits >> 2)) < 4096"
870  apply (clarsimp simp:pd_bits_def pageBits_def)
871  apply (rule iffD2[OF nat_less_eq_zless[where z = 4096,simplified]])
872  apply (simp)
873  using shiftr_less_t2n'[where m = 12 and x ="(y && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
874  apply (clarsimp simp:mask_twice)
875done
876
877lemma mask_pt_bits_less':
878  "uint (((ptr::word32) && mask pt_bits) >> 2)< 256"
879  apply (clarsimp simp:pt_bits_def pageBits_def)
880  using shiftr_less_t2n'[where m = 8 and x ="(ptr && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
881  apply (clarsimp simp:mask_twice )
882done
883
884lemma mask_pt_bits_less:
885  "nat (uint ((y::word32) && mask pt_bits >> 2)) < 256"
886  apply (clarsimp simp:pt_bits_def pageBits_def)
887  apply (rule iffD2[OF nat_less_eq_zless[where z = 256,simplified]])
888  apply (simp)
889  using shiftr_less_t2n'[where m = 8 and x ="(y && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
890  apply (clarsimp simp:mask_twice)
891done
892
893definition pd_pt_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
894where "pd_pt_relation pd pt offset s \<equiv>
895  \<exists>fun u v ref. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
896  \<and> page_table_at pt s \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.PageTablePDE ref u v
897  \<and> pt = ptrFromPAddr ref )"
898
899definition pd_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
900where "pd_section_relation pd pt offset s \<equiv>
901  \<exists>fun u v ref1 ref2. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
902  \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.SectionPDE ref1 u ref2 v
903  \<and> pt = ptrFromPAddr ref1 )"
904
905definition pd_super_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
906where "pd_super_section_relation pd pt offset s \<equiv>
907  \<exists>fun u v ref1. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
908  \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.SuperSectionPDE ref1 u v
909  \<and> pt = ptrFromPAddr ref1 )"
910
911definition pt_page_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>vmpage_size set\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
912where "pt_page_relation pt page offset S s \<equiv>
913  \<exists>fun. (kheap s pt = Some (ArchObj (arch_kernel_obj.PageTable fun)))
914  \<and> (case fun (ucast (offset && mask pt_bits >> 2)) of
915    ARM_A.pte.LargePagePTE ref fun1 fun2 \<Rightarrow>
916        page = ptrFromPAddr ref \<and> ARMLargePage \<in> S
917  | ARM_A.pte.SmallPagePTE ref fun1 fun2 \<Rightarrow>
918        page = ptrFromPAddr ref \<and> ARMSmallPage \<in> S
919  | _ \<Rightarrow> False)"
920
921lemma slot_with_pt_frame_relation:
922  "\<lbrakk>valid_idle s;pt_page_relation a oid y S s\<rbrakk>\<Longrightarrow>
923    (a, nat (uint (y && mask pt_bits >> 2))) \<in>
924    ((slots_with (\<lambda>x. \<exists>rights sz asid. x = FrameCap False oid rights sz Fake asid)) (transform s))"
925  apply (clarsimp simp:pt_page_relation_def)
926  apply (frule page_table_at_rev)
927  apply (frule(1) page_table_not_idle)
928  apply (clarsimp simp:slots_with_def transform_def transform_objects_def restrict_map_def)
929  apply (clarsimp simp:not_idle_thread_def has_slots_def object_slots_def)
930  apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def)
931  apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] )
932  apply (clarsimp simp:mask_pt_bits_less split:ARM_A.pte.split_asm)
933done
934
935lemma below_kernel_base:
936  "ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
937    \<Longrightarrow> kernel_pde_mask f (of_nat (unat (y && mask pd_bits >> 2)))
938    = f (of_nat (unat (y && mask pd_bits >> 2)))"
939  apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )
940  apply (simp add:ucast_nat_def[symmetric] unat_def)
941done
942
943(* we need an int version for 2016 *)
944lemma below_kernel_base_int:
945  "ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
946    \<Longrightarrow> kernel_pde_mask f (of_int (uint (y && mask pd_bits >> 2)))
947    = f (of_int (uint (y && mask pd_bits >> 2)))"
948  apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )
949  apply (simp add:ucast_nat_def[symmetric] unat_def)
950done
951
952lemma slot_with_pd_pt_relation:
953  "\<lbrakk>valid_idle s; pd_pt_relation a b y s; ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
954  (a, unat (y && mask pd_bits >> 2)) \<in>
955    (slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap b Fake asid)) (transform s)"
956  apply (clarsimp simp :pd_pt_relation_def)
957  apply (frule page_directory_at_rev)
958  apply (frule(1) page_directory_not_idle)
959  apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
960  apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def)
961  apply (clarsimp simp:has_slots_def object_slots_def)
962  apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
963  apply (clarsimp simp:ucast_def)
964  apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def below_kernel_base)
965  apply (simp add:mask_pd_bits_less)
966done
967
968lemma slot_with_pd_section_relation:
969  "\<lbrakk>valid_idle s; pd_super_section_relation a b y s \<or> pd_section_relation a b y s;
970    ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
971  (a, unat (y && mask pd_bits >> 2)) \<in>
972    (slots_with (\<lambda>x. \<exists>rights sz asid. x = cdl_cap.FrameCap False b rights sz Fake asid)) (transform s)"
973  apply (erule disjE)
974    apply (clarsimp simp :pd_super_section_relation_def)
975    apply (frule page_directory_at_rev)
976    apply (frule(1) page_directory_not_idle)
977    apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
978    apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def)
979    apply (clarsimp simp:has_slots_def object_slots_def)
980    apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
981    apply (clarsimp simp:ucast_def)
982    apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def mask_pd_bits_less)
983  apply (clarsimp simp :pd_section_relation_def)
984  apply (frule page_directory_at_rev)
985  apply (frule(1) page_directory_not_idle)
986  apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
987  apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def)
988  apply (clarsimp simp:has_slots_def object_slots_def)
989  apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
990  apply (clarsimp simp:ucast_def)
991  apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def)
992  apply (simp add:mask_pd_bits_less)
993done
994
995lemma opt_cap_page_table:"\<lbrakk>valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
996(opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s))
997  = Some (cdl_cap.PageTableCap pt_id Fake None)"
998  apply (clarsimp simp:pd_pt_relation_def opt_cap_def transform_def unat_def slots_of_def opt_object_def)
999  apply (frule page_directory_at_rev)
1000  apply (frule(1) page_directory_not_idle)
1001  apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
1002    restrict_map_def object_slots_def)
1003  apply (clarsimp simp:transform_page_directory_contents_def unat_def[symmetric] unat_map_def | rule conjI )+
1004    apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def)
1005  apply (clarsimp simp:below_kernel_base)
1006    apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] unat_def ucast_def)
1007  apply (simp add:mask_pd_bits_less unat_def)
1008done
1009
1010lemma opt_cap_page:"\<lbrakk>valid_idle s;pt_page_relation a pg x S s \<rbrakk>\<Longrightarrow>
1011\<exists>f sz. (opt_cap (a, unat (x && mask pt_bits >> 2) ) (transform s))
1012  = Some (cdl_cap.FrameCap False pg f sz Fake None)"
1013  apply (clarsimp simp:pt_page_relation_def unat_def opt_cap_def transform_def slots_of_def opt_object_def)
1014  apply (frule page_table_at_rev)
1015  apply (frule(1) page_table_not_idle)
1016  apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
1017    restrict_map_def object_slots_def)
1018  apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI )+
1019    apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def)
1020    apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ucast_def mask_pt_bits_less)+
1021    apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def)
1022done
1023
1024lemma opt_cap_section:
1025  "\<lbrakk>valid_idle s;pd_section_relation a pg x s \<or> pd_super_section_relation a pg x s;
1026    ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
1027  \<exists>f sz. (opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s))
1028    = Some (cdl_cap.FrameCap False pg f sz Fake None)"
1029  unfolding unat_def
1030  apply (erule disjE)
1031
1032    apply (clarsimp simp: pd_section_relation_def opt_cap_def transform_def slots_of_def opt_object_def)
1033    apply (frule page_directory_at_rev)
1034    apply (frule(1) page_directory_not_idle)
1035    apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
1036    restrict_map_def object_slots_def)
1037    apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+
1038      apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base_int)
1039      apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+
1040    apply (simp add:mask_pd_bits_less)
1041  apply (clarsimp simp:pd_super_section_relation_def opt_cap_def transform_def slots_of_def opt_object_def)
1042  apply (frule page_directory_at_rev)
1043  apply (frule(1) page_directory_not_idle)
1044  apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
1045    restrict_map_def object_slots_def)
1046  apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+
1047  apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base_int)
1048  apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+
1049  apply (simp add:mask_pd_bits_less)
1050done
1051
1052lemma opt_object_page_table:"\<lbrakk>valid_idle s;kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk>
1053\<Longrightarrow>opt_object a (transform s) =
1054  Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>)"
1055  apply (frule page_table_at_rev)
1056  apply (frule(1) page_table_not_idle)
1057  apply (clarsimp simp:transform_objects_def opt_object_def transform_def
1058    not_idle_thread_def restrict_map_def)
1059done
1060
1061lemma opt_object_page_directory:"\<lbrakk>valid_idle s;kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk>
1062\<Longrightarrow>opt_object a (transform s) =
1063  Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>)"
1064  apply (frule page_directory_at_rev)
1065  apply (frule(1) page_directory_not_idle)
1066  apply (clarsimp simp:transform_objects_def opt_object_def transform_def
1067    not_idle_thread_def restrict_map_def)
1068done
1069
1070lemma remove_cdt_pt_slot_exec:
1071  "\<lbrakk>dcorres dc \<top> Q (g ()) f;
1072   \<And>s. Q s\<longrightarrow> ( (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and pt_page_relation a pg_id ptr UNIV) s\<rbrakk>
1073    \<Longrightarrow> dcorres dc P Q
1074    (remove_parent (a ,aptr) >>= g) f"
1075  apply (rule corres_dummy_return_pr)
1076  apply (rule corres_guard_imp)
1077  apply (rule corres_split[OF _ dummy_remove_cdt_pt_slot])
1078    apply (rule_tac F="rv = ()" in corres_gen_asm)
1079    unfolding K_bind_def
1080    apply clarsimp
1081  apply (assumption)
1082  apply (simp|wp)+
1083  apply (drule_tac x = s in meta_spec)
1084  apply (clarsimp simp:pt_page_relation_def dest!:page_table_at_rev)
1085done
1086
1087lemma remove_cdt_pd_slot_exec:
1088  "\<lbrakk>dcorres dc \<top> Q (g ()) f;
1089   \<And>s. Q s\<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and page_directory_at a) s\<rbrakk>
1090    \<Longrightarrow> dcorres dc P Q
1091    (remove_parent (a ,aptr) >>= g) f"
1092  apply (rule corres_dummy_return_pr)
1093  apply (rule corres_guard_imp)
1094  apply (rule corres_split[OF _ dummy_remove_cdt_pd_slot])
1095    unfolding K_bind_def
1096  apply (simp|wp)+
1097done
1098
1099lemma remove_cdt_asid_pool_slot_exec:
1100  "\<lbrakk>dcorres dc \<top> Q (g ()) f;
1101   \<And>s. Q s\<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and asid_pool_at a) s\<rbrakk>
1102    \<Longrightarrow> dcorres dc P Q
1103    (remove_parent (a ,aptr) >>= g) f"
1104  apply (rule corres_dummy_return_pr)
1105  apply (rule corres_guard_imp)
1106  apply (rule corres_split[OF _ dummy_remove_cdt_asid_pool_slot])
1107    unfolding K_bind_def
1108  apply (simp|wp)+
1109done
1110
1111lemma dcorres_set_pte_cap:
1112  "\<lbrakk> (x::word32) = (ptr && mask pt_bits >> 2);pte_cap = transform_pte a_pte\<rbrakk>\<Longrightarrow>
1113    dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.PageTable fun)) a )
1114    (KHeap_D.set_cap (a, unat (ptr && mask pt_bits >> 2)) pte_cap)
1115    (KHeap_A.set_object a
1116      (ArchObj (arch_kernel_obj.PageTable (fun(ucast (ptr && mask pt_bits >> 2) := a_pte)))))"
1117  apply (simp add:KHeap_D.set_cap_def KHeap_A.set_object_def gets_the_def gets_def bind_assoc unat_def)
1118  apply (rule dcorres_absorb_get_r)
1119  apply (rule dcorres_absorb_get_l)
1120  apply (clarsimp simp:obj_at_def opt_object_page_table assert_opt_def has_slots_def object_slots_def)
1121  apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def
1122                       corres_underlying_def update_slots_def return_def object_slots_def)
1123  apply (rule sym)
1124  apply (clarsimp simp:transform_def transform_current_thread_def)
1125  apply (rule ext)
1126  apply (clarsimp | rule conjI)+
1127    apply (frule page_table_at_rev)
1128    apply (frule(1) page_table_not_idle)
1129    apply (clarsimp simp:transform_objects_def not_idle_thread_def)
1130    apply (rule ext)
1131      apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def)
1132      apply (clarsimp simp:word_of_int word_of_nat mask_pt_bits_less mask_pt_bits_less' ucast_def)
1133        apply (subst (asm) word_of_int_inj)
1134        apply (clarsimp simp:mask_pt_bits_less')+
1135    apply (clarsimp simp:uint_nat)
1136  apply clarify
1137  apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def)
1138done
1139
1140lemma dcorres_delete_cap_simple_set_pt:
1141  "dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))
1142       and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV
1143       and valid_idle and ko_at (ArchObj (arch_kernel_obj.PageTable fun)) (ptr && ~~ mask pt_bits))
1144    (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)))
1145    (set_pt (ptr && ~~ mask pt_bits) (fun(ucast (ptr && mask pt_bits >> 2) := ARM_A.pte.InvalidPTE)))"
1146  apply (simp add:delete_cap_simple_def set_pt_def gets_the_def gets_def bind_assoc get_object_def)
1147  apply (rule dcorres_absorb_get_l)
1148  apply (rule dcorres_absorb_get_r)
1149  apply (clarsimp simp:assert_def corres_free_fail
1150    split:Structures_A.kernel_object.split_asm arch_kernel_obj.splits)
1151  apply (frule opt_cap_page)
1152    apply (simp add:)+
1153  apply (clarsimp simp:gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def)
1154  apply (rule dcorres_absorb_get_l)
1155  apply (clarsimp simp: always_empty_slot_def gets_the_def gets_def bind_assoc)
1156  apply (rule remove_cdt_pt_slot_exec[where pg_id = pg_id])
1157   apply (rule corres_guard_imp)
1158     apply (rule dcorres_set_pte_cap)
1159      apply (simp add:transform_pte_def)+
1160  apply clarsimp
1161  apply simp
1162  done
1163
1164
1165lemma transform_page_table_contents_upd:
1166  "transform_page_table_contents fun(unat (y && mask pt_bits >> 2) \<mapsto> transform_pte pte) =
1167            transform_page_table_contents
1168             (fun(ucast ((y::word32) && mask pt_bits >> 2) := pte))"
1169  apply (rule ext)
1170  apply (clarsimp simp:transform_page_table_contents_def unat_map_def )
1171  apply (clarsimp simp:ucast_nat_def[symmetric])
1172  apply (subgoal_tac "unat (y && mask pt_bits >> 2) < 256")
1173  apply (rule conjI|clarsimp)+
1174    apply (drule word_unat.Abs_eqD)
1175     apply (simp add: unats_def)+
1176  apply (rule unat_less_helper)
1177  apply (subst shiftr_div_2n_w)
1178  apply (clarsimp simp:word_size)+
1179  apply (rule word_div_mult,simp)
1180  apply (clarsimp simp:pt_bits_def pageBits_def)
1181  apply (rule and_mask_less_size[where n = 10,simplified],simp add:word_size)
1182done
1183
1184lemma transform_page_directory_contents_upd:
1185  "ucast ((ptr::word32) && mask pd_bits >> 2) \<notin> kernel_mapping_slots
1186  \<Longrightarrow> transform_page_directory_contents f(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)
1187   =  transform_page_directory_contents (f(ucast (ptr && mask pd_bits >> 2) := a_pde))"
1188  apply (rule ext)
1189    apply (simp (no_asm) add:transform_page_directory_contents_def unat_map_def)
1190    apply (simp add:below_kernel_base)
1191      apply (clarsimp simp: unat_def mask_pd_bits_less|rule conjI)+
1192      apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def)
1193      apply (clarsimp simp:ucast_nat_def[symmetric])
1194      apply (drule sym)
1195      apply (drule word_unat.Abs_eqD)
1196        apply (simp add:unats_def unat_def[symmetric])+
1197      apply (rule unat_less_helper)
1198      apply (subst shiftr_div_2n_w,(simp add:word_size)+)
1199      apply (rule word_div_mult,simp)
1200      apply (clarsimp simp:pt_bits_def pd_bits_def pageBits_def)
1201      apply (rule and_mask_less_size[where n = 14,simplified],simp add:word_size)
1202    apply (simp add:word_of_int unat_def)
1203    apply (clarsimp simp:ucast_def word_of_int_nat[OF uint_ge_0,simplified])
1204done
1205
1206lemma dcorres_set_pde_cap:
1207  "\<lbrakk> (x::word32) = (ptr && mask pd_bits >> 2);pde_cap = transform_pde a_pde; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
1208    dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.PageDirectory fun)) a )
1209      (KHeap_D.set_cap (a, unat x) pde_cap)
1210      (KHeap_A.set_object a (ArchObj
1211                 (arch_kernel_obj.PageDirectory (fun(ucast x := a_pde)))))"
1212  apply (simp add:KHeap_D.set_cap_def KHeap_A.set_object_def gets_the_def gets_def bind_assoc)
1213  apply (rule dcorres_absorb_get_r)
1214  apply (rule dcorres_absorb_get_l)
1215  apply (clarsimp simp:obj_at_def opt_object_page_directory assert_opt_def has_slots_def object_slots_def)
1216  apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def corres_underlying_def update_slots_def object_slots_def return_def)
1217  apply (clarsimp simp:transform_def transform_current_thread_def)
1218    apply (rule ext)
1219    apply (clarsimp | rule conjI)+
1220      apply (frule page_directory_at_rev)
1221      apply (frule(1) page_directory_not_idle)
1222      apply (clarsimp simp:transform_objects_def not_idle_thread_def)
1223      apply (rule sym)
1224      apply (erule transform_page_directory_contents_upd)
1225   apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def)
1226done
1227
1228lemma dcorres_delete_cap_simple_set_pde:
1229  " ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
1230    \<Longrightarrow>dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))
1231    and (pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr
1232         or pd_section_relation (ptr && ~~ mask pd_bits) oid ptr
1233         or pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr)
1234    and valid_idle and ko_at (ArchObj (arch_kernel_obj.PageDirectory fun)) (ptr && ~~ mask pd_bits))
1235             (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)))
1236             (set_pd (ptr && ~~ mask pd_bits) (fun(ucast (ptr && mask pd_bits >> 2) := ARM_A.pde.InvalidPDE)))"
1237  apply (simp add:delete_cap_simple_def set_pd_def gets_the_def gets_def bind_assoc get_object_def)
1238  apply (rule dcorres_absorb_get_l)
1239  apply (rule dcorres_absorb_get_r)
1240  apply (clarsimp simp:assert_def corres_free_fail
1241    split:Structures_A.kernel_object.split_asm arch_kernel_obj.splits)
1242  apply (erule disjE)
1243    apply (frule opt_cap_page_table,simp+)
1244    apply (clarsimp simp:gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def)
1245    apply (rule dcorres_absorb_get_l)
1246    apply (clarsimp simp:always_empty_slot_def gets_the_def gets_def bind_assoc)
1247    apply (rule remove_cdt_pd_slot_exec)
1248      apply (rule corres_guard_imp)
1249      apply (rule dcorres_set_pde_cap)
1250    apply (simp add:transform_pte_def)+
1251    apply (clarsimp simp:pd_pt_relation_def transform_pde_def)+
1252    apply (rule page_directory_at_rev)
1253    apply simp
1254  apply (frule opt_cap_section,simp+)
1255    apply (clarsimp simp:gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def)
1256    apply (rule dcorres_absorb_get_l)
1257    apply (clarsimp simp:always_empty_slot_def gets_the_def gets_def bind_assoc)
1258    apply (rule remove_cdt_pd_slot_exec)
1259      apply (rule corres_guard_imp)
1260      apply (rule dcorres_set_pde_cap)
1261    apply simp+
1262    apply (clarsimp simp:pd_pt_relation_def transform_pde_def)+
1263    apply (rule page_directory_at_rev)
1264    apply simp
1265done
1266
1267lemma dcorres_lookup_pd_slot:
1268  "is_aligned pd 14
1269  \<Longrightarrow> (cdl_lookup_pd_slot pd vptr =  transform_pd_slot_ref (lookup_pd_slot pd vptr))"
1270  apply (clarsimp simp:cdl_lookup_pd_slot_def
1271     transform_pd_slot_ref_def lookup_pd_slot_def)
1272  by (simp add:vaddr_segment_nonsense vaddr_segment_nonsense2)
1273
1274
1275lemma dcorres_delete_cap_simple_section:
1276  "dcorres dc \<top> (invs and pd_section_relation (lookup_pd_slot pd v && ~~ mask pd_bits) oid
1277                    (lookup_pd_slot pd v) and  K (is_aligned pd pd_bits \<and> v < kernel_base))
1278           (delete_cap_simple (cdl_lookup_pd_slot pd v))
1279           (store_pde (lookup_pd_slot pd v) ARM_A.pde.InvalidPDE)"
1280  apply (clarsimp simp: store_pde_def transform_pd_slot_ref_def lookup_pd_slot_def)
1281  apply (rule corres_gen_asm2)
1282  apply (subst dcorres_lookup_pd_slot, simp add: pd_bits_def pageBits_def)
1283  apply (clarsimp simp: transform_pd_slot_ref_def lookup_pd_slot_def)
1284  apply (rule corres_guard_imp)
1285    apply (rule corres_symb_exec_r)
1286       apply (rule dcorres_delete_cap_simple_set_pde[where oid = oid])
1287       apply (drule(1) less_kernel_base_mapping_slots)
1288       apply (simp add: lookup_pd_slot_def)
1289      apply wpsimp+
1290  apply fastforce
1291  done
1292
1293lemma large_frame_range_helper:
1294  fixes t :: word32
1295  shows
1296  "t \<in> set [0 , 4 .e. 0x3C] \<Longrightarrow> t < 0x40"
1297  apply (clarsimp simp: upto_enum_step_def)
1298  apply (subgoal_tac "x < 0x10")
1299    apply (subst mult.commute)
1300    apply (subst shiftl_t2n[where n =2,simplified,symmetric])
1301    apply (rule shiftl_less_t2n[where m = 6 and n =2,simplified])
1302       apply simp+
1303    apply (rule le_less_trans)
1304    apply simp+
1305done
1306
1307lemma zip_map_eqv:
1308  "(y, x) \<in> set (zip (map g xs) (map f xs)) = (\<exists>t. (y = g t \<and> x = f t \<and> t \<in> set xs))"
1309  apply (clarsimp simp:zip_map1 zip_map2)
1310  apply (rule iffI)
1311   apply (fastforce simp: in_set_zip)
1312  apply (clarsimp simp:set_zip_same)
1313  using imageI[where f ="(\<lambda>(a, b). (a, f b)) \<circ> (\<lambda>(x, y). (g x, y))",simplified]
1314  apply clarify
1315  apply (drule_tac x = t in meta_spec)
1316  apply (drule_tac x = t in meta_spec)
1317  apply (drule_tac x = "Id \<inter> (set xs) \<times> (set xs) " in meta_spec)
1318  apply clarsimp
1319done
1320
1321lemma page_directory_address_eq:
1322  fixes ptr :: word32
1323  shows
1324  "\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits"
1325  apply (drule large_frame_range_helper)
1326  using mask_lower_twice[where m = 14 and n = 6 and x= ptr,symmetric]
1327  apply (clarsimp simp:pd_bits_def pageBits_def)
1328  using mask_lower_twice[where m = 14 and n = 6 and x= "ptr+t",symmetric]
1329  apply (clarsimp simp:pd_bits_def pageBits_def)
1330  apply (subgoal_tac "(ptr && ~~ mask 6)  = (ptr + t && ~~ mask 6)")
1331    apply simp
1332  apply (frule is_aligned_neg_mask_eq)
1333    apply simp
1334  apply (drule_tac q = t in mask_out_add_aligned)
1335  apply (subst(asm) less_mask_eq [THEN mask_eq_x_eq_0[THEN iffD1]], erule order_less_le_trans)
1336  apply clarsimp+
1337done
1338
1339lemma page_table_address_eq:
1340  fixes ptr :: word32
1341  shows
1342  "\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr + t && ~~ mask pt_bits"
1343  apply (drule large_frame_range_helper)
1344  using mask_lower_twice[where m = 10 and n = 6 and x= ptr,symmetric]
1345  apply (clarsimp simp:pt_bits_def pageBits_def)
1346  using mask_lower_twice[where m = 10 and n = 6 and x= "ptr+t",symmetric]
1347  apply (clarsimp simp:pt_bits_def pageBits_def)
1348  apply (subgoal_tac "(ptr && ~~ mask 6)  = (ptr + t && ~~ mask 6)")
1349    apply simp
1350  apply (frule is_aligned_neg_mask_eq)
1351    apply simp
1352  apply (drule_tac q = t in mask_out_add_aligned)
1353  apply (subst(asm) less_mask_eq [THEN mask_eq_x_eq_0[THEN iffD1]], erule order_less_le_trans)
1354  apply clarsimp+
1355done
1356
1357lemma shiftl_inj_if:
1358  "\<lbrakk>(shiftl a n) = (shiftl b n); shiftr (shiftl a n) n = a; shiftr (shiftl b n) n = b\<rbrakk> \<Longrightarrow> a = b"
1359 apply (drule arg_cong[where f = "\<lambda>x. shiftr x n"])
1360 apply (rule box_equals)
1361 defer
1362 apply (assumption)+
1363done
1364
1365lemma ucast_inj_mask:
1366  "((ucast (x::'a::len word)) :: ('b::len word)) = ((ucast (y::'a::len word)) :: ('b::len word))
1367    \<Longrightarrow> (x && mask (len_of TYPE('b))) = (y && mask (len_of TYPE('b)))"
1368  apply (simp add:ucast_def)
1369  apply (simp add:word_ubin.inverse_norm)
1370  apply (simp add:word_ubin.eq_norm)
1371  apply (simp add:and_mask_bintr)
1372done
1373
1374lemma split_word_noteq_on_mask:
1375  "(x \<noteq> y)  =  (x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k)"
1376  apply (rule iffI)
1377  using split_word_eq_on_mask[symmetric]
1378  apply auto
1379done
1380
1381lemma test_bits_mask:
1382  "\<lbrakk>x && mask l = y && mask l;na < size x; size x = size y\<rbrakk>
1383  \<Longrightarrow> na<l \<longrightarrow> x !! na = y !! na"
1384  apply (drule word_eqD)
1385  apply (auto simp:word_size)
1386done
1387
1388lemma test_bits_neg_mask:
1389  "\<lbrakk>x && ~~ mask l = y && ~~ mask l;na < size x; size x = size y\<rbrakk>
1390  \<Longrightarrow> l\<le> na \<longrightarrow> x !! na = y !! na"
1391  apply (drule word_eqD)
1392  apply (auto simp:word_size neg_mask_bang)
1393done
1394
1395lemma mask_compare_imply:
1396  "\<lbrakk> (x && mask k >> l) && mask n = (y && mask k >> l) && mask n;size x= size y; k\<le> size x; l+n \<le> k; x\<noteq>y\<rbrakk>
1397    \<Longrightarrow> (x && mask l \<noteq>y && mask l) \<or> (x && ~~ mask (l+n)) \<noteq> (y && ~~ mask (l+n))"
1398  apply (rule ccontr)
1399  apply (subgoal_tac "x = y")
1400   apply simp
1401  apply (rule word_eqI)
1402  apply clarsimp
1403  apply (case_tac "na<l")
1404   apply (drule_tac na = na in test_bits_mask[where l = l and y = y])
1405     apply clarsimp+
1406  apply (case_tac "l+n\<le> na")
1407   apply (drule_tac na = na in test_bits_neg_mask)
1408     apply clarsimp+
1409  apply (drule_tac na = "na-l" in test_bits_mask)
1410    apply (clarsimp simp: linorder_not_le)
1411    apply (subst (asm) add.commute[where a = l])+
1412    apply (drule nat_diff_less)
1413     apply (clarsimp simp:word_size)+
1414  apply (clarsimp simp:nth_shiftr)
1415  apply (auto simp:word_size)
1416done
1417
1418lemma aligned_in_step_up_to:
1419  "\<lbrakk>x\<in> set (map (\<lambda>x. x + ptr) [0 , (2^t) .e. up]); t < word_bits; is_aligned ptr t\<rbrakk>
1420  \<Longrightarrow> is_aligned x t"
1421  apply (clarsimp simp:upto_enum_step_def image_def)
1422  apply (rule aligned_add_aligned[where n = t])
1423    apply (rule is_aligned_mult_triv2)
1424   apply (simp add:word_bits_def)+
1425done
1426
1427lemma remain_pt_pd_relation:
1428  "\<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr\<notin> ys\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace>
1429    store_pte ptr sp
1430   \<lbrace>\<lambda>r s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace>"
1431  apply (rule hoare_vcg_const_Ball_lift)
1432  apply (subgoal_tac "ptr\<noteq> y")
1433   apply (simp add:store_pte_def)
1434   apply wp
1435     apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits)
1436                and  pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_vcg_precond_imp)
1437      apply (clarsimp simp:set_pt_def)
1438      apply wp
1439        apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits)
1440                     and  pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_vcg_precond_imp)
1441         apply (clarsimp simp:valid_def set_object_def in_monad)
1442         apply (drule_tac x= y in bspec,simp)
1443         apply (clarsimp simp:pt_page_relation_def dest!: ucast_inj_mask| rule conjI)+
1444          apply (drule mask_compare_imply)
1445              apply ((simp add:word_size pt_bits_def pageBits_def is_aligned_mask)+)
1446
1447         apply (clarsimp simp:pt_page_relation_def obj_at_def)
1448        apply (assumption)
1449       apply wp
1450      apply (simp add:get_object_def)
1451      apply wp
1452      apply (clarsimp simp:obj_at_def)+
1453     apply (assumption)
1454    apply wp
1455   apply (clarsimp simp:obj_at_def pt_page_relation_def)+
1456  done
1457
1458lemma remain_pd_section_relation:
1459  "\<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk>
1460   \<Longrightarrow> \<lbrace>\<lambda>s. pd_section_relation ( y && ~~ mask pd_bits) sid y s\<rbrace> store_pde ptr sp
1461       \<lbrace>\<lambda>r s. pd_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>"
1462  apply (simp add:store_pde_def)
1463  apply wp
1464    apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
1465                  and pd_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp)
1466     apply (clarsimp simp:set_pd_def)
1467     apply wp
1468       apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
1469                  and pd_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp)
1470        apply (clarsimp simp:valid_def set_object_def in_monad)
1471        apply (clarsimp simp:pd_section_relation_def dest!:ucast_inj_mask | rule conjI)+
1472         apply (drule mask_compare_imply)
1473             apply (simp add:word_size pd_bits_def pt_bits_def pageBits_def is_aligned_mask)+
1474        apply (clarsimp simp:pt_page_relation_def obj_at_def)
1475       apply (assumption)
1476      apply wp
1477     apply (simp add:get_object_def)
1478     apply wp
1479     apply (clarsimp simp:obj_at_def)+
1480    apply (assumption)
1481   apply wp
1482  apply (clarsimp simp:obj_at_def pt_page_relation_def)+
1483done
1484
1485lemma remain_pd_super_section_relation:
1486  "\<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk>
1487   \<Longrightarrow> \<lbrace>\<lambda>s. pd_super_section_relation ( y && ~~ mask pd_bits) sid y s\<rbrace> store_pde ptr sp
1488       \<lbrace>\<lambda>r s. pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>"
1489  apply (simp add:store_pde_def)
1490  apply wp
1491    apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
1492               and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp)
1493     apply (clarsimp simp:set_pd_def)
1494     apply wp
1495       apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
1496                 and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp)
1497        apply (clarsimp simp:valid_def set_object_def in_monad)
1498        apply (clarsimp simp:pd_super_section_relation_def dest!:ucast_inj_mask | rule conjI)+
1499         apply (drule mask_compare_imply)
1500             apply (simp add:word_size pd_bits_def pt_bits_def pageBits_def is_aligned_mask)+
1501        apply (clarsimp simp:pt_page_relation_def obj_at_def)
1502       apply (assumption)
1503      apply wp
1504     apply (simp add:get_object_def)
1505     apply wp
1506     apply (clarsimp simp:obj_at_def)+
1507    apply (assumption)
1508   apply wp
1509  apply (clarsimp simp:obj_at_def pt_page_relation_def)
1510  done
1511
1512lemma remain_pd_either_section_relation:
1513  "\<lbrakk>\<forall>y \<in> set ys. is_aligned y 2;ptr\<notin> set ys;is_aligned ptr 2\<rbrakk>
1514   \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in> set ys. (pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or>
1515    pd_section_relation (y && ~~ mask pd_bits) pg_id y s) \<rbrace>
1516    store_pde ptr ARM_A.pde.InvalidPDE
1517   \<lbrace>\<lambda>r s. \<forall>y\<in>set ys.
1518     (pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or>
1519     pd_section_relation (y && ~~ mask pd_bits) pg_id y s)\<rbrace>"
1520  including no_pre
1521  apply (rule hoare_vcg_const_Ball_lift)
1522  apply (wp hoare_vcg_disj_lift)
1523   apply (rule hoare_strengthen_post[OF remain_pd_super_section_relation]; fastforce)
1524  apply (rule hoare_strengthen_post[OF remain_pd_section_relation]; fastforce)
1525  done
1526
1527lemma is_aligned_less_kernel_base_helper:
1528  "\<lbrakk>is_aligned (ptr :: word32) 6;
1529    ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; x < 0x40 \<rbrakk>
1530   \<Longrightarrow> ucast (x + ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots"
1531  apply (simp add: kernel_mapping_slots_def)
1532  apply (simp add: word_le_nat_alt shiftr_20_unat_ucast
1533                   unat_ucast_pd_bits_shift)
1534  apply (fold word_le_nat_alt, unfold linorder_not_le)
1535  apply (drule minus_one_helper3[where x=x])
1536  apply (subst add.commute, subst is_aligned_add_or, assumption)
1537   apply (erule order_le_less_trans, simp)
1538  apply (simp add: word_ao_dist shiftr_over_or_dist)
1539  apply (subst less_mask_eq, erule order_le_less_trans)
1540   apply (simp add: pd_bits_def pageBits_def)
1541  apply (subst is_aligned_add_or[symmetric])
1542    apply (rule_tac n=4 in is_aligned_shiftr)
1543    apply (simp add: is_aligned_andI1)
1544   apply (rule shiftr_less_t2n)
1545   apply (erule order_le_less_trans, simp)
1546  apply (rule aligned_add_offset_less)
1547     apply (rule_tac n=4 in is_aligned_shiftr)
1548     apply (simp add: is_aligned_andI1)
1549    apply (simp add: kernel_base_def is_aligned_def)
1550   apply assumption
1551  apply (rule shiftr_less_t2n)
1552  apply (erule order_le_less_trans)
1553  apply simp
1554  done
1555
1556lemma neg_aligned_less_kernel_base_helper:
1557  "\<lbrakk> is_aligned (ptr :: word32) 6;
1558  ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots;
1559              y - ptr < 0x40 \<rbrakk>
1560   \<Longrightarrow> ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots"
1561  by (drule(2) is_aligned_less_kernel_base_helper, simp)
1562
1563lemma mapM_Cons_split:
1564  "xs \<noteq> [] \<Longrightarrow> (mapM f xs) = (do y \<leftarrow> f (hd xs); ys \<leftarrow> mapM f (tl xs); return (y # ys) od)"
1565  by (clarsimp simp:neq_Nil_conv mapM_Cons)
1566
1567lemma dcorres_store_invalid_pde_super_section:
1568  "dcorres dc \<top> (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr
1569   and invs
1570   and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
1571  (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)))
1572  (store_pde ptr ARM_A.pde.InvalidPDE)"
1573  apply simp
1574  apply (rule corres_gen_asm2)
1575  apply (rule corres_guard_imp)
1576    apply (simp add:store_pde_def)
1577    apply (rule corres_symb_exec_r)
1578       apply (rule dcorres_delete_cap_simple_set_pde[where oid = pg_id])
1579       apply simp
1580      apply (wp|simp)+
1581  apply (clarsimp simp: invs_def valid_mdb_def valid_state_def valid_pspace_def)
1582  done
1583
1584lemma dcorres_store_invalid_pte:
1585  "dcorres dc \<top> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV
1586   and invs )
1587  (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)))
1588  (store_pte ptr ARM_A.pte.InvalidPTE)"
1589  apply (rule corres_guard_imp)
1590    apply (simp add:store_pte_def)
1591    apply (rule corres_symb_exec_r)
1592       apply (rule dcorres_delete_cap_simple_set_pt[where pg_id = pg_id])
1593      apply (wp|simp)+
1594  apply (clarsimp simp: invs_def valid_mdb_def valid_state_def valid_pspace_def)
1595  done
1596
1597lemma dcorres_store_pde_non_sense:
1598  "dcorres dc \<top> (valid_idle and
1599     (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
1600     \<and> (f (ucast (slot && mask pd_bits >> 2)) = pde)))
1601  (return a) (store_pde slot pde)"
1602  apply (simp add:store_pde_def)
1603  apply (simp add:get_pd_def bind_assoc get_object_def set_pd_def gets_def)
1604  apply (rule dcorres_absorb_get_r)
1605  apply (clarsimp simp add:assert_def corres_free_fail
1606                  split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
1607  apply (rule dcorres_absorb_get_r)
1608  apply (clarsimp simp:corres_free_fail
1609                  split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
1610  apply (simp add:set_object_def put_def)
1611  apply (rule dcorres_absorb_get_r)
1612  apply (simp add:corres_underlying_def return_def transform_def transform_current_thread_def)
1613  apply (frule page_directory_at_rev)
1614  apply (drule(1) page_directory_not_idle[rotated])
1615  apply (rule ext)+
1616  apply (simp add:transform_objects_def not_idle_thread_def obj_at_def)
1617  done
1618
1619lemma dcorres_store_pte_non_sense:
1620  "dcorres dc \<top> (valid_idle and
1621     (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
1622      \<and> (f (ucast (slot && mask pt_bits >> 2)) = pte)))
1623  (return a) (store_pte slot pte)"
1624  apply (simp add:store_pte_def)
1625  apply (simp add:get_pt_def bind_assoc get_object_def set_pt_def gets_def)
1626  apply (rule dcorres_absorb_get_r)
1627  apply (clarsimp simp add:assert_def corres_free_fail
1628                  split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
1629  apply (rule dcorres_absorb_get_r)
1630  apply (clarsimp simp:corres_free_fail
1631                  split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
1632  apply (simp add:set_object_def put_def)
1633  apply (rule dcorres_absorb_get_r)
1634  apply (simp add:corres_underlying_def return_def transform_def transform_current_thread_def)
1635  apply (frule page_table_at_rev)
1636  apply (drule(1) page_table_not_idle[rotated])
1637  apply (rule ext)+
1638  apply (simp add:transform_objects_def not_idle_thread_def obj_at_def)
1639  done
1640
1641lemma store_pde_non_sense_wp:
1642  "\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
1643    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE)) \<rbrace>
1644  store_pde x ARM_A.pde.InvalidPDE
1645   \<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
1646    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE))\<rbrace>"
1647  apply (simp add:store_pde_def get_object_def get_pde_def set_pd_def set_object_def)
1648  apply wp
1649  apply (clarsimp simp:obj_at_def split:Structures_A.kernel_object.splits)
1650  done
1651
1652lemma dcorres_store_invalid_pde_tail_super_section:
1653  "dcorres dc \<top> (valid_idle and
1654    (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
1655    \<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE))
1656    and K (\<forall>sl\<in> set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits))
1657  (return a)
1658  (mapM (swp store_pde ARM_A.pde.InvalidPDE) slots)"
1659  proof (induct slots arbitrary:a)
1660    case Nil
1661    show ?case
1662      by (simp add:mapM_Nil)
1663  next
1664  case (Cons x xs)
1665  show ?case
1666   apply (rule corres_guard_imp)
1667     apply (simp add:mapM_Cons dc_def[symmetric])
1668     apply (rule corres_dummy_return_l)
1669     apply (rule corres_split[OF _ dcorres_store_pde_non_sense])
1670       apply (rule corres_dummy_return_l)
1671       apply (rule corres_split[OF _  Cons.hyps[unfolded swp_def]])
1672         apply (rule corres_free_return[where P=\<top> and P'=\<top>])
1673        apply wp+
1674     apply simp
1675     apply (wp store_pde_non_sense_wp)
1676    apply simp
1677   apply (clarsimp simp:obj_at_def)
1678  done
1679qed
1680
1681lemma store_pte_non_sense_wp:
1682  "\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
1683    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE)) \<rbrace>
1684  store_pte x ARM_A.pte.InvalidPTE
1685   \<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
1686    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE))\<rbrace>"
1687  apply (simp add:store_pte_def get_object_def get_pte_def set_pt_def set_object_def)
1688  apply wp
1689  apply (clarsimp simp:obj_at_def split: Structures_A.kernel_object.splits)
1690  done
1691
1692lemma dcorres_store_invalid_pte_tail_large_page:
1693  "dcorres dc \<top> (valid_idle and
1694    (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
1695    \<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE))
1696    and K (\<forall>sl\<in> set slots. sl && ~~ mask pt_bits = slot && ~~ mask pt_bits))
1697  (return a)
1698  (mapM (swp store_pte ARM_A.pte.InvalidPTE) slots)"
1699  proof (induct slots arbitrary:a)
1700    case Nil
1701    show ?case
1702      by (simp add:mapM_Nil)
1703  next
1704  case (Cons x xs)
1705  show ?case
1706   apply (rule corres_guard_imp)
1707     apply (simp add:mapM_Cons dc_def[symmetric])
1708     apply (rule corres_dummy_return_l)
1709     apply (rule corres_split[OF _ dcorres_store_pte_non_sense])
1710       apply (rule corres_dummy_return_l)
1711       apply (rule corres_split[OF _  Cons.hyps[unfolded swp_def]])
1712         apply (rule corres_free_return[where P=\<top> and P'=\<top>])
1713        apply wp+
1714     apply simp
1715     apply (wp store_pte_non_sense_wp)
1716    apply simp
1717   apply (clarsimp simp:obj_at_def)
1718  done
1719qed
1720
1721lemma and_mask_plus:
1722  "\<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^m\<rbrakk>
1723   \<Longrightarrow> (ptr::word32) + a && mask n = (ptr && mask n) + a"
1724  apply (rule mask_eqI[where n = m])
1725   apply (simp add:mask_twice min_def)
1726    apply (simp add:is_aligned_add_helper)
1727    apply (subst is_aligned_add_helper[THEN conjunct1])
1728      apply (erule is_aligned_after_mask)
1729     apply simp
1730    apply simp
1731   apply simp
1732  apply (subgoal_tac "(ptr + a && mask n) && ~~ mask m
1733     = (ptr + a && ~~ mask m ) && mask n")
1734   apply (simp add:is_aligned_add_helper)
1735   apply (subst is_aligned_add_helper[THEN conjunct2])
1736     apply (simp add:is_aligned_after_mask)
1737    apply simp
1738   apply simp
1739  apply (simp add:word_bw_comms word_bw_lcs)
1740  done
1741
1742lemma dcorres_unmap_large_section:
1743  "\<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14;
1744    v < kernel_base \<rbrakk>
1745  \<Longrightarrow> dcorres dc \<top>
1746     (invs and valid_pdpt_objs
1747           and (pd_super_section_relation ((lookup_pd_slot ptr v) && ~~ mask pd_bits)
1748               pg_id (lookup_pd_slot ptr v)))
1749     (delete_cap_simple (cdl_lookup_pd_slot ptr v))
1750     (mapM (swp store_pde ARM_A.pde.InvalidPDE)
1751           (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]))"
1752  supply is_aligned_neg_mask_eq[simp del] is_aligned_neg_mask_weaken[simp del]
1753  apply (subst mapM_Cons_split)
1754   apply (simp add:upto_enum_step_def upto_enum_def)
1755  apply (simp add:store_pte_def PageTableUnmap_D.unmap_page_def)
1756  apply (rule corres_dummy_return_l)
1757  apply (simp add: upto_enum_step_def transform_pt_slot_ref_def upto_enum_def hd_map_simp
1758                   dcorres_lookup_pd_slot)+
1759  apply (rule corres_guard_imp)
1760    apply (simp add:transform_pd_slot_ref_def)
1761    apply (rule corres_dummy_return_l)
1762    apply (rule corres_split[OF _ dcorres_store_invalid_pde_super_section[where pg_id = pg_id]])
1763      apply(rule corres_dummy_return_l)
1764      apply (rule_tac r'=dc in corres_split[OF corres_free_return[where P=\<top> and P'=\<top>]])
1765        apply (rule dcorres_store_invalid_pde_tail_super_section[where slot = ptr])
1766       apply wp+
1767    apply (wp store_pde_non_sense_wp)
1768   apply simp
1769  apply (simp add: hd_map_simp upto_enum_step_def upto_enum_def drop_map)
1770  apply (rule conjI)
1771   apply (rule less_kernel_base_mapping_slots)
1772    apply (simp add:pd_bits_def pageBits_def)+
1773  apply (rule conjI, fastforce) \<comment> \<open>valid_idle\<close>
1774  apply (rule conj_comms[THEN iffD1])
1775  apply (rule context_conjI)
1776   apply (clarsimp simp: tl_map tl_upt)
1777   apply (clarsimp simp: field_simps)
1778   apply (subst mask_lower_twice[symmetric,where n = 6])
1779    apply (simp add:pd_bits_def pageBits_def)
1780   apply (subst is_aligned_add_helper)
1781     apply (erule(1) lookup_pd_slot_aligned_6)
1782    apply (simp add:upto_0_to_n)
1783    apply (rule word_less_power_trans_ofnat[where k = 2 and m = 6,simplified])
1784     apply simp
1785    apply simp
1786   apply (simp add: lookup_pd_slot_def is_aligned_neg_mask_eq
1787                    pd_shifting[unfolded pd_bits_def pageBits_def,simplified])
1788  apply (clarsimp simp:pd_super_section_relation_def obj_at_def)
1789  apply (simp add: lookup_pd_slot_pd[unfolded pd_bits_def pageBits_def,simplified]
1790                   is_aligned_neg_mask_eq pd_shifting[unfolded pd_bits_def pageBits_def,simplified])
1791  apply (rule ballI, drule (1) bspec)
1792  supply is_aligned_neg_mask2[simp del]
1793  apply (clarsimp simp: upto_0_to_n tl_map)
1794  apply (frule (1) lookup_pd_slot_aligned_6[unfolded pd_bits_def pageBits_def,simplified])
1795  apply (drule(1) valid_pdpt_objs_pdD)
1796  apply clarsimp
1797  apply (frule (1) lookup_pd_slot_aligned_6[unfolded pd_bits_def pageBits_def,simplified])
1798  apply (rename_tac pd rights attr ref s slot)
1799  apply (drule_tac x = "(ucast (lookup_pd_slot ptr v + of_nat slot * 4 && mask pd_bits >> 2))"
1800               and y = "ucast (lookup_pd_slot ptr v && mask pd_bits >> 2)"
1801                in valid_entriesD[rotated])
1802   apply (rule ccontr)
1803   apply simp
1804   apply (drule_tac x="ucast v" for v in arg_cong[where f = "ucast::(12 word\<Rightarrow>word32)"])
1805   apply (drule_tac x="ucast v" for v in arg_cong[where f = "\<lambda>x. shiftl x 2"])
1806   apply (subst (asm) ucast_ucast_len)
1807    apply (rule shiftr_less_t2n)
1808    apply (rule less_le_trans[OF and_mask_less'])
1809     apply (simp add:pd_bits_def pageBits_def)
1810    apply (simp add:pd_bits_def pageBits_def)
1811   apply (subst (asm) ucast_ucast_len)
1812    apply (rule shiftr_less_t2n)
1813    apply (rule less_le_trans[OF and_mask_less'])
1814     apply (simp add:pd_bits_def pageBits_def)
1815    apply (simp add:pd_bits_def pageBits_def)
1816   apply (simp add:shiftr_shiftl1)
1817   apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
1818    apply (erule is_aligned_andI1[OF aligned_add_aligned])
1819     apply (simp add: shiftl_t2n[symmetric,where n =2, simplified field_simps,simplified]
1820                      is_aligned_shiftl_self)
1821    apply simp
1822   apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
1823    apply (erule is_aligned_andI1[OF is_aligned_weaken])
1824    apply simp
1825   apply (subst (asm) and_mask_plus)
1826       apply (erule lookup_pd_slot_aligned_6, simp)
1827      apply (simp add:pd_bits_def pageBits_def)+
1828    apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified])
1829    apply (rule shiftl_less_t2n[where m = 6,simplified])
1830     apply (simp add:word_of_nat_less)
1831    apply simp
1832   apply simp
1833   apply (subgoal_tac "0 < (of_nat (slot * 4)::word32)")
1834    apply simp
1835   apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]])
1836     apply fastforce
1837    apply simp
1838   apply fastforce
1839  apply (rule ccontr)
1840  apply (erule_tac x = "ucast (lookup_pd_slot ptr v + of_nat slot * 4 && mask pd_bits >> 2)"
1841                   in in_empty_interE)
1842   apply (rule non_invalid_in_pde_range)
1843   apply (simp add: pd_bits_def pageBits_def field_simps)
1844  apply (simp add: ucast_neg_mask)
1845  apply (simp add:is_aligned_shiftr)
1846  apply (rule arg_cong[where f = ucast])
1847  apply (rule shiftr_eq_neg_mask_eq)
1848  apply (simp add:shiftr_shiftr shiftr_over_and_dist)
1849  apply (subst aligned_shift')
1850     apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified])
1851     apply (rule shiftl_less_t2n[where m = 6,simplified])
1852      apply (simp add:word_of_nat_less)
1853     apply simp+
1854  done
1855
1856lemma pt_page_relation_weaken:
1857  "\<lbrakk> pt_page_relation a b c S s; S \<subseteq> T \<rbrakk> \<Longrightarrow> pt_page_relation a b c T s"
1858  apply (clarsimp simp: pt_page_relation_def)
1859  apply (auto split: ARM_A.pte.split)
1860  done
1861
1862lemma pt_page_relation_univ:
1863  "pt_page_relation a b c {ARMLargePage} s
1864  \<Longrightarrow> pt_page_relation a b c UNIV s"
1865  apply (clarsimp simp:pt_page_relation_def)
1866  apply (clarsimp split: ARM_A.pte.splits)
1867  done
1868
1869lemma dcorres_unmap_large_page:
1870  "is_aligned ptr 6
1871    \<Longrightarrow> dcorres dc \<top> (invs and valid_pdpt_objs
1872          and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage})
1873     (delete_cap_simple (transform_pt_slot_ref ptr))
1874     (mapM (swp store_pte ARM_A.pte.InvalidPTE) (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]))"
1875  supply is_aligned_neg_mask_eq[simp del]
1876         is_aligned_neg_mask_weaken[simp del]
1877  apply (subst mapM_Cons_split)
1878   apply (simp add:upto_enum_step_def upto_enum_def)
1879  apply (simp add: PageTableUnmap_D.unmap_page_def)
1880  apply (rule corres_dummy_return_l)
1881  apply (simp add:upto_enum_step_def transform_pt_slot_ref_def upto_enum_def hd_map_simp)+
1882  apply (rule corres_guard_imp)
1883    apply(rule corres_dummy_return_l)
1884    apply (rule corres_split[OF _ dcorres_store_invalid_pte[where pg_id = pg_id]])
1885      apply(rule corres_dummy_return_l)
1886      apply (rule_tac r'=dc in corres_split[OF corres_free_return[where P=\<top> and P'=\<top>]])
1887        apply (rule dcorres_store_invalid_pte_tail_large_page[where slot = ptr])
1888       apply wp+
1889    apply (wp store_pte_non_sense_wp)
1890   apply simp
1891  apply (clarsimp simp:unat_def pt_page_relation_univ)
1892  apply (rule conjI,fastforce)
1893  apply (rule conj_comms[THEN iffD1])
1894  apply (rule context_conjI)
1895   apply (clarsimp simp:tl_map drop_map tl_upt)
1896   apply (simp add:field_simps)
1897   apply (subst mask_lower_twice[symmetric,where n = 6])
1898    apply (simp add:pt_bits_def pageBits_def)
1899   apply (subst is_aligned_add_helper)
1900     apply simp
1901    apply (simp add:upto_0_to_n)
1902    apply (rule word_less_power_trans_ofnat[where k = 2 and m = 6,simplified])
1903     apply simp
1904    apply simp
1905   apply simp
1906  apply (clarsimp simp:pt_page_relation_def obj_at_def)
1907  apply (drule(1) bspec)
1908  apply (clarsimp simp:tl_map drop_map upto_0_to_n)
1909  apply (simp add: field_simps)
1910  apply (drule(1) valid_pdpt_objs_ptD,clarify)
1911  apply (drule_tac x = "(ucast (ptr + of_nat x * 4 && mask pt_bits >> 2))"
1912               and y = "ucast (ptr && mask pt_bits >> 2)"
1913                in valid_entriesD[rotated])
1914   apply (rule ccontr)
1915   apply simp
1916   apply (drule_tac x="ucast v" for v in arg_cong[where f = "ucast::(word8\<Rightarrow>word32)"])
1917   apply (drule_tac x="ucast v" for v in arg_cong[where f = "\<lambda>x. shiftl x 2"])
1918   apply (subst (asm) ucast_ucast_len)
1919    apply (rule shiftr_less_t2n)
1920    apply (rule less_le_trans[OF and_mask_less'])
1921     apply (simp add:pt_bits_def pageBits_def)
1922    apply (simp add:pt_bits_def pageBits_def)
1923   apply (subst (asm) ucast_ucast_len)
1924    apply (rule shiftr_less_t2n)
1925    apply (rule less_le_trans[OF and_mask_less'])
1926     apply (simp add:pt_bits_def pageBits_def)
1927    apply (simp add:pt_bits_def pageBits_def)
1928   apply (simp add:shiftr_shiftl1)
1929   apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
1930    apply (erule is_aligned_andI1[OF aligned_add_aligned])
1931     apply (simp add: shiftl_t2n[symmetric, where n=2, simplified field_simps, simplified]
1932                      is_aligned_shiftl_self)
1933    apply simp
1934   apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
1935    apply (erule is_aligned_andI1[OF is_aligned_weaken])
1936    apply simp
1937   apply (subst (asm) and_mask_plus)
1938       apply simp
1939      apply (simp add:pt_bits_def pageBits_def)+
1940    apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified])
1941    apply (rule shiftl_less_t2n[where m = 6,simplified])
1942     apply (simp add:word_of_nat_less)
1943    apply simp
1944   apply simp
1945   apply (subgoal_tac "0 < (of_nat (x * 4)::word32)")
1946    apply simp
1947   apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]])
1948     apply fastforce
1949    apply simp
1950   apply fastforce
1951  apply (clarsimp split:if_splits pte.split_asm)
1952   apply (rule ccontr)
1953   apply (erule_tac x = "ucast (ptr + of_nat x * 4 && mask pt_bits >> 2)" in in_empty_interE)
1954    apply (rule non_invalid_in_pte_range)
1955    apply simp
1956   apply (simp add: ucast_neg_mask)
1957   apply (rule arg_cong[where f = ucast])
1958   apply (rule shiftr_eq_neg_mask_eq)
1959   apply (simp add:shiftr_shiftr shiftr_over_and_dist)
1960   apply (subst aligned_shift')
1961      apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified])
1962      apply (rule shiftl_less_t2n[where m = 6,simplified])
1963       apply (simp add:word_of_nat_less)
1964      apply (simp+)[4]
1965  apply (simp add: is_aligned_shiftr)
1966  done
1967
1968end
1969
1970lemma (in pspace_update_eq) pd_pt_relation_update[iff]:
1971  "pd_pt_relation a b c (f s) = pd_pt_relation a b c s"
1972  by (simp add: pd_pt_relation_def pspace)
1973
1974context begin interpretation Arch . (*FIXME: arch_split*)
1975
1976crunch cdt[wp] :flush_page "\<lambda>s. P (cdt s)"
1977  (wp: crunch_wps simp:crunch_simps)
1978
1979crunch valid_idle[wp]: flush_page "valid_idle"
1980  (wp: crunch_wps simp:crunch_simps)
1981
1982lemma mdb_cte_at_flush_page[wp]:
1983  "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> flush_page a b c d
1984   \<lbrace>\<lambda>_ s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>"
1985  apply (simp add:mdb_cte_at_def)
1986  apply (simp only: imp_conv_disj)
1987  apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift)
1988  done
1989
1990crunch pd_pt_relation[wp]: flush_table "pd_pt_relation a b c"
1991  (wp: crunch_wps simp: crunch_simps)
1992
1993crunch valid_idle[wp]: flush_table "valid_idle"
1994  (wp: crunch_wps simp:crunch_simps)
1995
1996crunch valid_idle[wp]: page_table_mapped "valid_idle"
1997  (wp: crunch_wps simp:crunch_simps)
1998
1999crunch valid_idle[wp]: invalidate_asid_entry "valid_idle"
2000  (wp: crunch_wps simp:crunch_simps)
2001
2002crunch valid_idle[wp]: flush_space "valid_idle"
2003  (wp: crunch_wps simp:crunch_simps)
2004
2005lemma page_table_mapped_stable[wp]:
2006  "\<lbrace>(=) s\<rbrace> page_table_mapped a b w \<lbrace>\<lambda>r. (=) s\<rbrace>"
2007  apply (simp add:page_table_mapped_def)
2008  apply (wp|wpc)+
2009  apply (simp add:get_pde_def)
2010  apply wp
2011  apply (simp add:find_pd_for_asid_def)
2012  apply (wp|wpc)+
2013  apply clarsimp
2014done
2015
2016lemma eqv_imply_stable:
2017assumes "\<And>cs. \<lbrace>(=) cs\<rbrace> f \<lbrace>\<lambda>r. (=) cs\<rbrace>"
2018shows "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace>"
2019  using assms
2020  apply (fastforce simp:valid_def)
2021done
2022
2023lemma check_mapping_pptr_pt_relation:
2024  "\<lbrace>\<lambda>s. vmpage_size \<in> S\<rbrace> check_mapping_pptr w vmpage_size (Inl b)
2025            \<lbrace>\<lambda>r s. r \<longrightarrow> pt_page_relation (b && ~~ mask pt_bits) w b S s\<rbrace>"
2026  apply (simp add:check_mapping_pptr_def get_pte_def)
2027  apply (rule hoare_pre, wp get_pte_wp)
2028  apply (clarsimp simp: obj_at_def)
2029  apply (clarsimp simp: pt_page_relation_def)
2030  apply (simp split: ARM_A.pte.split_asm)
2031  done
2032
2033lemma check_mapping_pptr_section_relation:
2034  "\<lbrace>\<top>\<rbrace> check_mapping_pptr w ARMSection (Inr (lookup_pd_slot rv' b))
2035   \<lbrace>\<lambda>rv s. rv \<longrightarrow>
2036    pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>"
2037  apply (rule hoare_vcg_precond_imp)
2038   apply (simp add:check_mapping_pptr_def)
2039   apply (wp get_pde_wp)
2040  apply (clarsimp simp: obj_at_def)
2041  apply (clarsimp simp: pd_section_relation_def pd_super_section_relation_def
2042                 split: ARM_A.pde.split_asm)
2043done
2044
2045lemma check_mapping_pptr_super_section_relation:
2046  "\<lbrace>\<top>\<rbrace> check_mapping_pptr w ARMSuperSection (Inr (lookup_pd_slot rv' b))
2047   \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>"
2048  apply (rule hoare_vcg_precond_imp)
2049   apply (simp add:check_mapping_pptr_def)
2050   apply (wp get_pde_wp)
2051  apply (clarsimp simp: obj_at_def)
2052  apply (clarsimp simp: pd_section_relation_def pd_super_section_relation_def
2053                 split: ARM_A.pde.split_asm)
2054done
2055
2056lemma lookup_pt_slot_aligned:
2057  "\<lbrace>invs and \<exists>\<rhd> pd and K (is_aligned pd pd_bits \<and> is_aligned vptr 16 \<and> vptr < kernel_base)\<rbrace>
2058        lookup_pt_slot pd vptr \<lbrace>\<lambda>rb s. is_aligned rb 6\<rbrace>, -"
2059  apply (rule hoare_gen_asmE)+
2060  apply (rule hoare_pre, rule hoare_post_imp_R, rule lookup_pt_slot_cap_to)
2061   apply auto
2062  done
2063
2064lemma get_pde_pd_relation:
2065  "\<lbrace>P\<rbrace> get_pde x
2066           \<lbrace>\<lambda>r s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (x && ~~ mask pd_bits) s
2067           \<and> r = f (ucast (x && mask pd_bits >> 2))\<rbrace>"
2068  apply (simp add:get_pde_def)
2069  apply wp
2070  apply (clarsimp simp:obj_at_def)
2071done
2072
2073lemma pd_pt_relation_page_table_mapped_wp:
2074  "\<lbrace>page_table_at w\<rbrace> page_table_mapped a b w
2075      \<lbrace>\<lambda>r s. (case r of Some pd \<Rightarrow> pd_pt_relation
2076    (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s | _ \<Rightarrow> True)\<rbrace>"
2077  apply (simp add:page_table_mapped_def)
2078  apply wp
2079     apply wpc
2080        apply (clarsimp simp:validE_def valid_def return_def returnOk_def)
2081       apply wp+
2082    apply simp
2083    apply (simp add:get_pde_def)
2084    apply wp
2085   apply (simp add:validE_def)
2086   apply (rule hoare_strengthen_post[where Q="\<lambda>rv. page_table_at w"])
2087    apply wp
2088   apply (clarsimp simp:pd_pt_relation_def obj_at_def)+
2089 done
2090
2091lemma hoare_post_Some_conj:
2092  "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> Q a s | _ \<Rightarrow> S \<rbrace>;
2093    \<lbrace>P'\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> R a s | _ \<Rightarrow> S \<rbrace>
2094   \<rbrakk> \<Longrightarrow>\<lbrace>P and P'\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> Q a s \<and> R a s | _ \<Rightarrow> S\<rbrace>"
2095  apply (clarsimp simp:valid_def)
2096  apply (drule_tac x = s in spec)+
2097  apply clarsimp
2098  apply (drule_tac x= "(a,b)" in bspec,simp)+
2099  apply (clarsimp split:option.splits)
2100done
2101
2102lemma cleanByVA_PoU_underlying_memory[wp]: " \<lbrace>\<lambda>m'. underlying_memory m' = m\<rbrace> cleanByVA_PoU w q \<lbrace>\<lambda>_ m'. underlying_memory m' = m\<rbrace>"
2103    apply(clarsimp simp: cleanByVA_PoU_def, wp)
2104done
2105
2106lemma cdl_asid_table_transform:
2107  "cdl_asid_table (transform sa) x
2108  =  unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table (arch_state sa)) x"
2109  by (simp add:transform_def transform_asid_table_def)
2110
2111lemma dcorres_find_pd_for_asid:
2112  "dcorres ( dc \<oplus> (=)) \<top> valid_idle
2113    (cdl_find_pd_for_asid (transform_asid a, b))
2114    (find_pd_for_asid a)"
2115  apply (simp add:cdl_find_pd_for_asid_def find_pd_for_asid_def transform_asid_def)
2116  apply (simp add:liftE_bindE assertE_assert)
2117  apply (rule dcorres_symb_exec_r[where Q' = "\<lambda>r. valid_idle"])
2118    apply (simp add:gets_def)
2119    apply (rule dcorres_get)
2120    apply (clarsimp simp:cdl_asid_table_transform liftE_bindE
2121      transform_asid_table_entry_def split:option.splits)
2122    apply (simp add:get_asid_pool_def get_object_def gets_the_def gets_def bind_assoc)
2123    apply (rule dcorres_get)
2124    apply (clarsimp simp: obj_at_def opt_object_asid_pool
2125                          assert_opt_def has_slots_def opt_cap_def slots_of_def assert_def
2126                          corres_free_fail
2127                   split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
2128    apply (clarsimp simp:transform_asid_pool_contents_def
2129      object_slots_def transform_asid_pool_entry_def split:option.splits)
2130    apply (rule corres_guard_imp[OF dcorres_returnOk])
2131    apply (simp|wp)+
2132  done
2133
2134lemma unat_pd_bits_less_4096_helper[simp]:
2135  "\<And>x. unat (x && mask pd_bits >> 2 :: word32) < 4096"
2136  apply (rule order_less_le_trans[where y="2^12"])
2137   apply (rule unat_less_power[rotated])
2138    apply (rule shiftr_less_t2n)
2139    apply (rule order_less_le_trans, rule and_mask_less')
2140     apply (simp_all add: pd_bits_def pageBits_def word_bits_conv)
2141  done
2142
2143lemma pd_at_cdl_pd_at:
2144  "\<lbrakk>valid_idle s ; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots;
2145  kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk>
2146  \<Longrightarrow> opt_cap (transform_pd_slot_ref ptr) (transform s) =
2147  Some (transform_pde (fun (of_nat (unat (ptr && mask pd_bits >> 2)))))"
2148  apply (clarsimp simp:opt_cap_def transform_pd_slot_ref_def transform_def
2149    slots_of_def opt_object_def transform_objects_def pred_tcb_def2
2150    valid_idle_def restrict_map_def object_slots_def
2151    transform_page_directory_contents_def unat_map_def
2152     dest!:get_tcb_SomeD split:option.splits)
2153  apply (simp add: below_kernel_base)
2154  apply (auto simp:transform_page_directory_contents_def unat_map_def)
2155  done
2156
2157lemma dcorres_get_pde_helper:
2158  "ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
2159  \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') \<top> valid_idle
2160  (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)"
2161  apply (simp add:cdl_get_pde_def
2162    get_pde_def gets_def gets_the_def
2163    get_pd_def get_object_def bind_assoc)
2164  apply (rule dcorres_absorb_get_l)
2165  apply (rule dcorres_absorb_get_r)
2166  apply (clarsimp simp:assert_def assert_opt_def
2167    corres_free_fail
2168    split:Structures_A.kernel_object.splits
2169    arch_kernel_obj.splits)
2170  apply (drule(2) pd_at_cdl_pd_at)
2171  apply (simp add:ucast_nat_def)
2172  done
2173
2174lemma dcorres_get_pde:
2175  "dcorres (\<lambda>r r'. r = transform_pde r') \<top>
2176  (valid_idle and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
2177  (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)"
2178  apply (rule corres_guard_imp[OF corres_gen_asm2])
2179  apply (rule dcorres_get_pde_helper)
2180  apply simp+
2181  done
2182
2183lemma PPtrPAddr:
2184  "(addrFromPPtr w = v) = (ptrFromPAddr v = w)"
2185  by (auto simp:addrFromPPtr_def ptrFromPAddr_def)
2186
2187lemma dcorres_page_table_mapped:
2188   "b < kernel_base
2189    \<Longrightarrow> dcorres (\<lambda>r r'. r = option_map (\<lambda>x. cdl_lookup_pd_slot x b) r')
2190    \<top> (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageTableCap w (Some (a, b)))))
2191        (cdl_page_table_mapped (transform_asid a, b) w)
2192        (page_table_mapped a b w)"
2193  apply (simp add:cdl_page_table_mapped_def page_table_mapped_def
2194    dcorres_lookup_pd_slot)
2195  apply (rule corres_guard_imp[OF corres_split_catch
2196      [where f = dc and E = dc and E' =dc]])
2197       apply simp
2198      apply (rule corres_splitEE[OF _ dcorres_find_pd_for_asid])
2199        apply (rule_tac F =" is_aligned pda 14" in corres_gen_asm2)
2200        apply (clarsimp simp:liftE_bindE dcorres_lookup_pd_slot)
2201        apply (rule corres_split[OF _ dcorres_get_pde])
2202          apply (case_tac  rv')
2203             apply (simp add:transform_pde_def)
2204             apply (rule dcorres_returnOk,simp)
2205            apply (simp add:transform_pde_def PPtrPAddr)
2206            apply (intro conjI impI)
2207             apply (rule dcorres_returnOk,simp)
2208            apply (rule dcorres_returnOk,simp)
2209           apply (simp add:transform_pde_def)
2210           apply (rule dcorres_returnOk,simp)
2211          apply (simp add:transform_pde_def)
2212          apply (rule dcorres_returnOk,simp)
2213         apply wp+
2214      apply (rule hoare_post_imp_R[OF find_pd_for_asid_aligned_pd])
2215      apply simp
2216      apply (erule less_kernel_base_mapping_slots)
2217      apply (simp add:pd_bits_def pageBits_def)
2218     apply wp
2219       apply ((simp add:dc_def,rule hoareE_TrueI[where P = \<top>])|wp)+
2220   apply simp+
2221  apply fastforce
2222  done
2223
2224lemma lookup_pd_slot_aligned_simp:
2225 "is_aligned pd pd_bits
2226  \<Longrightarrow> lookup_pd_slot pd vptr && mask pd_bits >> 2 = vptr >> 20"
2227  by (simp add:lookup_pd_slot_def mask_add_aligned
2228    shiftr_shiftl_mask_pd_bits vptr_shifting_3_ways)
2229
2230
2231lemma dcorres_unmap_page_table_store_pde:
2232  "dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))
2233    and valid_idle and K (is_aligned pd 14 \<and> vptr < kernel_base)
2234    and pd_pt_relation (lookup_pd_slot pd vptr && ~~ mask pd_bits) pt_id (lookup_pd_slot pd vptr) )
2235           (delete_cap_simple (cdl_lookup_pd_slot pd vptr))
2236           (store_pde (lookup_pd_slot pd vptr) ARM_A.pde.InvalidPDE)"
2237  apply (rule corres_guard_imp)
2238    apply (rule corres_gen_asm2)
2239    apply (subst dcorres_lookup_pd_slot,assumption)
2240    apply (simp add:store_pde_def)
2241    apply (rule corres_symb_exec_r)
2242       apply (simp add:transform_pd_slot_ref_def)
2243       apply (rule corres_gen_asm2)
2244       apply (rule dcorres_delete_cap_simple_set_pde[where oid = pt_id])
2245       apply assumption
2246      apply (wp|simp)+
2247  apply (rule impI)
2248  apply (rule less_kernel_base_mapping_slots)
2249   apply (simp add: pd_bits_def pageBits_def)+
2250  done
2251
2252lemma dcorres_option:
2253  "\<lbrakk> x = None \<Longrightarrow> dcorres sr T P g (C None);
2254    \<And>z. x = Some z \<Longrightarrow> dcorres sr T (Q z) g (C (Some z))\<rbrakk> \<Longrightarrow>
2255  dcorres sr T (\<lambda>s. case x of None \<Rightarrow> P s | Some z \<Rightarrow> Q z s) g (C x)"
2256  by (case_tac x ,auto)
2257
2258lemma dcorres_unmap_page_table:
2259  "\<lbrakk>a \<le> mask asid_bits ; b < kernel_base ; vmsz_aligned b ARMSection\<rbrakk>
2260   \<Longrightarrow> dcorres dc \<top> (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageTableCap w (Some (a, b)))))
2261     (PageTableUnmap_D.unmap_page_table (transform_asid a,b)  w)
2262     (ARM_A.unmap_page_table a b w)"
2263  apply (simp add: unmap_page_table_def PageTableUnmap_D.unmap_page_table_def)
2264  apply (rule corres_guard_imp)
2265    apply (rule corres_split[OF _ dcorres_page_table_mapped])
2266      apply (rule dcorres_option[where P = \<top>])
2267       apply simp
2268      apply (simp add: dc_def[symmetric])
2269      apply (rule corres_dummy_return_l)
2270       apply (rule corres_split[where r'=dc])
2271          apply clarify
2272          apply (rule corres_dummy_return_l)
2273          apply (rule corres_split[where r'=dc])
2274            apply (rule dcorres_flush_table)
2275           apply (clarsimp)
2276           apply (rule dcorres_machine_op_noop)
2277           apply wp+
2278       apply (rule dcorres_unmap_page_table_store_pde)
2279      apply (wp|simp)+
2280    apply (wp hoare_post_Some_conj)
2281     apply (wp page_table_mapped_wp)[1]
2282    apply (wp hoare_post_Some_conj)
2283     apply (wp page_table_mapped_wp)[1]
2284    apply (wp hoare_post_Some_conj)
2285     apply (wp page_table_mapped_wp)[1]
2286    apply (wp pd_pt_relation_page_table_mapped_wp)
2287   apply simp
2288  apply (clarsimp simp:invs_psp_aligned invs_vspace_objs
2289    invs_mdb_cte[unfolded swp_def] invs_valid_idle
2290    valid_cap_def pd_bits_def pageBits_def)
2291  done
2292
2293lemma imp_strength:
2294  "(A \<and> (B\<longrightarrow>C)) \<longrightarrow> (B \<longrightarrow> (A\<and>C))"
2295  by clarsimp
2296
2297lemma cleanCacheRange_PoU_underlying_memory[wp]:
2298             "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>
2299              cleanCacheRange_PoU a b c
2300              \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
2301   apply (clarsimp simp: cleanCacheRange_PoU_def, wp)
2302done
2303
2304lemma valid_pde_pt_at:
2305  "\<lbrakk>valid_pde (ARM_A.pde.PageTablePDE word1 se word2) s \<and> pspace_aligned s\<rbrakk>
2306  \<Longrightarrow> (ptrFromPAddr word1, unat ((vaddr >> 12) && 0xFF)) =
2307  transform_pt_slot_ref (ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2))"
2308  apply (clarsimp simp :transform_pt_slot_ref_def )
2309  apply (drule(1) pt_aligned)
2310  apply (simp add:vaddr_segment_nonsense3
2311    vaddr_segment_nonsense4)
2312  apply (subst shiftl_shiftr_id)
2313    apply simp
2314   apply (rule le_less_trans[OF word_and_le1])
2315   apply simp
2316  apply simp
2317  done
2318
2319lemma dcorres_lookup_pt_slot:
2320  "dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) \<top>
2321    (valid_vspace_objs and \<exists>\<rhd> (lookup_pd_slot v a && ~~ mask pd_bits) and pspace_aligned
2322       and valid_idle and K(is_aligned v pd_bits)
2323       and K (ucast (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
2324    (cdl_lookup_pt_slot v a)
2325    (lookup_pt_slot v a)"
2326  apply (simp add:cdl_lookup_pt_slot_def lookup_pt_slot_def)
2327  apply (rule corres_guard_imp)
2328  apply (rule_tac F =" is_aligned v 14" in corres_gen_asm2)
2329     apply (clarsimp simp:dcorres_lookup_pd_slot)
2330     apply (rule corres_splitEE[OF _
2331      corres_liftE_rel_sum[THEN iffD2,OF dcorres_get_pde] ])
2332      apply (case_tac rv')
2333         prefer 2
2334         apply (simp add:transform_pde_def)
2335         apply (rule corres_returnOk)
2336         apply (erule valid_pde_pt_at)
2337        apply (simp add:transform_pde_def)+
2338       apply (rule hoare_TrueI)
2339    apply (wp|simp)+
2340  apply (simp add:pd_bits_def pageBits_def)
2341  done
2342
2343lemma find_pd_for_asid_kernel_mapping_help:
2344  "\<lbrace>pspace_aligned and valid_vspace_objs and K (v<kernel_base) \<rbrace> find_pd_for_asid a
2345   \<lbrace>\<lambda>rv s. ucast (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<rbrace>,-"
2346  apply (rule hoare_gen_asmE)
2347  apply (rule hoare_post_imp_R)
2348   apply (rule find_pd_for_asid_aligned_pd_bits)
2349   apply simp
2350  apply (rule less_kernel_base_mapping_slots)
2351  apply simp+
2352  done
2353
2354lemma dcorres_might_throw:
2355  "\<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) \<top> \<top> might_throw (throw_on_false a b)"
2356  apply (simp add: liftE_bindE unlessE_def
2357    might_throw_def throw_on_false_def split:if_splits)
2358  apply (rule corres_symb_exec_r)
2359     apply (clarsimp split:if_splits)
2360     apply (intro conjI impI)
2361      apply (rule corres_alternate1)
2362      apply (simp add:returnOk_def)
2363     apply (rule corres_alternate2)
2364     apply simp
2365    apply (wp hoare_TrueI)
2366   apply simp
2367  apply simp
2368  done
2369
2370lemma corres_dummy_returnOk_l:
2371  "dcorres cr P P' (f >>=E returnOk) g \<Longrightarrow> dcorres cr P P' f g"
2372  by (simp add:liftE_def)
2373
2374lemma dcorres_unmap_page:
2375  notes swp_apply[simp del]
2376  shows "dcorres dc \<top> (invs and valid_pdpt_objs and
2377                  valid_cap (cap.ArchObjectCap (arch_cap.PageCap dev pg fun vmpage_size (Some (a, v)))))
2378              (PageTableUnmap_D.unmap_page (transform_asid a,v) pg (pageBitsForSize vmpage_size))
2379              (ARM_A.unmap_page vmpage_size a v pg)"
2380  apply (rule dcorres_expand_pfx)
2381  apply (clarsimp simp:valid_cap_def)
2382  apply (case_tac vmpage_size)
2383\<comment> \<open>ARMSmallPage\<close>
2384  apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
2385    PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
2386  apply (rule corres_guard_imp)
2387    apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
2388      in corres_split_catch [where f = dc and E = dc and E' =dc])
2389       apply simp
2390      apply (rule corres_guard_imp)
2391        apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
2392        apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
2393               pageBitsForSize_def bindE_assoc mapM_x_singleton)
2394       apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot])
2395         apply (rule corres_splitEE[OF _ dcorres_might_throw])
2396          apply (rule corres_dummy_returnOk_l)
2397          apply (rule corres_splitEE)
2398prefer 2
2399             apply (simp add:transform_pt_slot_ref_def)
2400             apply (rule dcorres_store_invalid_pte[where pg_id = pg])
2401            apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
2402            apply (rule dcorres_symb_exec_r)
2403              apply (rule dcorres_flush_page)
2404             apply (wp do_machine_op_wp | clarsimp)+
2405         apply (simp add: imp_conjR)
2406         apply ((wp check_mapping_pptr_pt_relation | wp_once hoare_drop_imps)+)[1]
2407        apply (simp | wp lookup_pt_slot_inv)+
2408     apply (simp add: dc_def
2409       | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
2410       | rule conjI | clarify)+
2411
2412\<comment> \<open>ARMLargePage\<close>
2413
2414  apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
2415    PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
2416  apply (rule corres_guard_imp)
2417    apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
2418      in corres_split_catch [where f = dc and E = dc and E' =dc])
2419       apply simp
2420      apply (rule corres_guard_imp)
2421        apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
2422        apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
2423               pageBitsForSize_def bindE_assoc mapM_x_singleton)
2424       apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot])
2425         apply (rule corres_splitEE[OF _ dcorres_might_throw])
2426            apply (rule dcorres_symb_exec_rE)
2427              apply (rule corres_dummy_returnOk_l)
2428              apply (rule corres_splitEE)
2429prefer 2
2430                 apply simp
2431                 apply (rule_tac F = "is_aligned xa 6" in corres_gen_asm2)
2432                 apply (erule dcorres_unmap_large_page[where pg_id = pg])
2433                apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
2434                apply (rule dcorres_symb_exec_r)
2435                  apply (rule dcorres_flush_page[unfolded dc_def])
2436                 apply (wp do_machine_op_wp | clarsimp)+
2437         apply (simp add: imp_conjR is_aligned_mask)
2438         apply (rule hoare_vcg_conj_lift)
2439          apply (wp hoare_drop_imps)[1]
2440         apply (rule hoare_vcg_conj_lift)
2441          apply (wp hoare_drop_imps)[1]
2442         apply (rule hoare_strengthen_post[OF check_mapping_pptr_pt_relation])
2443          apply fastforce
2444        apply (simp | wp lookup_pt_slot_inv)+
2445       apply (simp add: dc_def
2446         | wp lookup_pt_slot_inv hoare_drop_imps
2447           find_pd_for_asid_kernel_mapping_help
2448         | safe)+
2449
2450\<comment> \<open>Section\<close>
2451  apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
2452    PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
2453  apply (rule corres_guard_imp)
2454    apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
2455      in corres_split_catch [where f = dc and E = dc and E' =dc])
2456       apply simp
2457      apply (rule corres_guard_imp)
2458        apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
2459          apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
2460            pageBitsForSize_def bindE_assoc mapM_x_singleton)
2461       apply (rule corres_splitEE[OF _ dcorres_might_throw])
2462       apply (rule corres_dummy_returnOk_l)
2463          apply (rule corres_splitEE)
2464prefer 2
2465             apply simp
2466             apply (rule dcorres_delete_cap_simple_section[where oid = pg])
2467            apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
2468            apply (rule dcorres_symb_exec_r)
2469              apply (rule dcorres_flush_page[unfolded dc_def])
2470             apply (wp do_machine_op_wp | clarsimp)+
2471         apply (simp add: imp_conjR)
2472         apply ((wp check_mapping_pptr_section_relation | wp_once hoare_drop_imps)+)[1]
2473        apply (simp | wp lookup_pt_slot_inv)+
2474     apply (simp add: dc_def
2475       | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
2476       | safe)+
2477
2478\<comment> \<open>SuperSection\<close>
2479
2480  apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
2481    PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
2482  apply (rule corres_guard_imp)
2483    apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
2484      in corres_split_catch [where f = dc and E = dc and E' =dc])
2485       apply simp
2486      apply (rule corres_guard_imp)
2487        apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
2488        apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
2489               pageBitsForSize_def bindE_assoc mapM_x_singleton)
2490        apply (rule corres_splitEE[OF _ dcorres_might_throw])
2491           apply (rule dcorres_symb_exec_rE)
2492             apply (rule corres_dummy_returnOk_l)
2493             apply (rule corres_splitEE)
2494prefer 2
2495                 apply simp
2496                 apply (rule_tac F = "is_aligned pda 14" in corres_gen_asm2)
2497                 apply (erule(2) dcorres_unmap_large_section[where pg_id = pg])
2498                apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
2499                apply (rule dcorres_symb_exec_r)
2500                  apply (rule dcorres_flush_page[unfolded dc_def])
2501                 apply (wp do_machine_op_wp | clarsimp)+
2502         apply (simp add: imp_conjR is_aligned_mask)
2503         apply (rule hoare_vcg_conj_lift)
2504          apply (wp hoare_drop_imps)[1]
2505         apply (rule hoare_vcg_conj_lift)
2506          apply (wp hoare_drop_imps)[1]
2507         apply (rule hoare_vcg_conj_lift)
2508          apply (rule hoare_strengthen_post[OF check_mapping_pptr_super_section_relation])
2509          apply clarsimp
2510       apply (simp add:is_aligned_mask[symmetric] dc_def
2511         | wp lookup_pt_slot_inv hoare_drop_imps
2512           find_pd_for_asid_kernel_mapping_help
2513         | safe)+
2514done
2515
2516
2517lemma dcorres_delete_asid_none:
2518  "dcorres dc \<top> \<top> (CSpace_D.delete_asid x word) (return ())"
2519  apply (clarsimp simp:CSpace_D.delete_asid_def)
2520  apply (rule corres_alternate2)
2521  apply clarsimp
2522  done
2523
2524lemma asid_table_transform:
2525  "cdl_asid_table (transform s) slot =
2526   unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table (arch_state s)) slot"
2527  apply (simp add:transform_def transform_asid_table_def transform_asid_table_entry_def)
2528  done
2529
2530lemma dcorres_delete_asid:
2531  "dcorres dc \<top> (valid_idle)
2532    (CSpace_D.delete_asid (transform_asid asid) word)
2533    (ARM_A.delete_asid asid word)"
2534  apply (clarsimp simp:CSpace_D.delete_asid_def ARM_A.delete_asid_def)
2535  apply (clarsimp simp:gets_def)
2536  apply (rule dcorres_absorb_get_r)
2537  apply (clarsimp simp:when_def split:option.splits)
2538  apply (rule conjI)
2539   apply clarsimp
2540   apply (rule corres_alternate2)
2541   apply clarsimp
2542  apply clarsimp
2543  apply (rule dcorres_symb_exec_r_strong)
2544    apply clarsimp
2545    apply (rule conjI)
2546     apply clarsimp
2547     apply (rule corres_alternate1)
2548     apply (rule dcorres_absorb_get_l)
2549     apply (drule_tac s="transform s'" in sym)
2550     apply (clarsimp simp:when_def asid_table_transform transform_asid_def
2551                          transform_asid_table_entry_def
2552                     split:option.splits if_splits)
2553     apply (rule dcorres_symb_exec_r_strong)
2554       apply (rule dcorres_symb_exec_r_strong)
2555         apply (rule corres_guard_imp)
2556           apply (rule corres_dummy_return_l)
2557           apply (rule corres_split[OF corres_trivial,where r'=dc])
2558              apply (rule dcorres_symb_exec_r[OF dcorres_set_vm_root])
2559               apply wp+
2560             apply (rule dcorres_set_asid_pool)
2561               apply simp
2562              apply (clarsimp simp:transform_asid_def)
2563             apply (clarsimp simp:transform_asid_pool_entry_def)
2564            apply (wp | clarsimp)+
2565         apply simp
2566        apply (wp | clarsimp)+
2567      apply (rule hoare_pre, wp)
2568      apply simp
2569     apply (wp | clarsimp)+
2570    apply (rule corres_alternate2)
2571    apply simp
2572   apply (wp | clarsimp)+
2573done
2574
2575lemma thread_in_thread_cap_not_idle:
2576 "\<lbrakk>valid_global_refs s;cte_wp_at ((=) (cap.ThreadCap ptr)) slot s\<rbrakk>
2577  \<Longrightarrow> not_idle_thread ptr s"
2578  apply (rule ccontr)
2579  apply (clarsimp simp:valid_cap_def valid_global_refs_def valid_refs_def)
2580  apply (case_tac slot)
2581  apply (drule_tac x = a in spec)
2582    apply (drule_tac x = b in spec)
2583  apply (clarsimp simp:cte_wp_at_def not_idle_thread_def)
2584  apply (simp add:cap_range_def global_refs_def)
2585done
2586
2587lemma set_cap_set_thread_state_inactive:
2588  "dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
2589   (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap)
2590   (set_thread_state thread Structures_A.thread_state.Inactive)"
2591  apply (clarsimp simp:set_thread_state_def)
2592  apply (rule dcorres_absorb_gets_the)
2593  apply (rule corres_guard_imp)
2594    apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres])
2595    apply (rule set_pending_cap_corres)
2596   apply simp
2597  apply (clarsimp dest!:get_tcb_SomeD
2598    simp:obj_at_def infer_tcb_pending_op_def)
2599  done
2600
2601lemma prepare_thread_delete_dcorres: "dcorres dc P P' (CSpace_D.prepare_thread_delete t) (prepare_thread_delete t)"
2602  apply (clarsimp simp: CSpace_D.prepare_thread_delete_def prepare_thread_delete_def)
2603  done
2604
2605lemma dcorres_finalise_cap:
2606  "cdlcap = transform_cap cap \<Longrightarrow>
2607      dcorres (\<lambda>r r'. fst r = transform_cap (fst r'))
2608             \<top> (invs and valid_cap cap and valid_pdpt_objs and cte_wp_at ((=) cap) slot and valid_etcbs)
2609          (CSpace_D.finalise_cap cdlcap final)
2610          (CSpace_A.finalise_cap cap final)"
2611  apply (case_tac cap)
2612             apply (simp_all add: when_def)
2613       apply clarsimp
2614       apply (rule corres_rel_imp)
2615        apply (rule corres_guard_imp[OF dcorres_cancel_all_ipc])
2616         apply (clarsimp simp:invs_def valid_state_def)+
2617      apply (rule corres_rel_imp)
2618       apply (rule corres_guard_imp)
2619         apply (rule corres_split[OF dcorres_cancel_all_signals dcorres_unbind_maybe_notification])
2620          apply (wp unbind_maybe_notification_valid_etcbs | simp | wpc)+
2621       apply ((clarsimp simp:invs_def valid_state_def)+)[2]
2622     apply (simp add:IpcCancel_A.suspend_def bind_assoc)
2623     apply clarsimp
2624     apply (rule corres_guard_imp)
2625       apply (rule corres_split[OF _ dcorres_unbind_notification])
2626         apply (rule corres_split[OF _ finalise_cancel_ipc])
2627           apply (rule corres_split)
2628              unfolding K_bind_def
2629              apply (rule dcorres_rhs_noop_above_True[OF tcb_sched_action_dcorres[where P=\<top> and P'=\<top>]])
2630              apply (rule corres_split'[OF prepare_thread_delete_dcorres])
2631                apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]])
2632                apply (clarsimp simp:transform_cap_def)
2633               apply wp+
2634             apply (rule set_cap_set_thread_state_inactive)
2635            apply wp+
2636         apply (simp add:not_idle_thread_def)
2637         apply (wp unbind_notification_invs | simp add: not_idle_thread_def)+
2638     apply clarsimp
2639     apply (drule(1) thread_in_thread_cap_not_idle[OF invs_valid_global_refs])
2640     apply (simp add:not_idle_thread_def)
2641    apply clarsimp
2642    apply (rule corres_guard_imp)
2643      apply (rule corres_split[OF _ dcorres_deleting_irq_handler])
2644        apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]])
2645        apply (clarsimp simp:transform_cap_def)
2646       apply (wp|clarsimp)+
2647   apply (clarsimp simp:assert_def corres_free_fail)
2648  apply (rename_tac arch_cap)
2649  apply (case_tac arch_cap)
2650      apply (simp_all add: arch_finalise_cap_def split:arch_cap.split_asm)
2651     apply clarsimp
2652     \<comment> \<open>arch_cap.ASIDPoolCap\<close>
2653     apply (rule corres_guard_imp)
2654       apply (simp add:transform_asid_def)
2655       apply (rule corres_split[OF _ dcorres_delete_asid_pool])
2656         apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]])
2657         apply (clarsimp simp:transform_cap_def)
2658        apply (wp|clarsimp)+
2659    apply (clarsimp split:option.splits | rule conjI)+
2660     \<comment> \<open>arch_cap.PageCap\<close>
2661     apply (simp add:transform_mapping_def)
2662    apply (clarsimp simp:transform_mapping_def)
2663    apply (rule corres_guard_imp)
2664      apply (rule_tac corres_split[OF _ dcorres_unmap_page])
2665        apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]])
2666        apply (clarsimp simp:transform_cap_def)
2667       apply (wp | clarsimp )+
2668    apply simp
2669   \<comment> \<open>arch_cap.PageTableCap\<close>
2670   apply (clarsimp simp:transform_mapping_def split:option.splits)
2671   apply (rule dcorres_expand_pfx)
2672   apply (rule corres_guard_imp)
2673     apply (rule corres_split[OF _ dcorres_unmap_page_table])
2674          apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]])
2675          apply (clarsimp simp:transform_cap_def)
2676         apply ((wp|clarsimp )+)[4]
2677         apply (rule iffD1[OF le_mask_iff_lt_2n,THEN iffD2],simp add:word_size asid_bits_def)
2678         apply (clarsimp simp:valid_cap_def cap_aligned_def  )+
2679       apply (simp add:vmsz_aligned_def)
2680      apply (wp|clarsimp)+
2681  apply (rule conjI | clarsimp split:option.splits)+
2682  apply (rule corres_guard_imp)
2683    apply (rule corres_split[OF _ dcorres_delete_asid])
2684      apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]])
2685      apply (clarsimp simp:transform_cap_def)
2686     apply (wp|clarsimp split:option.splits)+
2687  done
2688
2689lemma dcorres_splits:
2690  "\<lbrakk> T a \<Longrightarrow> dcorres r P (Q a) f (g a);
2691    \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a)\<rbrakk>\<Longrightarrow>
2692    dcorres r P ( (\<lambda>s. (T a) \<longrightarrow> (Q a s)) and (\<lambda>s. (\<not> (T a)) \<longrightarrow> (Q' a s)) ) f (g a)"
2693  apply (case_tac "T a")
2694    apply clarsimp+
2695done
2696
2697lemma get_cap_weak_wp:
2698  "\<lbrace>cte_wp_at Q slot\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
2699  by (clarsimp simp:valid_def cte_wp_at_def)
2700
2701definition remainder_cap :: "bool \<Rightarrow> cap \<Rightarrow> cap"
2702where "remainder_cap final c\<equiv> case c of
2703  cap.CNodeCap r bits g \<Rightarrow> if final then cap.Zombie r (Some bits) (2 ^ bits) else cap.NullCap
2704| cap.ThreadCap r \<Rightarrow> if final then cap.Zombie r None 5 else cap.NullCap
2705| cap.Zombie r b n \<Rightarrow> cap.Zombie r b n
2706| cap.ArchObjectCap a \<Rightarrow> cap.NullCap
2707| _ \<Rightarrow> cap.NullCap"
2708
2709lemma finalise_cap_remainder:
2710  "\<lbrace>\<top>\<rbrace>CSpace_A.finalise_cap cap final \<lbrace>\<lambda>r s. fst (r) = (remainder_cap final cap) \<rbrace>"
2711  apply (case_tac cap; simp add: remainder_cap_def)
2712             apply (wp|clarsimp)+
2713            apply (fastforce simp:valid_def)
2714           apply (simp add: liftM_def |clarify)+
2715          apply (wp|clarsimp|rule conjI)+
2716  apply (simp add:arch_finalise_cap_def)
2717  apply (cases final)
2718
2719   apply (rename_tac arch_cap)
2720
2721
2722   apply (case_tac arch_cap)
2723       apply (simp_all)
2724       apply (wp|clarsimp)+
2725     apply (simp_all split:option.splits)
2726     apply (wp | clarsimp | rule conjI)+
2727  apply (rename_tac arch_cap)
2728  apply (case_tac arch_cap; simp)
2729      apply (wp|clarsimp split:option.splits | rule conjI)+
2730  done
2731
2732lemma obj_ref_not_idle:
2733  "\<lbrakk>valid_objs s;valid_global_refs s;cte_at slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) slot s"
2734  apply (simp add:valid_global_refs_def valid_refs_def)
2735  apply (case_tac slot)
2736  apply clarsimp
2737  apply (drule_tac x = a in spec)
2738  apply (drule_tac x = b in spec)
2739  apply (clarsimp simp:cte_wp_at_def not_idle_thread_def cap_range_def global_refs_def)
2740  done
2741
2742lemma singleton_set_eq:
2743  "\<lbrakk>x = {a}; b\<in> x\<rbrakk>\<Longrightarrow> b = a"
2744  by clarsimp
2745
2746lemma zombies_final_ccontr:
2747  "\<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; is_zombie cap; zombies_final s;
2748     caps_of_state s p' = Some cap'\<rbrakk>
2749    \<Longrightarrow> r\<in> obj_refs cap' \<longrightarrow> is_zombie cap' \<and> p = p'"
2750  apply (rule ccontr)
2751  apply (case_tac p)
2752  apply (clarsimp simp:zombies_final_def)
2753  apply (drule_tac x = a in spec,drule_tac x = b in spec)
2754  apply (frule caps_of_state_cteD)
2755    apply (simp add:cte_wp_at_def)
2756  apply (clarsimp simp:IpcCancel_A.is_final_cap'_def)
2757  apply (frule_tac a = "(aa,ba)" and b = p' in singleton_set_eq)
2758    apply (clarsimp)
2759    apply (drule_tac a = "(aa,ba)" and b = p' in singleton_set_eq)
2760      apply (clarsimp dest!:caps_of_state_cteD simp:cte_wp_at_def)
2761      apply (drule IntI)
2762        apply (simp add: gen_obj_refs_Int)+
2763  apply (drule_tac a = "(aa,ba)" and b = "(a,b)" in singleton_set_eq)
2764    apply clarsimp
2765  apply clarsimp
2766done
2767
2768lemma zombie_cap_has_all:
2769  "\<lbrakk>valid_objs s;if_unsafe_then_cap s; zombies_final s;valid_global_refs s;
2770    caps_of_state s slot = Some (cap.Zombie w option n);
2771    (w,x) \<notin> cte_refs (cap.Zombie w option n) f  \<rbrakk>
2772    \<Longrightarrow>  caps_of_state s (w,x) = None \<or> caps_of_state s (w,x) = Some cap.NullCap"
2773  apply (clarsimp simp:if_unsafe_then_cap_def valid_cap_def split:option.splits)
2774  apply (drule_tac x = w in spec,drule_tac x = x in spec)
2775  apply (rule ccontr)
2776  apply clarsimp
2777  apply (clarsimp simp:ex_cte_cap_wp_to_def appropriate_cte_cap_def)
2778  apply (drule iffD1[OF cte_wp_at_caps_of_state])
2779  apply clarsimp
2780  apply (frule_tac p = slot and p'="(a,b)" in zombies_final_ccontr)
2781      apply simp+
2782     apply (simp add:is_zombie_def)
2783    apply simp+
2784  apply (case_tac cap; simp)
2785  apply (case_tac y; simp)
2786  apply (frule_tac p = "(a,b)" in caps_of_state_valid_cap)
2787   apply simp
2788  apply (frule_tac p = slot in caps_of_state_valid_cap)
2789   apply simp
2790  apply (rename_tac word w2 w3 rights)
2791  apply (clarsimp simp:valid_cap_def tcb_at_def dest!:get_tcb_SomeD)
2792  apply (drule_tac p = "(interrupt_irq_node s word,[])" in caps_of_state_cteD)
2793  apply (clarsimp simp:cte_wp_at_cases)
2794  apply (clarsimp simp:obj_at_def tcb_cap_cases_def tcb_cnode_index_def to_bl_1 split:if_splits)
2795  apply (drule valid_globals_irq_node[OF _ caps_of_state_cteD])
2796   apply simp
2797  apply (fastforce simp:cap_range_def)
2798  done
2799
2800lemma monadic_trancl_steps:
2801  "monadic_rewrite False False \<top>
2802     (monadic_trancl f x)
2803     (do y \<leftarrow> monadic_trancl f x;
2804           monadic_trancl f y od)"
2805  apply (simp add: monadic_rewrite_def monadic_trancl_def
2806                   bind_def split_def monadic_option_dest_def)
2807  apply (safe, simp_all)
2808  done
2809
2810lemma monadic_trancl_f:
2811  "monadic_rewrite False False \<top>
2812     (monadic_trancl f x) (f x)"
2813  apply (simp add: monadic_rewrite_def monadic_trancl_def
2814                   bind_def split_def monadic_option_dest_def)
2815  apply (safe, simp_all)
2816   apply (simp add: r_into_rtrancl monadic_rel_optionation_form_def)+
2817  done
2818
2819lemma monadic_trancl_step:
2820  "monadic_rewrite False False \<top>
2821       (monadic_trancl f x) (do y \<leftarrow> f x; monadic_trancl f y od)"
2822  apply (rule monadic_rewrite_imp)
2823   apply (rule monadic_rewrite_trans)
2824    apply (rule monadic_trancl_steps)
2825   apply (rule monadic_rewrite_bind_head)
2826   apply (rule monadic_trancl_f)
2827  apply simp
2828  done
2829
2830lemma monadic_trancl_return:
2831  "monadic_rewrite False False \<top>
2832          (monadic_trancl f x) (return x)"
2833  by (simp add: monadic_rewrite_def monadic_trancl_def
2834                monadic_option_dest_def return_def)
2835
2836lemma monadic_rewrite_if_lhs:
2837  "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q b a;
2838     \<not> P \<Longrightarrow> monadic_rewrite F E R c a\<rbrakk>
2839     \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s))
2840        (if P then b else c) a"
2841  by (cases P, simp_all)
2842
2843lemma monadic_rewrite_case_option:
2844  "\<lbrakk> \<And>y. x = Some y \<Longrightarrow> monadic_rewrite E F (P x) f (g y);
2845           x = None \<Longrightarrow> monadic_rewrite E F Q f h \<rbrakk>
2846     \<Longrightarrow> monadic_rewrite E F (\<lambda>s. (\<forall>y. x = Some y \<longrightarrow> P x s) \<and> (x = None \<longrightarrow> Q s))
2847              f (case x of Some y \<Rightarrow> g y | None \<Rightarrow> h)"
2848  by (cases x, simp_all)
2849
2850lemma rtrancl_idem:
2851  assumes S: "S `` T = T"
2852       shows "S\<^sup>* `` T = T"
2853proof -
2854  note P = eqset_imp_iff[OF S, THEN iffD1, OF ImageI]
2855  have Q: "\<And>x y. (x, y) \<in> S\<^sup>* \<Longrightarrow> x \<in> T \<longrightarrow> y \<in> T"
2856    by (erule rtrancl.induct, auto dest: P)
2857
2858  thus ?thesis
2859    by auto
2860qed
2861
2862lemma monadic_trancl_lift_Inl:
2863  "monadic_trancl (lift f) (Inl err) = throwError err"
2864  apply (rule ext)
2865  apply (simp add: throwError_def return_def monadic_trancl_def)
2866  apply (subst rtrancl_idem)
2867   apply (auto simp: monadic_rel_optionation_form_def lift_def
2868                     throwError_def return_def monadic_option_dest_def)
2869  done
2870
2871lemma monadic_trancl_preemptible_steps:
2872  "monadic_rewrite False False \<top>
2873      (monadic_trancl_preemptible f x)
2874      (doE y \<leftarrow> monadic_trancl_preemptible f x;
2875              monadic_trancl_preemptible f y odE)"
2876  apply (simp add: monadic_trancl_preemptible_def)
2877  apply (rule monadic_rewrite_imp)
2878   apply (rule monadic_rewrite_trans)
2879    apply (rule monadic_trancl_steps)
2880   apply (simp add: bindE_def)
2881   apply (rule_tac Q="\<top>\<top>" in monadic_rewrite_bind_tail)
2882    apply (case_tac x)
2883     apply (simp add: lift_def monadic_trancl_lift_Inl)
2884     apply (rule monadic_rewrite_refl)
2885    apply (simp add: lift_def)
2886    apply (rule monadic_rewrite_refl)
2887   apply (wp | simp)+
2888  done
2889
2890lemma monadic_trancl_preemptible_f:
2891  "monadic_rewrite False False (\<lambda>_. True)
2892     (monadic_trancl_preemptible f x) (f x)"
2893  apply (simp add: monadic_trancl_preemptible_def)
2894  apply (rule monadic_rewrite_imp)
2895   apply (rule monadic_rewrite_trans)
2896    apply (rule monadic_trancl_f)
2897   apply (simp add: lift_def)
2898   apply (rule monadic_rewrite_refl)
2899  apply simp
2900  done
2901
2902lemmas monadic_rewrite_bindE_head
2903    = monadic_rewrite_bindE[OF _ monadic_rewrite_refl hoare_vcg_propE_R]
2904
2905lemma monadic_trancl_preemptible_step:
2906  "monadic_rewrite False False \<top>
2907      (monadic_trancl_preemptible f x)
2908      (doE y \<leftarrow> f x;
2909            monadic_trancl_preemptible f y odE)"
2910  apply (rule monadic_rewrite_imp)
2911   apply (rule monadic_rewrite_trans)
2912    apply (rule monadic_trancl_preemptible_steps)
2913   apply (rule monadic_rewrite_bindE_head)
2914   apply (rule monadic_trancl_preemptible_f)
2915  apply simp
2916  done
2917
2918lemma monadic_trancl_preemptible_return:
2919  "monadic_rewrite False False (\<lambda>_. True)
2920     (monadic_trancl_preemptible f x) (returnOk x)"
2921  apply (simp add: monadic_trancl_preemptible_def)
2922  apply (rule monadic_rewrite_imp)
2923   apply (rule monadic_rewrite_trans)
2924    apply (rule monadic_trancl_return)
2925   apply (simp add: returnOk_def)
2926   apply (rule monadic_rewrite_refl)
2927  apply simp
2928  done
2929
2930lemma monadic_rewrite_corres2:
2931  "\<lbrakk> monadic_rewrite False E Q a a';
2932        corres_underlying R False F r P P' a' c \<rbrakk>
2933     \<Longrightarrow> corres_underlying R False F r (P and Q) P' a c"
2934  apply (simp add: corres_underlying_def monadic_rewrite_def)
2935  apply (erule ballEI, clarsimp)
2936  apply (drule(1) bspec, clarsimp)
2937  apply (drule spec, drule(1) mp)
2938  apply fastforce
2939  done
2940
2941lemma dcorres_get_cap_symb_exec:
2942  "\<lbrakk> \<And>cap. dcorres r (P cap) (P' cap) f (g cap) \<rbrakk>
2943        \<Longrightarrow> dcorres r
2944          (\<lambda>s. \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s)
2945          (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s)
2946          f (do cap \<leftarrow> get_cap slot; g cap od)"
2947  apply (rule corres_symb_exec_r[OF _ get_cap_sp])
2948    apply (rule stronger_corres_guard_imp, assumption)
2949     apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap)
2950    apply (clarsimp simp: cte_wp_at_caps_of_state)
2951   apply (wp | simp)+
2952  done
2953
2954lemma set_cdt_modify:
2955  "set_cdt c = modify (\<lambda>s. s \<lparr> cdt := c \<rparr>)"
2956  by (simp add: set_cdt_def modify_def)
2957
2958lemma no_cdt_loop_mloop:
2959  "no_mloop m \<Longrightarrow> m x \<noteq> Some x"
2960  apply (rule notI)
2961  apply (simp add: no_mloop_def cdt_parent_rel_def del: split_paired_All)
2962  apply (drule_tac x=x in spec)
2963  apply (erule notE, rule r_into_trancl)
2964  apply (simp add: is_cdt_parent_def)
2965  done
2966
2967lemma set_cdt_list_modify:
2968  "set_cdt_list c = modify (\<lambda>s. s \<lparr> cdt_list := c \<rparr>)"
2969  by (simp add: set_cdt_list_def modify_def)
2970
2971lemma swap_cap_corres:
2972  "dcorres dc \<top> (valid_idle and valid_mdb and cte_at slot_a and cte_at slot_b
2973                 and valid_etcbs and K (slot_a \<noteq> slot_b)
2974                 and not_idle_thread (fst slot_a)
2975                 and not_idle_thread (fst slot_b))
2976     (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a)
2977               (transform_cap cap_b) (transform_cslot_ptr slot_b))
2978     (cap_swap cap_a slot_a cap_b slot_b)"
2979proof -
2980  note inj_on_insert[iff del]
2981  show ?thesis
2982  apply (simp add: swap_cap_def cap_swap_def)
2983  apply (rule corres_guard_imp)
2984    apply (rule corres_split_nor [OF _ set_cap_corres[OF refl refl]])
2985      apply (rule corres_split_nor [OF _ set_cap_corres[OF refl refl]])
2986        apply (simp add: swap_parents_def set_original_def
2987                         set_cdt_modify gets_fold_into_modify bind_assoc
2988                         cap_swap_ext_def update_cdt_list_def set_cdt_list_modify)
2989        apply (simp add: gets_fold_into_modify modify_modify Fun.swap_def o_def)
2990        apply (rule_tac P'="K (slot_a \<noteq> slot_b) and cte_at slot_a and cte_at slot_b
2991                              and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s))
2992                              and no_mloop o cdt"
2993                   and P=\<top> in corres_modify)
2994
2995        apply (clarsimp simp:transform_def transform_current_thread_def
2996                             transform_asid_table_def transform_objects_def
2997                             transform_cdt_def split del: if_split)
2998        apply (rule sym)
2999        apply (subgoal_tac "inj_on transform_cslot_ptr
3000                   ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s'))
3001                     \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b")
3002         apply (elim conjE)
3003         apply (subst map_lift_over_upd, erule subset_inj_on)
3004          apply (safe elim!: ranE, simp_all split: if_split_asm,
3005                 simp_all add: ranI)[1]
3006         apply (subst map_lift_over_upd, erule subset_inj_on)
3007          apply (safe elim!: ranE, simp_all split: if_split_asm,
3008                 simp_all add: ranI)[1]
3009         apply (subst map_lift_over_if_eq_twice)
3010          apply (erule subset_inj_on, fastforce)
3011         apply (rule ext)
3012         apply (cases slot_a, cases slot_b)
3013         apply (simp split del: if_split)
3014         apply (intro if_cong[OF refl],
3015                simp_all add: map_lift_over_eq_Some inj_on_eq_iff[where f=transform_cslot_ptr]
3016                              ranI domI)[1]
3017          apply (subst subset_inj_on, assumption, fastforce)+
3018          prefer 2
3019          apply (subst subset_inj_on, assumption, fastforce)+
3020          apply (auto simp: map_lift_over_eq_Some inj_on_eq_iff[where f=transform_cslot_ptr]
3021                            ranI domI
3022                     intro: map_lift_over_f_eq[THEN iffD2, OF _ refl]
3023                      elim: subset_inj_on)[2]
3024        apply (clarsimp simp: no_cdt_loop_mloop)
3025        apply (rule_tac s=s' in transform_cdt_slot_inj_on_cte_at[where P=\<top>])
3026        apply (auto simp: swp_def dest: mdb_cte_atD
3027                    elim!: ranE)[1]
3028       apply (wp set_cap_caps_of_state2 set_cap_idle
3029                  | simp add: swp_def cte_wp_at_caps_of_state)+
3030  apply clarsimp
3031  apply (clarsimp simp: cte_wp_at_caps_of_state valid_mdb_def)
3032  apply (safe intro!: mdb_cte_atI)
3033     apply (auto simp: swp_def cte_wp_at_caps_of_state not_idle_thread_def
3034                 dest: mdb_cte_atD elim!: ranE)
3035    done
3036qed
3037
3038lemma swap_for_delete_corres:
3039  "dcorres dc \<top> (valid_mdb and valid_idle and not_idle_thread (fst p)
3040                     and not_idle_thread (fst p') and valid_etcbs and (\<lambda>_. p \<noteq> p'))
3041      (swap_for_delete (transform_cslot_ptr p) (transform_cslot_ptr p'))
3042      (cap_swap_for_delete p p')"
3043  apply (rule corres_gen_asm2)
3044  apply (simp add: swap_for_delete_def cap_swap_for_delete_def when_def)
3045  apply (rule corres_guard_imp)
3046    apply (rule corres_split[OF _ get_cap_corres[OF refl]])+
3047        apply simp
3048        apply (rule swap_cap_corres)
3049       apply (wp get_cap_wp)+
3050   apply simp
3051  apply (clarsimp simp: cte_wp_at_caps_of_state)
3052  done
3053
3054definition
3055  "arch_page_vmpage_size cap \<equiv>
3056   case cap of cap.ArchObjectCap (arch_cap.PageCap dev _ _ sz _) \<Rightarrow> sz
3057         | _ \<Rightarrow> undefined"
3058
3059lemma set_cap_noop_dcorres3:
3060  "dcorres dc \<top> (cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap'
3061                                 \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr)
3062    (return ()) (set_cap cap ptr)"
3063  apply (rule corres_noop, simp_all)
3064  apply (simp add: set_cap_def split_def set_object_def)
3065  apply (wp get_object_wp | wpc)+
3066  apply (clarsimp simp: obj_at_def)
3067  apply (erule cte_wp_atE)
3068   apply (clarsimp simp: transform_def transform_current_thread_def
3069                         transform_objects_def)
3070   apply (rule ext)
3071   apply (simp add: fun_upd_def[symmetric]
3072               del: dom_fun_upd)
3073   apply (simp add: restrict_map_def transform_cnode_contents_def
3074                    fun_eq_iff option_map_join_def map_add_def
3075             split: option.split nat.split)
3076  apply (clarsimp simp: transform_def transform_current_thread_def
3077                        transform_objects_def fun_eq_iff
3078                        arch_page_vmpage_size_def)
3079  apply (simp add: restrict_map_def transform_cnode_contents_def map_add_def
3080                   transform_tcb_def fun_eq_iff infer_tcb_pending_op_def
3081            split: option.split cong: Structures_A.thread_state.case_cong)
3082  apply (subgoal_tac "snd ptr = tcb_cnode_index 4 \<longrightarrow>
3083                       (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns
3084                          = get_ipc_buffer_words ms tcb ns)")
3085   apply (simp cong: transform_full_intent_cong)
3086   apply (simp add: transform_full_intent_def Let_def get_tcb_message_info_def
3087                    get_tcb_mrs_def)
3088   apply fastforce
3089  apply clarsimp
3090  apply (simp add: transform_cap_def split: cap.split_asm arch_cap.split_asm if_split_asm,
3091         simp_all add: get_ipc_buffer_words_def)
3092  done
3093
3094lemma finalise_zombie:
3095  "is_zombie cap \<Longrightarrow> finalise_cap cap final
3096        = do assert final; return (cap, cap.NullCap) od"
3097  by (clarsimp simp add: is_cap_simps)
3098
3099lemma corres_assert_rhs:
3100  "(F \<Longrightarrow> corres_underlying sr False False r P P' f (g ()))
3101    \<Longrightarrow> corres_underlying sr False False r P (\<lambda>s. F \<longrightarrow> P' s) f (assert F >>= g)"
3102  by (cases F, simp_all add: corres_fail)
3103
3104lemma monadic_rewrite_select_x:
3105  "monadic_rewrite F False
3106      (\<lambda>s. x \<in> S) (select S) (return x)"
3107  by (simp add: monadic_rewrite_def return_def select_def)
3108
3109lemmas monadic_rewrite_select_pick_x
3110    = monadic_rewrite_bind_head
3111         [OF monadic_rewrite_select_x[where x=x], simplified,
3112          THEN monadic_rewrite_trans] for x
3113
3114lemma finalise_cap_zombie':
3115  "(case cap of ZombieCap _ \<Rightarrow> True | _ \<Rightarrow> False)
3116     \<Longrightarrow> CSpace_D.finalise_cap cap fin =
3117              do assert fin; return (cap, cdl_cap.NullCap) od"
3118  by (simp split: cdl_cap.split_asm)
3119
3120lemma corres_use_cutMon:
3121  "\<lbrakk> \<And>s. corres_underlying sr False fl r P P' f (cutMon ((=) s) g) \<rbrakk>
3122       \<Longrightarrow> corres_underlying sr False fl r P P' f g"
3123  apply atomize
3124  apply (simp add: corres_underlying_def cutMon_def fail_def
3125            split: if_split_asm)
3126  apply (clarsimp simp: split_def)
3127  done
3128
3129lemma corres_drop_cutMon:
3130  "corres_underlying sr False False r P P' f g
3131     \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g)"
3132  apply (simp add: corres_underlying_def cutMon_def fail_def
3133            split: if_split)
3134  apply (clarsimp simp: split_def)
3135  done
3136
3137lemma corres_drop_cutMon_bind:
3138  "corres_underlying sr False False r P P' f (g >>= h)
3139     \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g >>= h)"
3140  apply (simp add: corres_underlying_def cutMon_def fail_def bind_def
3141            split: if_split)
3142  apply (clarsimp simp: split_def)
3143  done
3144
3145lemma corres_drop_cutMon_bindE:
3146  "corres_underlying sr False False r P P' f (g >>=E h)
3147     \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g >>=E h)"
3148  apply (simp add: bindE_def)
3149  apply (erule corres_drop_cutMon_bind)
3150  done
3151
3152lemma corres_cutMon:
3153  "\<lbrakk> \<And>s. Q s \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon ((=) s) g) \<rbrakk>
3154         \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g)"
3155  apply atomize
3156  apply (simp add: corres_underlying_def cutMon_def fail_def
3157            split: if_split_asm)
3158  apply (clarsimp simp: split_def)
3159  done
3160
3161lemma underlying_memory_irq_state_independent[intro!, simp]:
3162  "underlying_memory (s\<lparr>irq_state := f (irq_state s)\<rparr>)
3163   = underlying_memory s"
3164  by simp
3165
3166lemma get_ipc_buffer_words_irq_state_independent[intro!, simp]:
3167  "get_ipc_buffer_words (s\<lparr>irq_state := f (irq_state s)\<rparr>)
3168   = get_ipc_buffer_words s"
3169  apply (rule ext, rule ext)
3170  apply (simp add: get_ipc_buffer_words_def)
3171  apply (case_tac "tcb_ipcframe x", simp_all)
3172  apply (clarsimp split: ARM_A.arch_cap.splits)
3173  apply (rule arg_cong[where f=the])
3174  apply (rule evalMonad_mapM_cong)
3175    apply (simp add: evalMonad_def)
3176    apply safe
3177      apply ((clarsimp simp: loadWord_def bind_def gets_def get_def return_def in_monad)+)[3]
3178   apply (rule loadWord_inv)
3179  apply (rule df_loadWord)
3180  done
3181
3182lemma get_tcb_mrs_irq_state_independent[intro!, simp]:
3183  "get_tcb_mrs (s\<lparr>irq_state := f (irq_state s)\<rparr>)
3184   = get_tcb_mrs s"
3185  by (auto simp: get_tcb_mrs_def)
3186
3187lemma transform_full_intent_irq_state_independent[intro!, simp]:
3188  "transform_full_intent (s\<lparr>irq_state := f (irq_state s)\<rparr>)
3189   = transform_full_intent s"
3190  by (rule ext, rule ext, simp add: transform_full_intent_def)
3191
3192lemma transform_tcb_irq_state_independent[intro!, simp]:
3193  "transform_tcb (s\<lparr>irq_state := f (irq_state s)\<rparr>)
3194   = transform_tcb s"
3195  by (rule ext, rule ext, rule ext, simp add: transform_tcb_def)
3196
3197lemma transform_object_irq_state_independent[intro!, simp]:
3198  "transform_object (s \<lparr> irq_state := f (irq_state s) \<rparr>)
3199   = transform_object s"
3200  by (rule ext, rule ext, rule ext,
3201      simp add: transform_object_def
3202         split: Structures_A.kernel_object.splits)
3203
3204lemma transform_objects_irq_state_independent[intro!, simp]:
3205  "transform_objects (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>)
3206   = transform_objects s"
3207  by (simp add: transform_objects_def)
3208
3209lemma transform_irq_state_independent[intro!, simp]:
3210  "transform (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>)
3211   = transform s"
3212  by (simp add: transform_def transform_current_thread_def)
3213
3214lemma transform_work_units_independent[intro!, simp]:
3215  "transform (s \<lparr> work_units_completed := f (work_units_completed s) \<rparr>)
3216   = transform s"
3217  apply (simp add: transform_def transform_current_thread_def transform_objects_def transform_cdt_def transform_asid_table_def)
3218  done
3219
3220lemma transform_work_units_then_irq_state_independent[intro!, simp]:
3221  "transform (s \<lparr> work_units_completed := g (work_units_completed s) \<rparr>
3222                \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>) =
3223   transform s"
3224  apply (simp add: transform_def transform_current_thread_def transform_objects_def transform_cdt_def transform_asid_table_def)
3225  done
3226
3227lemma throw_or_return_preemption_corres:
3228  "dcorres (dc \<oplus> dc) P P'
3229       (Monads_D.throw \<sqinter> returnOk ())
3230       preemption_point"
3231  apply (simp add: preemption_point_def)
3232  apply (auto simp: preemption_point_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
3233                    corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
3234                    alternative_def throwError_def returnOk_def return_def lift_def
3235                    put_def do_machine_op_def
3236                    update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def
3237                    work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
3238           split: option.splits kernel_object.splits)
3239  done
3240
3241lemma cutMon_fail:
3242  "cutMon P fail = fail"
3243  by (simp add: cutMon_def)
3244
3245declare rec_del.simps[simp del]
3246
3247lemma select_pick_corres_asm:
3248  "\<lbrakk> x \<in> S; corres_underlying sr nf nf' r P Q (f x) g \<rbrakk>
3249    \<Longrightarrow> corres_underlying sr nf nf' r P Q (select S >>= f) g"
3250  by (drule select_pick_corres[where x=x and S=S], simp)
3251
3252lemma invs_weak_valid_mdb:
3253  "invs s \<longrightarrow> weak_valid_mdb s"
3254  by (simp add: weak_valid_mdb_def invs_def valid_mdb_def valid_state_def)
3255
3256lemma invs_valid_idle_strg:
3257  "invs s \<longrightarrow> valid_idle s"
3258  by auto
3259
3260lemma cutMon_validE_R_drop:
3261  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>,-"
3262  by (simp add: validE_R_def validE_def cutMon_valid_drop)
3263
3264crunch idle_thread [wp]: cap_swap_for_delete "\<lambda>s::'a::state_ext state. P (idle_thread s)"
3265  (wp: dxo_wp_weak)
3266
3267crunch idle_thread [wp]: finalise_cap "\<lambda>s. P (idle_thread s)"
3268 (wp: crunch_wps simp: crunch_simps)
3269
3270lemma preemption_point_idle_thread[wp]: "\<lbrace> \<lambda>s. P (idle_thread s) \<rbrace> preemption_point \<lbrace> \<lambda>_ s. P (idle_thread s) \<rbrace>"
3271  apply (simp add: preemption_point_def OR_choiceE_def)
3272  apply (wpsimp wp: hoare_drop_imps dxo_wp_weak[where P="\<lambda>s. P (idle_thread s)"])
3273  done
3274
3275lemma rec_del_idle_thread[wp]:
3276  "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> rec_del args \<lbrace>\<lambda>rv s::'a::state_ext state. P (idle_thread s)\<rbrace>"
3277  by (wp rec_del_preservation | simp)+
3278
3279lemmas gets_constant = gets_to_return
3280
3281lemma monadic_rewrite_gets_the_gets:
3282  "monadic_rewrite F E (\<lambda>s. f s \<noteq> None) (gets_the f) (gets (the o f))"
3283  apply (simp add: monadic_rewrite_def gets_the_def assert_opt_def exec_gets
3284            split: option.split)
3285  apply (auto simp: simpler_gets_def return_def)
3286  done
3287
3288lemmas corres_gets_the_bind
3289    = monadic_rewrite_corres2[OF monadic_rewrite_bind_head [OF monadic_rewrite_gets_the_gets]]
3290
3291lemma finalise_slot_inner1_add_if_Null:
3292  "monadic_rewrite F False \<top>
3293     (finalise_slot_inner1 victim)
3294     (do cap \<leftarrow> KHeap_D.get_cap victim;
3295        if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True)
3296        else do
3297          final \<leftarrow> PageTableUnmap_D.is_final_cap cap;
3298          (cap', irqopt) \<leftarrow> CSpace_D.finalise_cap cap final;
3299          removeable \<leftarrow> gets $ CSpace_D.cap_removeable cap' victim;
3300          when (\<not> removeable) (KHeap_D.set_cap victim cap')
3301               \<sqinter> KHeap_D.set_cap victim cap';
3302          return (cap', removeable)
3303       od
3304     od)"
3305  apply (simp add: finalise_slot_inner1_def)
3306  apply (rule monadic_rewrite_imp)
3307   apply (rule monadic_rewrite_bind_tail)
3308    apply (rule monadic_rewrite_if_rhs)
3309     apply (simp add: PageTableUnmap_D.is_final_cap_def)
3310     apply (rule monadic_rewrite_trans)
3311      apply (rule monadic_rewrite_bind_tail[where j="\<lambda>_. j" for j, OF _ gets_wp])+
3312      apply (rename_tac remove, rule_tac P=remove in monadic_rewrite_gen_asm)
3313      apply simp
3314      apply (rule monadic_rewrite_refl)
3315     apply (simp add: gets_bind_ign when_def)
3316     apply (rule monadic_rewrite_trans)
3317      apply (rule monadic_rewrite_bind_head)
3318      apply (rule monadic_rewrite_pick_alternative_1)
3319     apply simp
3320     apply (rule monadic_rewrite_refl)
3321    apply (rule monadic_rewrite_refl)
3322   apply wp
3323  apply (clarsimp simp: CSpace_D.cap_removeable_def)
3324  done
3325
3326lemma corres_if_rhs_only:
3327  "\<lbrakk> G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q a b;
3328      \<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P' Q' a c\<rbrakk>
3329       \<Longrightarrow> corres_underlying sr nf nf' rvr
3330             (P and P') (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not> G \<longrightarrow> Q' s))
3331             a (if G then b else c)"
3332  by (rule corres_guard_imp, rule corres_if_rhs, simp+)
3333
3334lemma OR_choiceE_det:
3335  "\<lbrakk>det c; \<And>P. \<lbrace>P\<rbrace> c \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> (OR_choiceE c (f :: ('a + 'b) det_ext_monad) g)
3336     = (doE rv \<leftarrow> liftE c; if rv then f else g odE)"
3337  apply (rule ext)
3338  apply (clarsimp simp: OR_choiceE_def select_f_def bind_def det_def valid_def
3339               wrap_ext_bool_det_ext_ext_def get_def bindE_def ethread_get_def split_def
3340               gets_the_def assert_opt_def return_def gets_def fail_def mk_ef_def liftE_def no_fail_def
3341               split: option.splits prod.splits)
3342  apply atomize
3343  apply (erule_tac x="(=) x" in allE)
3344  apply (erule_tac x=x in allE)+
3345  apply clarsimp
3346  done
3347
3348lemma transform_work_units_completed_update[simp]: "transform (s\<lparr> work_units_completed := a \<rparr>) = transform s"
3349  by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)
3350
3351lemma finalise_preemption_corres:
3352  "dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) \<top> \<top>
3353      (monadic_trancl_preemptible finalise_slot_inner2 S) (preemption_point)"
3354  apply (simp add: finalise_slot_inner2_def preemption_point_def split_def)
3355  apply (subst OR_choiceE_det)
3356    apply (simp add: work_units_limit_reached_def)
3357   apply ((simp add: work_units_limit_reached_def | wp)+)[1]
3358  apply (rule corres_guard_imp)
3359
3360
3361    apply (rule dcorres_symb_exec_rE)
3362      apply (rule dcorres_symb_exec_rE)
3363        apply simp
3364        apply (rule conjI, clarsimp)
3365         apply (rule dcorres_symb_exec_rE)
3366           apply (rule dcorres_symb_exec_rE)
3367             apply (simp split: option.splits)
3368             apply (rule conjI, clarsimp)
3369              apply (rule monadic_rewrite_corres2)
3370               apply (rule monadic_trancl_preemptible_return)
3371              apply (rule dcorres_returnOk, simp)
3372             apply clarsimp
3373             apply (rule corres_guard_imp)
3374               apply (rule monadic_rewrite_corres2)
3375                apply (rule monadic_trancl_preemptible_f)
3376               apply (rule corres_alternate2[OF dcorres_throw], simp_all)[4]
3377           apply ((wp | simp)+)[1]
3378          apply (rule hoare_TrueI)
3379         apply ((simp add: reset_work_units_def | wp)+)[1]
3380        apply clarsimp
3381        apply (rule corres_guard_imp)
3382          apply (rule monadic_rewrite_corres2)
3383           apply (rule monadic_trancl_preemptible_return)
3384          apply (rule dcorres_returnOk, simp_all)[3]
3385       apply (rule hoare_TrueI)
3386      apply ((simp add: work_units_limit_reached_def | wp)+)[1]
3387     apply (rule hoare_TrueI)
3388    apply (simp add: update_work_units_def | wp)+
3389  done
3390
3391lemma zombie_is_cap_toE_pre2:
3392  "\<lbrakk> s \<turnstile> cap.Zombie ptr zbits n; m < n \<rbrakk>
3393     \<Longrightarrow> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs (cap.Zombie ptr zbits n) irqn"
3394  apply (clarsimp simp add: valid_cap_def cap_aligned_def)
3395  apply (clarsimp split: option.split_asm)
3396   apply (simp add: unat_of_bl_nat_to_cref)
3397   apply (simp add: nat_to_cref_def word_bits_conv)
3398  apply (simp add: unat_of_bl_nat_to_cref)
3399  apply (simp add: nat_to_cref_def word_bits_conv)
3400  done
3401
3402lemma corres_note_assumption:
3403  "\<lbrakk> F; corres_underlying sr fl fl' r P P' f g \<rbrakk>
3404        \<Longrightarrow> corres_underlying sr fl fl' r (\<lambda>s. F \<longrightarrow> P s) P' f g"
3405  by simp
3406
3407lemma corres_req2:
3408  "\<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> F; F \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g\<rbrakk>
3409         \<Longrightarrow> corres_underlying sr nf nf' r (P and Q) (P' and Q') f g"
3410  apply (rule_tac F=F in corres_req, simp_all)
3411  apply (erule corres_guard_imp, simp_all)
3412  done
3413
3414lemma nat_split_conv_to_if:
3415  "(case n of 0 \<Rightarrow> a | Suc nat' \<Rightarrow> f nat') = (if n = 0 then a else f (n - 1))"
3416  by (auto split: nat.splits)
3417
3418lemma opt_cap_cnode:
3419  "\<lbrakk> kheap s y = Some (CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn \<rbrakk>
3420    \<Longrightarrow> (opt_cap (y, node) (transform s) = Some cap)
3421           = (\<exists>v cap'. transform_cslot_ptr (y, v) = (y, node)
3422                   \<and> cn v = Some cap' \<and> cap = transform_cap cap')"
3423  apply clarsimp
3424  apply (simp add: opt_cap_def slots_of_def opt_object_def
3425                   transform_def transform_objects_def restrict_map_def
3426                   transform_cnode_contents_def option_map_join_def
3427                   transform_cslot_ptr_def object_slots_def
3428                   nat_split_conv_to_if
3429            split: option.split)
3430  apply (case_tac "sz = 0")
3431   apply (clarsimp, rule conjI)
3432    apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD)
3433   apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2
3434                             option.inject wf_cs_nD) (* slow 20s *)
3435  (* "sz \<noteq> 0" *)
3436  apply (clarsimp, rule conjI)
3437   apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD)
3438  apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2
3439                            option.inject wf_cs_nD) (* slow 30s *)
3440  done
3441
3442lemma preemption_point_valid_etcbs[wp]: "\<lbrace> valid_etcbs \<rbrace> preemption_point \<lbrace> \<lambda>_. valid_etcbs \<rbrace>"
3443  apply (clarsimp simp: preemption_point_def)
3444  apply (auto simp: valid_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
3445                    corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
3446                    alternative_def throwError_def returnOk_def return_def lift_def
3447                    put_def do_machine_op_def
3448                    update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def
3449                    work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
3450           split: option.splits kernel_object.splits)
3451  done
3452
3453crunch valid_etcbs[wp]: cap_swap_ext, cap_swap_for_delete "valid_etcbs"
3454
3455lemma rec_del_valid_etcbs[wp]:
3456  "\<lbrace> valid_etcbs \<rbrace> rec_del args \<lbrace>\<lambda>_. valid_etcbs \<rbrace>"
3457  by (wp rec_del_preservation | simp)+
3458
3459lemma dcorres_rec_del:
3460  "\<lbrakk> (case args of CTEDeleteCall slot e \<Rightarrow> \<not> e | _ \<Rightarrow> True);
3461           (transform_cslot_ptr (slot_rdcall args), \<not> exposed_rdcall args) \<in> fst S;
3462           (case args of ReduceZombieCall (cap.Zombie p zbits (Suc n)) _ _ \<Rightarrow>
3463               (transform_cslot_ptr (p, replicate (zombie_cte_bits zbits) False), True) \<in> fst S
3464              \<and> (transform_cslot_ptr (p, nat_to_cref (zombie_cte_bits zbits) n), True) \<in> fst S
3465               | _ \<Rightarrow> True) \<rbrakk>
3466   \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. (case args of FinaliseSlotCall _ _ \<Rightarrow>
3467                          fst rv' \<longrightarrow> (\<exists>v. (transform_cslot_ptr (slot_rdcall args), v) \<in> snd rv
3468                                 \<and> (\<not> exposed_rdcall args \<longrightarrow> v)) | _ \<Rightarrow> True)
3469                               \<and> fst S \<subseteq> fst rv))
3470      \<top>
3471      (invs and valid_rec_del_call args and cte_at (slot_rdcall args)
3472            and valid_etcbs
3473            and valid_pdpt_objs
3474            and emptyable (slot_rdcall args) and not_idle_thread (fst (slot_rdcall args))
3475            and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow>
3476                   ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s)
3477            and (\<lambda>s. case args of
3478                ReduceZombieCall cap sl ex \<Rightarrow> \<forall>t\<in>obj_refs cap. halted_if_tcb t s
3479                   | _ \<Rightarrow> True))
3480      (doE S' \<leftarrow> monadic_trancl_preemptible
3481           finalise_slot_inner2 S;
3482         whenE ((case args of ReduceZombieCall _ _ _ \<Rightarrow> False | _ \<Rightarrow> True)
3483              \<and> exposed_rdcall args
3484              \<and> \<not> (transform_cslot_ptr (slot_rdcall args)) \<in> fst ` snd S') Monads_D.throw;
3485         returnOk S'
3486       odE)
3487      (cutMon ((=) s) (rec_del args))"
3488proof (induct arbitrary: S rule: rec_del.induct,
3489       simp_all(no_asm) only: rec_del_fails fail_bindE corres_free_fail cutMon_fail)
3490  case (1 slot exposed s S)
3491  note ps = "1.prems"[simplified]
3492  hence nexp[simp]: "\<not> exposed" by simp
3493  show ?case
3494    using ps
3495    apply (simp add: dc_def[symmetric])
3496    apply (subst rec_del_simps_ext[unfolded split_def])
3497    apply simp
3498    apply (rule corres_guard_imp)
3499      apply (rule monadic_rewrite_corres2)
3500       apply (rule monadic_trancl_preemptible_steps)
3501      apply (simp add: cutMon_walk_bindE)
3502      apply (rule corres_splitEE)
3503         prefer 2
3504         apply (rule "1.hyps"[simplified, folded dc_def], assumption+)
3505        apply (rule corres_drop_cutMon)
3506        apply (simp add: liftME_def[symmetric])
3507        apply (rule_tac R="fst rv" in corres_cases)
3508         apply (simp add: when_def)
3509         apply (rule monadic_rewrite_corres2)
3510          apply (rule monadic_trancl_preemptible_f)
3511         apply (simp add: finalise_slot_inner2_def[unfolded split_def])
3512         apply (rule corres_alternate1, rule corres_alternate2)
3513         apply simp
3514         apply (rule select_pick_corres_asm)
3515          apply clarsimp
3516          apply assumption
3517         apply (simp add: liftM_def[symmetric] o_def dc_def[symmetric])
3518         apply (rule empty_slot_corres)
3519        apply (simp add: when_def)
3520        apply (rule monadic_rewrite_corres2)
3521         apply (rule monadic_trancl_preemptible_return)
3522        apply (rule corres_trivial, simp add: returnOk_liftE)
3523        apply wp
3524       apply (wp_trace cutMon_validE_R_drop rec_del_invs
3525                  | simp add: not_idle_thread_def
3526                  | strengthen invs_weak_valid_mdb invs_valid_idle_strg
3527                  | rule hoare_vcg_E_elim[rotated])+
3528
3529    done
3530next
3531  case (2 slot exposed s S)
3532  note if_split[split del]
3533  have removeables:
3534    "\<And>s cap fin. \<lbrakk> cte_wp_at ((=) cap) slot s; s \<turnstile> remainder_cap fin cap; invs s; valid_etcbs s;
3535            CSpace_A.cap_removeable (remainder_cap fin cap) slot  \<rbrakk>
3536      \<Longrightarrow> CSpace_D.cap_removeable (transform_cap (remainder_cap fin cap))
3537                 (transform_cslot_ptr slot) (transform s)"
3538    apply (case_tac "remainder_cap fin cap = cap.NullCap")
3539     apply (simp add: CSpace_D.cap_removeable_def)
3540    apply (clarsimp simp: remainder_cap_def valid_cap_simps
3541                          cte_wp_at_caps_of_state
3542                   split: cap.split_asm if_split_asm)
3543    apply (rename_tac word nat option)
3544    apply (frule valid_global_refsD2, clarsimp)
3545    apply (clarsimp simp: CSpace_D.cap_removeable_def)
3546    apply (subgoal_tac "\<exists>x cap. (word, b) = transform_cslot_ptr (word, x)
3547                              \<and> caps_of_state s (word, x) = Some cap \<and> cap \<noteq> cap.NullCap")
3548     apply clarsimp
3549     apply (case_tac "(word, x) \<in> cte_refs (the (caps_of_state s slot)) (interrupt_irq_node s)")
3550      apply (clarsimp simp: unat_eq_0)
3551      apply (drule of_bl_eq_0)
3552       apply (simp add: cap_aligned_def word_bits_conv split: option.split_asm)
3553      apply clarsimp
3554     apply (frule zombie_cap_has_all[rotated -2], simp, clarsimp+)
3555    apply (clarsimp simp: tcb_at_def cap_range_def global_refs_def
3556                          opt_cap_tcb
3557                   split: option.split_asm if_split_asm | drule(1) valid_etcbs_get_tcb_get_etcb)+
3558       apply (rule_tac x="tcb_cnode_index b" in exI)
3559       apply (clarsimp simp: transform_cslot_ptr_def dest!: get_tcb_SomeD)
3560       apply (rule conjI, rule sym, rule bl_to_bin_tcb_cnode_index)
3561        apply (auto simp: tcb_slot_defs)[1]
3562       apply (rule iffD1[OF cte_wp_at_caps_of_state cte_wp_at_tcbI], (simp | rule conjI)+)
3563      apply (frule final_zombie_not_live[rotated 1, OF caps_of_state_cteD], clarsimp)
3564       apply (rule ccontr, erule zombies_finalE)
3565         apply (simp add: is_cap_simps)
3566        apply clarsimp
3567       apply (erule caps_of_state_cteD)
3568
3569      apply (clarsimp simp: obj_at_def live_def hyp_live_def dest!: get_tcb_SomeD)
3570      apply (auto simp: infer_tcb_pending_op_def)[1]
3571     apply (frule final_zombie_not_live[rotated 1, OF caps_of_state_cteD], clarsimp)
3572      apply (rule ccontr, erule zombies_finalE)
3573        apply (simp add: is_cap_simps)
3574       apply clarsimp
3575      apply (erule caps_of_state_cteD)
3576     apply (clarsimp simp: obj_at_def live_def hyp_live_def dest!: get_tcb_SomeD)
3577     apply (auto simp: infer_tcb_bound_notification_def)[1]
3578    apply (clarsimp simp: obj_at_def live_def hyp_live_def is_cap_table_def)
3579    apply (clarsimp simp: opt_cap_cnode
3580                   split: Structures_A.kernel_object.split_asm)
3581    apply (rule exI, rule conjI, erule sym)
3582    apply (rule iffD1[OF cte_wp_at_caps_of_state cte_wp_at_cteI],
3583             (simp | rule conjI)+)
3584    done
3585  show ?case
3586    using "2.prems"
3587    apply (simp add: dc_def[symmetric])
3588    apply (subst rec_del_simps_ext[unfolded split_def])
3589    apply (simp add: bindE_assoc, simp add: liftE_bindE)
3590    apply (rule stronger_corres_guard_imp)
3591      apply (simp add: cutMon_walk_bind)
3592      apply (rule corres_drop_cutMon_bind)
3593      apply (rule monadic_rewrite_corres2)
3594       apply (rule monadic_rewrite_bindE_head)
3595       apply (rule monadic_trancl_preemptible_step)
3596      apply (simp add: finalise_slot_inner2_def
3597                          [THEN fun_cong, unfolded split_def])
3598      apply (simp add: alternative_bindE_distrib)
3599      apply (rule corres_alternate1)+
3600      apply (simp add: liftE_bindE bind_bindE_assoc bind_assoc)
3601      apply (rule select_pick_corres_asm, assumption)
3602      apply (rule monadic_rewrite_corres2)
3603       apply (rule monadic_rewrite_bind_head)
3604       apply (rule finalise_slot_inner1_add_if_Null[unfolded split_def])
3605      apply (simp add: bind_assoc if_to_top_of_bind)
3606      apply (rule corres_split[OF _ get_cap_corres[OF refl]])
3607        apply (rename_tac cap)
3608        apply (rule corres_cutMon)
3609        apply (simp add: if_to_top_of_bindE cutMon_walk_if
3610                    del: transform_cap_Null)
3611        apply (rule Corres_UL.corres_if2[unfolded if_apply_def2])
3612          apply simp
3613         apply (rule corres_drop_cutMon)
3614         apply (rule corres_underlying_gets_pre_lhs)+
3615         apply (rule monadic_rewrite_corres2)
3616          apply (rule monadic_rewrite_bindE_head)
3617          apply (rule monadic_trancl_preemptible_return)
3618         apply simp
3619         apply (rule corres_trivial, simp add: returnOk_liftE)
3620        apply (rule_tac F="cap \<noteq> cap.NullCap" in corres_gen_asm2)
3621        apply (rule corres_cutMon)
3622        apply (simp add: cutMon_walk_bind del: fst_conv)
3623        apply (rule corres_drop_cutMon_bind)
3624        apply (rule corres_split [OF _ is_final_cap_corres[OF refl]])
3625           apply (rule corres_cutMon)
3626           apply (simp add: cutMon_walk_bind del: fst_conv)
3627           apply (rule corres_drop_cutMon_bind)
3628           apply (rule corres_split[OF _ dcorres_finalise_cap[where slot=slot]])
3629              apply (rename_tac fin fin')
3630              apply (rule corres_cutMon)
3631              apply (simp(no_asm) add: cutMon_walk_if)
3632              apply (rule corres_underlying_gets_pre_lhs)
3633              apply (rename_tac remove)
3634              apply (rule_tac P="\<lambda>s. remove = CSpace_D.cap_removeable (fst fin) (transform_cslot_ptr slot) s"
3635                         and P'="cte_wp_at ((=) cap) slot and invs and valid_etcbs and valid_cap (fst fin')"
3636                         and F="CSpace_A.cap_removeable (fst fin') slot \<longrightarrow> remove"
3637                              in corres_req2)
3638               apply (drule use_valid[OF _ finalise_cap_remainder, OF _ TrueI])
3639               apply (clarsimp simp: removeables)
3640              apply (rule corres_if_rhs_only)
3641               apply (rule_tac F=remove in corres_note_assumption, simp)
3642               apply (simp add: when_def)
3643               apply (rule monadic_rewrite_corres2)
3644                apply (rule monadic_rewrite_bind)
3645                  apply (rule monadic_rewrite_pick_alternative_1)
3646                 apply (rule monadic_rewrite_bind_tail)
3647                  apply (rule monadic_rewrite_bindE_head)
3648                  apply (rule monadic_trancl_preemptible_return)
3649                 apply wp+
3650               apply simp
3651               apply (rule corres_underlying_gets_pre_lhs)
3652               apply (rule corres_drop_cutMon)
3653               apply (rule corres_trivial, simp add: returnOk_liftE)
3654              apply (rule corres_if_rhs_only)
3655               apply simp
3656               apply (rule corres_drop_cutMon)
3657               apply (rule monadic_rewrite_corres2)
3658                apply (rule monadic_rewrite_bind)
3659                  apply (rule monadic_rewrite_pick_alternative_2)
3660                 apply (rule monadic_rewrite_bind_tail)
3661                  apply (rule monadic_trancl_preemptible_return)
3662                 apply wp+
3663               apply (rule corres_split[OF _ set_cap_corres])
3664                   apply (rule corres_underlying_gets_pre_lhs)
3665                   apply (rule corres_trivial, simp add: returnOk_liftE)
3666                  apply (wp | simp)+
3667              apply (rule monadic_rewrite_corres2)
3668               apply (rule monadic_rewrite_bind_head)
3669               apply (rule monadic_rewrite_pick_alternative_2)
3670              apply (simp add: cutMon_walk_bind)
3671              apply (rule corres_drop_cutMon_bind)
3672              apply (rule corres_split[OF _ set_cap_corres])
3673                  apply (rule_tac P="dcorres r P P' f" for r P P' f in subst)
3674                   apply (rule_tac f="\<lambda>_. ()" in gets_bind_ign)
3675                  apply (rule_tac r'="\<lambda>rv rv'. transform_cslot_ptr `
3676                                            (case fst fin' of cap.Zombie p zb (Suc n) \<Rightarrow>
3677                                                {(p, replicate (zombie_cte_bits zb) False),
3678                                                 (p, nat_to_cref (zombie_cte_bits zb) n)} | _ \<Rightarrow> {}) \<subseteq> rv"
3679                              and P=\<top> and P'="valid_cap (fst fin') and invs and valid_etcbs
3680                                                 and (\<lambda>s. idle_thread s \<notin> obj_refs (fst fin'))" in corres_split)
3681                     apply (rule monadic_rewrite_corres2)
3682                      apply (rule monadic_rewrite_bindE_head)
3683                      apply (rule monadic_rewrite_trans)
3684                       apply (rule monadic_trancl_preemptible_steps)
3685                      apply (rule monadic_rewrite_bindE[OF monadic_rewrite_refl])
3686                       apply (rule monadic_trancl_preemptible_steps)
3687                      apply wp
3688                     apply (rule corres_cutMon)
3689                     apply (simp add: cutMon_walk_bindE bindE_assoc)
3690                     apply (rule corres_splitEE)
3691                        prefer 2
3692                        apply (rule "2.hyps"[simplified, folded dc_def],
3693                                   (assumption | simp | rule conjI refl)+)
3694                        apply (clarsimp split: cap.split nat.split)
3695                       apply (rule corres_cutMon)
3696                       apply (simp add: cutMon_walk_bindE dc_def[symmetric])
3697                       apply (rule corres_drop_cutMon_bindE)
3698                       apply (rule corres_splitEE[OF _ finalise_preemption_corres])
3699                         apply (rule corres_cutMon)
3700                         apply (rule corres_rel_imp, rule "2.hyps"[simplified, folded dc_def],
3701                                  (assumption | simp | rule conjI refl)+)
3702                          apply clarsimp
3703                          apply blast
3704                         apply (rename_tac excr excr', case_tac excr, simp_all)[1]
3705                         apply clarsimp
3706                         apply blast
3707                        apply (wp cutMon_validE_R_drop rec_del_invs rec_del_cte_at
3708                                  rec_del_ReduceZombie_emptyable reduce_zombie_cap_to preemption_point_valid_etcbs preemption_point_inv
3709                                          | simp add: not_idle_thread_def del: gets_to_return)+
3710                    apply (clarsimp simp: get_zombie_range_def dom_def
3711                                   split: cap.split nat.split)
3712
3713                    apply (frule cte_at_nat_to_cref_zbits[OF _ lessI])
3714                    apply (frule cte_at_replicate_zbits)
3715                    apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap)
3716                    apply (clarsimp simp: transform_cslot_ptr_def)
3717                   apply (wp | simp)+
3718              apply (simp add: conj_comms)
3719              apply (wp replace_cap_invs final_cap_same_objrefs set_cap_cte_wp_at
3720                        hoare_vcg_const_Ball_lift set_cap_cte_cap_wp_to static_imp_wp
3721                          | erule finalise_cap_not_reply_master[simplified in_monad, simplified]
3722                          | simp only: not_idle_thread_def pred_conj_def simp_thms)+
3723           apply (rule hoare_strengthen_post)
3724            apply (rule_tac Q="\<lambda>fin s. invs s \<and> replaceable s slot (fst fin) cap
3725                                      \<and> valid_pdpt_objs s
3726                                      \<and> valid_etcbs s
3727                                      \<and> cte_wp_at ((=) cap) slot s \<and> s \<turnstile> fst fin
3728                                      \<and> emptyable slot s \<and> fst slot \<noteq> idle_thread s
3729                                      \<and> (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s)"
3730                       in hoare_vcg_conj_lift)
3731             apply (wp finalise_cap_invs[where slot=slot]
3732                       finalise_cap_replaceable
3733                       finalise_cap_makes_halted[where slot=slot]
3734                       hoare_vcg_disj_lift hoare_vcg_ex_lift)[1]
3735            apply (rule finalise_cap_cases[where slot=slot])
3736           apply clarsimp
3737           apply (frule if_unsafe_then_capD, clarsimp+)
3738           apply (clarsimp simp: cte_wp_at_caps_of_state)
3739           apply (frule valid_global_refsD2, clarsimp+)
3740           apply (erule disjE[where P="c = cap.NullCap \<and> P" for c P])
3741            apply clarsimp
3742           apply (clarsimp simp: conj_comms invs_valid_idle global_refs_def cap_range_def
3743                          dest!: is_cap_simps [THEN iffD1])
3744           apply (frule trans [OF _ appropriate_Zombie, OF sym])
3745           apply (case_tac cap,
3746                  simp_all add: fst_cte_ptrs_def is_cap_simps is_final_cap'_def)[1]
3747          apply assumption
3748         apply (wp get_cap_wp | simp add: is_final_cap_def)+
3749    apply (auto simp: not_idle_thread_def cte_wp_at_caps_of_state
3750                elim: caps_of_state_valid_cap)
3751    done
3752next
3753  case (3 ptr bits n slot s S)
3754  show ?case
3755    using "3.prems"
3756    apply (subst rec_del.simps)
3757    apply (clarsimp simp: assertE_assert liftE_bindE assert_def
3758                          corres_free_fail cutMon_fail)
3759    apply (case_tac "ptr = idle_thread s \<or> fst slot = idle_thread s")
3760     apply (clarsimp simp: cutMon_def corres_underlying_def fail_def)
3761     apply (clarsimp simp: cte_wp_at_caps_of_state
3762                    dest!: zombie_cap_two_nonidles)
3763    apply (rule corres_drop_cutMon)
3764    apply (simp add: liftME_def[symmetric] liftE_bindE[symmetric])
3765    apply (rule stronger_corres_guard_imp)
3766      apply (rule monadic_rewrite_corres2)
3767       apply (rule monadic_trancl_preemptible_f)
3768      apply (simp add: finalise_slot_inner2_def[unfolded split_def])
3769      apply (rule corres_alternate1, rule corres_alternate1, rule corres_alternate2)
3770      apply simp
3771      apply (rule_tac x="(p, p')" for p p' in select_pick_corres)
3772      apply (simp add: liftM_def[symmetric] o_def dc_def[symmetric])
3773      apply (rule swap_for_delete_corres)
3774     apply (clarsimp simp: cte_wp_at_caps_of_state)
3775     apply (frule(1) caps_of_state_valid, drule cte_at_replicate_zbits)
3776     apply (clarsimp simp: cte_wp_at_caps_of_state transform_cslot_ptr_inj)
3777    apply (clarsimp simp: cte_wp_at_caps_of_state)
3778    apply (auto simp: not_idle_thread_def dest: zombie_cap_two_nonidles)
3779    done
3780next
3781  case (4 ptr bits n slot s S)
3782  show ?case
3783    using "4.prems"
3784    apply (subst rec_del.simps)
3785    apply simp
3786    apply (rule stronger_corres_guard_imp)
3787      apply (simp add: cutMon_walk_bindE)
3788      apply (rule monadic_rewrite_corres2)
3789       apply (rule monadic_trancl_preemptible_steps)
3790      apply (rule corres_splitEE[OF _ "4.hyps"[simplified, folded dc_def]])
3791          apply (rule corres_drop_cutMon)
3792          apply (simp add: liftE_bindE)
3793          apply (rule corres_symb_exec_r)
3794             apply (simp add: liftME_def[symmetric] split del: if_split)
3795             apply (rule monadic_rewrite_corres2)
3796              apply (rule monadic_trancl_preemptible_return)
3797             apply (rule corres_if_rhs_only)
3798              apply (simp add: returnOk_liftE)
3799              apply (rule corres_add_noop_lhs,
3800                     simp only: liftM_def[symmetric] corres_liftM_simp)
3801              apply (simp add: o_def dc_def[symmetric])
3802              apply (rule set_cap_noop_dcorres3)
3803             apply (simp add: assertE_assert liftE_def)
3804             apply (rule corres_assert_rhs)
3805             apply (rule corres_trivial, simp add: returnOk_def)
3806            apply (rule hoare_strengthen_post, rule get_cap_cte_wp_at)
3807            apply (clarsimp simp: cte_wp_at_caps_of_state arch_page_vmpage_size_def)
3808           apply (wp | simp)+
3809         apply (simp add: in_monad)
3810        apply simp
3811       apply (wp cutMon_validE_R_drop)+
3812     apply clarsimp
3813    apply (clarsimp simp: cte_wp_at_caps_of_state halted_emptyable)
3814    apply (frule valid_global_refsD2, clarsimp+)
3815    apply (frule(1) caps_of_state_valid,
3816           drule_tac m=n in cte_at_nat_to_cref_zbits)
3817     apply simp
3818    apply (auto simp: cte_wp_at_caps_of_state not_idle_thread_def
3819                      global_refs_def cap_range_def
3820                elim: zombie_is_cap_toE[OF caps_of_state_cteD])
3821    done
3822qed
3823
3824lemma dcorres_finalise_slot:
3825  "dcorres (dc \<oplus> dc) \<top> (invs and cte_at slot and valid_etcbs and valid_pdpt_objs and emptyable slot
3826                            and not_idle_thread (fst slot))
3827    (CSpace_D.finalise_slot (transform_cslot_ptr slot))
3828    (rec_del (FinaliseSlotCall slot True))"
3829  apply (rule corres_use_cutMon)
3830  apply (cut_tac b="\<lambda>_. returnOk ()" and d="\<lambda>_. returnOk ()" and r=dc
3831                and args3="FinaliseSlotCall slot True"
3832                and S3="({(transform_cslot_ptr slot, False)}, {})" and s3=s
3833            in corres_splitEE[rotated, OF dcorres_rec_del wp_post_tautE wp_post_tautE])
3834      apply (simp_all add: bindE_assoc CSpace_D.finalise_slot_def split_def)
3835   apply (simp_all add: liftME_def[symmetric])
3836  apply (simp add: returnOk_def)
3837  done
3838
3839end
3840
3841end
3842