1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory Finalise_R
12imports
13  IpcCancel_R
14  InterruptAcc_R
15  Retype_R
16begin
17context begin interpretation Arch . (*FIXME: arch_split*)
18
19declare doUnbindNotification_def[simp]
20
21text {* Properties about empty_slot/emptySlot *}
22
23lemma case_Null_If:
24  "(case c of NullCap \<Rightarrow> a | _ \<Rightarrow> b) = (if c = NullCap then a else b)"
25  by (case_tac c, simp_all)
26
27crunch aligned'[wp]: emptySlot pspace_aligned' (simp: case_Null_If)
28crunch distinct'[wp]: emptySlot pspace_distinct' (simp: case_Null_If)
29
30lemma updateCap_cte_wp_at_cases:
31  "\<lbrace>\<lambda>s. (ptr = ptr' \<longrightarrow> cte_wp_at' (P \<circ> cteCap_update (K cap)) ptr' s) \<and> (ptr \<noteq> ptr' \<longrightarrow> cte_wp_at' P ptr' s)\<rbrace>
32     updateCap ptr cap
33   \<lbrace>\<lambda>rv. cte_wp_at' P ptr'\<rbrace>"
34  apply (clarsimp simp: valid_def)
35  apply (drule updateCap_stuff)
36  apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def)
37  done
38
39crunch cte_wp_at'[wp]: postCapDeletion, updateTrackedFreeIndex "cte_wp_at' P p"
40
41lemma updateFreeIndex_cte_wp_at:
42  "\<lbrace>\<lambda>s. cte_at' p s \<and> P (cte_wp_at' (if p = p' then P'
43      o (cteCap_update (capFreeIndex_update (K idx))) else P') p' s)\<rbrace>
44    updateFreeIndex p idx
45  \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p' s)\<rbrace>"
46  apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def
47        split del: if_split)
48  apply (rule hoare_pre)
49   apply (wp updateCap_cte_wp_at' getSlotCap_wp)
50  apply (clarsimp simp: cte_wp_at_ctes_of)
51  apply (cases "p' = p", simp_all)
52  apply (case_tac cte, simp)
53  done
54
55lemma emptySlot_cte_wp_cap_other:
56  "\<lbrace>(\<lambda>s. cte_wp_at' (\<lambda>c. P (cteCap c)) p s) and K (p \<noteq> p')\<rbrace>
57  emptySlot p' opt
58  \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>"
59  apply (rule hoare_gen_asm)
60  apply (simp add: emptySlot_def clearUntypedFreeIndex_def getSlotCap_def)
61  apply (rule hoare_pre)
62   apply (wp updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases
63             updateFreeIndex_cte_wp_at getCTE_wp' hoare_vcg_all_lift
64              | simp add:  | wpc
65              | wp_once hoare_drop_imps)+
66  done
67
68crunch typ_at'[wp]: emptySlot "\<lambda>s. P (typ_at' T p s)"
69lemmas clearUntypedFreeIndex_typ_ats[wp]
70    = typ_at_lifts[OF clearUntypedFreeIndex_typ_at']
71
72crunch tcb_at'[wp]: postCapDeletion "tcb_at' t"
73crunch ct[wp]: emptySlot "\<lambda>s. P (ksCurThread s)"
74crunch cur_tcb'[wp]: clearUntypedFreeIndex "cur_tcb'"
75  (ignore: setObject wp: cur_tcb_lift)
76
77crunch ksRQ[wp]: emptySlot "\<lambda>s. P (ksReadyQueues s)"
78crunch ksRQL1[wp]: emptySlot "\<lambda>s. P (ksReadyQueuesL1Bitmap s)"
79crunch ksRQL2[wp]: emptySlot "\<lambda>s. P (ksReadyQueuesL2Bitmap s)"
80crunch obj_at'[wp]: postCapDeletion "obj_at' P p"
81
82lemmas postCapDeletion_valid_queues[wp] =
83    valid_queues_lift [OF postCapDeletion_obj_at'
84                          postCapDeletion_pred_tcb_at'
85                          postCapDeletion_ksRQ]
86
87crunch inQ[wp]: clearUntypedFreeIndex "\<lambda>s. P (obj_at' (inQ d p) t s)"
88crunch tcbDomain[wp]: clearUntypedFreeIndex "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t"
89crunch tcbPriority[wp]: clearUntypedFreeIndex "obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t"
90
91lemma emptySlot_queues [wp]:
92  "\<lbrace>Invariants_H.valid_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
93  unfolding emptySlot_def
94  by (wp | wpcw | wp valid_queues_lift | simp)+
95
96crunch nosch[wp]: emptySlot "\<lambda>s. P (ksSchedulerAction s)"
97crunch ksCurDomain[wp]: emptySlot "\<lambda>s. P (ksCurDomain s)"
98
99lemma emptySlot_sch_act_wf [wp]:
100  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
101  emptySlot sl opt
102  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
103  apply (simp add: emptySlot_def case_Null_If)
104  apply (wp sch_act_wf_lift tcb_in_cur_domain'_lift | wpcw | simp)+
105  done
106
107lemma updateCap_valid_objs' [wp]:
108  "\<lbrace>valid_objs' and valid_cap' cap\<rbrace>
109  updateCap ptr cap \<lbrace>\<lambda>r. valid_objs'\<rbrace>"
110  unfolding updateCap_def
111  by (wp setCTE_valid_objs getCTE_wp) (clarsimp dest!: cte_at_cte_wp_atD)
112
113lemma updateFreeIndex_valid_objs' [wp]:
114  "\<lbrace>valid_objs'\<rbrace> clearUntypedFreeIndex ptr \<lbrace>\<lambda>r. valid_objs'\<rbrace>"
115  apply (simp add: clearUntypedFreeIndex_def getSlotCap_def)
116  apply (wp getCTE_wp' | wpc | simp add: updateTrackedFreeIndex_def)+
117  done
118
119crunch valid_objs'[wp]: emptySlot "valid_objs'"
120
121crunch state_refs_of'[wp]: setInterruptState "\<lambda>s. P (state_refs_of' s)"
122  (simp: state_refs_of'_pspaceI)
123crunch state_refs_of'[wp]: emptySlot "\<lambda>s. P (state_refs_of' s)"
124  (wp: crunch_wps)
125
126lemma mdb_chunked2D:
127  "\<lbrakk> mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p'';
128     m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd'');
129     sameRegionAs cap cap''; p \<noteq> p'' \<rbrakk>
130     \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') \<and> sameRegionAs cap cap'"
131  apply (subgoal_tac "\<exists>cap' nd'. m p' = Some (CTE cap' nd')")
132   apply (clarsimp simp add: mdb_chunked_def)
133   apply (drule spec[where x=p])
134   apply (drule spec[where x=p''])
135   apply clarsimp
136   apply (drule mp, erule trancl_into_trancl2)
137    apply (erule trancl.intros(1))
138   apply (simp add: is_chunk_def)
139   apply (drule spec, drule mp, erule trancl.intros(1))
140   apply (drule mp, rule trancl_into_rtrancl)
141    apply (erule trancl.intros(1))
142   apply clarsimp
143  apply (clarsimp simp: mdb_next_unfold)
144  apply (case_tac z, simp)
145  done
146
147lemma nullPointer_eq_0_simp[simp]:
148  "(nullPointer = 0) = True"
149  "(0 = nullPointer) = True"
150  by (simp add: nullPointer_def)+
151
152lemma capRange_Null [simp]:
153  "capRange NullCap = {}"
154  by (simp add: capRange_def)
155
156lemma no_0_no_0_lhs_trancl [simp]:
157  "no_0 m \<Longrightarrow> \<not> m \<turnstile> 0 \<leadsto>\<^sup>+ x"
158  by (rule, drule tranclD, clarsimp simp: next_unfold')
159
160lemma no_0_no_0_lhs_rtrancl [simp]:
161  "\<lbrakk> no_0 m; x \<noteq> 0 \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> 0 \<leadsto>\<^sup>* x"
162  by (clarsimp dest!: rtranclD)
163
164end
165locale mdb_empty =
166  mdb_ptr?: mdb_ptr m _ _ slot s_cap s_node
167    for m slot s_cap s_node +
168
169  fixes n
170  defines "n \<equiv>
171           modify_map
172             (modify_map
173               (modify_map
174                 (modify_map m (mdbPrev s_node)
175                   (cteMDBNode_update (mdbNext_update (%_. (mdbNext s_node)))))
176                 (mdbNext s_node)
177                 (cteMDBNode_update
178                   (\<lambda>mdb. mdbFirstBadged_update (%_. (mdbFirstBadged mdb \<or> mdbFirstBadged s_node))
179                           (mdbPrev_update (%_. (mdbPrev s_node)) mdb))))
180               slot (cteCap_update (%_. capability.NullCap)))
181              slot (cteMDBNode_update (const nullMDBNode))"
182begin
183interpretation Arch . (*FIXME: arch_split*)
184
185lemmas m_slot_prev = m_p_prev
186lemmas m_slot_next = m_p_next
187lemmas prev_slot_next = prev_p_next
188lemmas next_slot_prev = next_p_prev
189
190lemma n_revokable:
191  "n p = Some (CTE cap node) \<Longrightarrow>
192  (\<exists>cap' node'. m p = Some (CTE cap' node') \<and>
193              (if p = slot
194               then \<not> mdbRevocable node
195               else mdbRevocable node = mdbRevocable node'))"
196  by (auto simp add: n_def modify_map_if nullMDBNode_def split: if_split_asm)
197
198lemma m_revokable:
199  "m p = Some (CTE cap node) \<Longrightarrow>
200  (\<exists>cap' node'. n p = Some (CTE cap' node') \<and>
201              (if p = slot
202               then \<not> mdbRevocable node'
203               else mdbRevocable node' = mdbRevocable node))"
204  apply (clarsimp simp add: n_def modify_map_if nullMDBNode_def split: if_split_asm)
205  apply (cases "p=slot", simp)
206  apply (cases "p=mdbNext s_node", simp)
207   apply (cases "p=mdbPrev s_node", simp)
208   apply clarsimp
209  apply simp
210  apply (cases "p=mdbPrev s_node", simp)
211  apply simp
212  done
213
214lemma no_0_n:
215  "no_0 n"
216  using no_0 by (simp add: n_def)
217
218lemma n_next:
219  "n p = Some (CTE cap node) \<Longrightarrow>
220  (\<exists>cap' node'. m p = Some (CTE cap' node') \<and>
221              (if p = slot
222               then mdbNext node = 0
223               else if p = mdbPrev s_node
224               then mdbNext node = mdbNext s_node
225               else mdbNext node = mdbNext node'))"
226  apply (subgoal_tac "p \<noteq> 0")
227   prefer 2
228   apply (insert no_0_n)[1]
229   apply clarsimp
230  apply (cases "p = slot")
231   apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm)
232  apply (cases "p = mdbPrev s_node")
233   apply (auto simp: n_def modify_map_if initMDBNode_def split: if_split_asm)
234  done
235
236lemma n_prev:
237  "n p = Some (CTE cap node) \<Longrightarrow>
238  (\<exists>cap' node'. m p = Some (CTE cap' node') \<and>
239              (if p = slot
240               then mdbPrev node = 0
241               else if p = mdbNext s_node
242               then mdbPrev node = mdbPrev s_node
243               else mdbPrev node = mdbPrev node'))"
244  apply (subgoal_tac "p \<noteq> 0")
245   prefer 2
246   apply (insert no_0_n)[1]
247   apply clarsimp
248  apply (cases "p = slot")
249   apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm)
250  apply (cases "p = mdbNext s_node")
251   apply (auto simp: n_def modify_map_if initMDBNode_def split: if_split_asm)
252  done
253
254lemma n_cap:
255  "n p = Some (CTE cap node) \<Longrightarrow>
256  \<exists>cap' node'. m p = Some (CTE cap' node') \<and>
257              (if p = slot
258               then cap = NullCap
259               else cap' = cap)"
260  apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm)
261   apply (cases node)
262   apply auto
263  done
264
265lemma m_cap:
266  "m p = Some (CTE cap node) \<Longrightarrow>
267  \<exists>cap' node'. n p = Some (CTE cap' node') \<and>
268              (if p = slot
269               then cap' = NullCap
270               else cap' = cap)"
271  apply (clarsimp simp: n_def modify_map_cases initMDBNode_def)
272  apply (cases node)
273  apply clarsimp
274  apply (cases "p=slot", simp)
275  apply clarsimp
276  apply (cases "mdbNext s_node = p", simp)
277   apply fastforce
278  apply simp
279  apply (cases "mdbPrev s_node = p", simp)
280  apply fastforce
281  done
282
283lemma n_badged:
284  "n p = Some (CTE cap node) \<Longrightarrow>
285  \<exists>cap' node'. m p = Some (CTE cap' node') \<and>
286              (if p = slot
287               then \<not> mdbFirstBadged node
288               else if p = mdbNext s_node
289               then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node)
290               else mdbFirstBadged node = mdbFirstBadged node')"
291  apply (subgoal_tac "p \<noteq> 0")
292   prefer 2
293   apply (insert no_0_n)[1]
294   apply clarsimp
295  apply (cases "p = slot")
296   apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm)
297  apply (cases "p = mdbNext s_node")
298   apply (auto simp: n_def modify_map_if nullMDBNode_def split: if_split_asm)
299  done
300
301lemma m_badged:
302  "m p = Some (CTE cap node) \<Longrightarrow>
303  \<exists>cap' node'. n p = Some (CTE cap' node') \<and>
304              (if p = slot
305               then \<not> mdbFirstBadged node'
306               else if p = mdbNext s_node
307               then mdbFirstBadged node' = (mdbFirstBadged node \<or> mdbFirstBadged s_node)
308               else mdbFirstBadged node' = mdbFirstBadged node)"
309  apply (subgoal_tac "p \<noteq> 0")
310   prefer 2
311   apply (insert no_0_n)[1]
312   apply clarsimp
313  apply (cases "p = slot")
314   apply (clarsimp simp: n_def modify_map_if nullMDBNode_def split: if_split_asm)
315  apply (cases "p = mdbNext s_node")
316   apply (clarsimp simp: n_def modify_map_if nullMDBNode_def split: if_split_asm)
317  apply clarsimp
318  apply (cases "p = mdbPrev s_node")
319   apply (auto simp: n_def modify_map_if initMDBNode_def  split: if_split_asm)
320  done
321
322lemmas slot = m_p
323
324lemma m_next:
325  "m p = Some (CTE cap node) \<Longrightarrow>
326  \<exists>cap' node'. n p = Some (CTE cap' node') \<and>
327              (if p = slot
328               then mdbNext node' = 0
329               else if p = mdbPrev s_node
330               then mdbNext node' = mdbNext s_node
331               else mdbNext node' = mdbNext node)"
332  apply (subgoal_tac "p \<noteq> 0")
333   prefer 2
334   apply clarsimp
335  apply (cases "p = slot")
336   apply (clarsimp simp: n_def modify_map_if)
337  apply (cases "p = mdbPrev s_node")
338   apply (simp add: n_def modify_map_if)
339  apply simp
340  apply (simp add: n_def modify_map_if)
341  apply (cases "mdbNext s_node = p")
342   apply fastforce
343  apply fastforce
344  done
345
346lemma m_prev:
347  "m p = Some (CTE cap node) \<Longrightarrow>
348  \<exists>cap' node'. n p = Some (CTE cap' node') \<and>
349              (if p = slot
350               then mdbPrev node' = 0
351               else if p = mdbNext s_node
352               then mdbPrev node' = mdbPrev s_node
353               else mdbPrev node' = mdbPrev node)"
354  apply (subgoal_tac "p \<noteq> 0")
355   prefer 2
356   apply clarsimp
357  apply (cases "p = slot")
358   apply (clarsimp simp: n_def modify_map_if)
359  apply (cases "p = mdbPrev s_node")
360   apply (simp add: n_def modify_map_if)
361  apply simp
362  apply (simp add: n_def modify_map_if)
363  apply (cases "mdbNext s_node = p")
364   apply fastforce
365  apply fastforce
366  done
367
368lemma n_nextD:
369  "n \<turnstile> p \<leadsto> p' \<Longrightarrow>
370  if p = slot then p' = 0
371  else if p = mdbPrev s_node
372  then m \<turnstile> p \<leadsto> slot \<and> p' = mdbNext s_node
373  else m \<turnstile> p \<leadsto> p'"
374  apply (clarsimp simp: mdb_next_unfold split del: if_split cong: if_cong)
375  apply (case_tac z)
376  apply (clarsimp split del: if_split)
377  apply (drule n_next)
378  apply (elim exE conjE)
379  apply (simp split: if_split_asm)
380  apply (frule dlist_prevD [OF m_slot_prev])
381  apply (clarsimp simp: mdb_next_unfold)
382  done
383
384lemma n_next_eq:
385  "n \<turnstile> p \<leadsto> p' =
386  (if p = slot then p' = 0
387  else if p = mdbPrev s_node
388  then m \<turnstile> p \<leadsto> slot \<and> p' = mdbNext s_node
389  else m \<turnstile> p \<leadsto> p')"
390  apply (rule iffI)
391   apply (erule n_nextD)
392  apply (clarsimp simp: mdb_next_unfold split: if_split_asm)
393    apply (simp add: n_def modify_map_if slot)
394   apply hypsubst_thin
395   apply (case_tac z)
396   apply simp
397   apply (drule m_next)
398   apply clarsimp
399  apply (case_tac z)
400  apply simp
401  apply (drule m_next)
402  apply clarsimp
403  done
404
405lemma n_prev_eq:
406  "n \<turnstile> p \<leftarrow> p' =
407  (if p' = slot then p = 0
408  else if p' = mdbNext s_node
409  then m \<turnstile> slot \<leftarrow> p' \<and> p = mdbPrev s_node
410  else m \<turnstile> p \<leftarrow> p')"
411  apply (rule iffI)
412   apply (clarsimp simp: mdb_prev_def split del: if_split cong: if_cong)
413   apply (case_tac z)
414   apply (clarsimp split del: if_split)
415   apply (drule n_prev)
416   apply (elim exE conjE)
417   apply (simp split: if_split_asm)
418   apply (frule dlist_nextD [OF m_slot_next])
419   apply (clarsimp simp: mdb_prev_def)
420  apply (clarsimp simp: mdb_prev_def split: if_split_asm)
421    apply (simp add: n_def modify_map_if slot)
422   apply hypsubst_thin
423   apply (case_tac z)
424   apply clarsimp
425   apply (drule m_prev)
426   apply clarsimp
427  apply (case_tac z)
428  apply simp
429  apply (drule m_prev)
430  apply clarsimp
431  done
432
433lemma valid_dlist_n:
434  "valid_dlist n" using dlist
435  apply (clarsimp simp: valid_dlist_def2 [OF no_0_n])
436  apply (simp add: n_next_eq n_prev_eq m_slot_next m_slot_prev cong: if_cong)
437  apply (rule conjI, clarsimp)
438   apply (rule conjI, clarsimp simp: next_slot_prev prev_slot_next)
439   apply (fastforce dest!: dlist_prev_src_unique)
440  apply clarsimp
441  apply (rule conjI, clarsimp)
442   apply (clarsimp simp: valid_dlist_def2 [OF no_0])
443   apply (case_tac "mdbNext s_node = 0")
444    apply simp
445    apply (subgoal_tac "m \<turnstile> slot \<leadsto> c'")
446     prefer 2
447     apply fastforce
448    apply (clarsimp simp: mdb_next_unfold slot)
449   apply (frule next_slot_prev)
450   apply (drule (1) dlist_prev_src_unique, simp)
451   apply simp
452  apply clarsimp
453  apply (rule conjI, clarsimp)
454   apply (fastforce dest: dlist_next_src_unique)
455  apply clarsimp
456  apply (rule conjI, clarsimp)
457   apply (clarsimp simp: valid_dlist_def2 [OF no_0])
458   apply (clarsimp simp: mdb_prev_def slot)
459  apply (clarsimp simp: valid_dlist_def2 [OF no_0])
460  done
461
462lemma caps_contained_n:
463  "caps_contained' n"
464  using valid
465  apply (clarsimp simp: valid_mdb_ctes_def caps_contained'_def)
466  apply (drule n_cap)+
467  apply (clarsimp split: if_split_asm)
468  apply (erule disjE, clarsimp)
469  apply clarsimp
470  apply fastforce
471  done
472
473lemma chunked:
474  "mdb_chunked m"
475  using valid by (simp add: valid_mdb_ctes_def)
476
477lemma valid_badges:
478  "valid_badges m"
479  using valid ..
480
481lemma valid_badges_n:
482  "valid_badges n"
483proof -
484  from valid_badges
485  show ?thesis
486    apply (simp add: valid_badges_def2)
487    apply clarsimp
488    apply (drule_tac p=p in n_cap)
489    apply (frule n_cap)
490    apply (drule n_badged)
491    apply (clarsimp simp: n_next_eq)
492    apply (case_tac "p=slot", simp)
493    apply clarsimp
494    apply (case_tac "p'=slot", simp)
495    apply clarsimp
496    apply (case_tac "p = mdbPrev s_node")
497     apply clarsimp
498     apply (insert slot)[1]
499     (* using mdb_chunked to show cap in between is same as on either side *)
500     apply (subgoal_tac "capMasterCap s_cap = capMasterCap cap'")
501      prefer 2
502      apply (thin_tac "\<forall>p. P p" for P)
503      apply (drule mdb_chunked2D[OF chunked])
504           apply (fastforce simp: mdb_next_unfold)
505          apply assumption+
506        apply (simp add: sameRegionAs_def3)
507        apply (intro disjI1)
508        apply (fastforce simp:isCap_simps capMasterCap_def split:capability.splits)
509       apply clarsimp
510      apply clarsimp
511      apply (erule sameRegionAsE, auto simp: isCap_simps capMasterCap_def split:capability.splits)[1]
512     (* instantiating known valid_badges on both sides to transitively
513        give the link we need *)
514     apply (frule_tac x="mdbPrev s_node" in spec)
515     apply simp
516     apply (drule spec, drule spec, drule spec,
517            drule(1) mp, drule(1) mp)
518     apply simp
519     apply (drule_tac x=slot in spec)
520     apply (drule_tac x="mdbNext s_node" in spec)
521     apply simp
522     apply (drule mp, simp(no_asm) add: mdb_next_unfold)
523      apply simp
524     apply (cases "capBadge s_cap", simp_all)[1]
525    apply clarsimp
526    apply (case_tac "p' = mdbNext s_node")
527     apply clarsimp
528     apply (frule vdlist_next_src_unique[where y=slot])
529        apply (simp add: mdb_next_unfold slot)
530       apply clarsimp
531      apply (rule dlist)
532     apply clarsimp
533    apply clarsimp
534    apply fastforce
535    done
536qed
537
538lemma p_not_slot:
539  assumes "n \<turnstile> p \<rightarrow> p'"
540  shows "p \<noteq> slot"
541  using assms
542  by induct (auto simp: mdb_next_unfold n_def modify_map_if)
543
544lemma to_slot_eq [simp]:
545  "m \<turnstile> p \<leadsto> slot = (p = mdbPrev s_node \<and> p \<noteq> 0)"
546  apply (rule iffI)
547   apply (frule dlist_nextD0, simp)
548   apply (clarsimp simp: mdb_prev_def slot mdb_next_unfold)
549  apply (clarsimp intro!: prev_slot_next)
550  done
551
552lemma n_parent_of:
553  "\<lbrakk> n \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot \<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf p'"
554  apply (clarsimp simp: parentOf_def)
555  apply (case_tac cte, case_tac cte')
556  apply clarsimp
557  apply (frule_tac p=p in n_cap)
558  apply (frule_tac p=p in n_badged)
559  apply (drule_tac p=p in n_revokable)
560  apply (clarsimp)
561  apply (frule_tac p=p' in n_cap)
562  apply (frule_tac p=p' in n_badged)
563  apply (drule_tac p=p' in n_revokable)
564  apply (clarsimp split: if_split_asm;
565         clarsimp simp: isMDBParentOf_def isCap_simps split: if_split_asm cong: if_cong)
566  done
567
568lemma m_parent_of:
569  "\<lbrakk> m \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot; p\<noteq>p'; p'\<noteq>mdbNext s_node \<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf p'"
570  apply (clarsimp simp add: parentOf_def)
571  apply (case_tac cte, case_tac cte')
572  apply clarsimp
573  apply (frule_tac p=p in m_cap)
574  apply (frule_tac p=p in m_badged)
575  apply (drule_tac p=p in m_revokable)
576  apply clarsimp
577  apply (frule_tac p=p' in m_cap)
578  apply (frule_tac p=p' in m_badged)
579  apply (drule_tac p=p' in m_revokable)
580  apply clarsimp
581  apply (simp split: if_split_asm;
582         clarsimp simp: isMDBParentOf_def isCap_simps split: if_split_asm cong: if_cong)
583  done
584
585lemma m_parent_of_next:
586  "\<lbrakk> m \<turnstile> p parentOf mdbNext s_node; m \<turnstile> p parentOf slot; p \<noteq> slot; p\<noteq>mdbNext s_node \<rbrakk>
587  \<Longrightarrow> n \<turnstile> p parentOf mdbNext s_node"
588  using slot
589  apply (clarsimp simp add: parentOf_def)
590  apply (case_tac cte'a, case_tac cte)
591  apply clarsimp
592  apply (frule_tac p=p in m_cap)
593  apply (frule_tac p=p in m_badged)
594  apply (drule_tac p=p in m_revokable)
595  apply (frule_tac p="mdbNext s_node" in m_cap)
596  apply (frule_tac p="mdbNext s_node" in m_badged)
597  apply (drule_tac p="mdbNext s_node" in m_revokable)
598  apply (frule_tac p="slot" in m_cap)
599  apply (frule_tac p="slot" in m_badged)
600  apply (drule_tac p="slot" in m_revokable)
601  apply (clarsimp simp: isMDBParentOf_def isCap_simps split: if_split_asm cong: if_cong)
602  done
603
604lemma parency_n:
605  assumes "n \<turnstile> p \<rightarrow> p'"
606  shows "m \<turnstile> p \<rightarrow> p' \<and> p \<noteq> slot \<and> p' \<noteq> slot"
607using assms
608proof induct
609  case (direct_parent c')
610  moreover
611  hence "p \<noteq> slot"
612    by (clarsimp simp: n_next_eq)
613  moreover
614  from direct_parent
615  have "c' \<noteq> slot"
616    by (clarsimp simp add: n_next_eq split: if_split_asm)
617  ultimately
618  show ?case
619    apply simp
620    apply (simp add: n_next_eq split: if_split_asm)
621     prefer 2
622     apply (erule (1) subtree.direct_parent)
623     apply (erule (2) n_parent_of)
624    apply clarsimp
625    apply (frule n_parent_of, simp, simp)
626    apply (rule subtree.trans_parent[OF _ m_slot_next], simp_all)
627    apply (rule subtree.direct_parent)
628      apply (erule prev_slot_next)
629     apply simp
630    apply (clarsimp simp: parentOf_def slot)
631    apply (case_tac cte'a)
632    apply (case_tac ctea)
633    apply clarsimp
634    apply (frule(2) mdb_chunked2D [OF chunked prev_slot_next m_slot_next])
635      apply (clarsimp simp: isMDBParentOf_CTE)
636     apply simp
637    apply (simp add: slot)
638    apply (clarsimp simp add: isMDBParentOf_CTE)
639    apply (insert valid_badges)
640    apply (simp add: valid_badges_def2)
641    apply (drule spec[where x=slot])
642    apply (drule spec[where x="mdbNext s_node"])
643    apply (simp add: slot m_slot_next)
644    apply (insert valid_badges)
645    apply (simp add: valid_badges_def2)
646    apply (drule spec[where x="mdbPrev s_node"])
647    apply (drule spec[where x=slot])
648    apply (simp add: slot prev_slot_next)
649    apply (case_tac cte, case_tac cte')
650    apply (rename_tac cap'' node'')
651    apply (clarsimp simp: isMDBParentOf_CTE)
652    apply (frule n_cap, drule n_badged)
653    apply (frule n_cap, drule n_badged)
654    apply clarsimp
655    apply (case_tac cap'', simp_all add: isCap_simps)[1]
656     apply (clarsimp simp: sameRegionAs_def3 isCap_simps)
657    apply (clarsimp simp: sameRegionAs_def3 isCap_simps)
658    done
659next
660  case (trans_parent c c')
661  moreover
662  hence "p \<noteq> slot"
663    by (clarsimp simp: n_next_eq)
664  moreover
665  from trans_parent
666  have "c' \<noteq> slot"
667    by (clarsimp simp add: n_next_eq split: if_split_asm)
668  ultimately
669  show ?case
670    apply clarsimp
671    apply (simp add: n_next_eq split: if_split_asm)
672     prefer 2
673     apply (erule (2) subtree.trans_parent)
674     apply (erule n_parent_of, simp, simp)
675    apply clarsimp
676    apply (rule subtree.trans_parent)
677       apply (rule subtree.trans_parent, assumption)
678         apply (rule prev_slot_next)
679         apply clarsimp
680        apply clarsimp
681       apply (frule n_parent_of, simp, simp)
682       apply (clarsimp simp: parentOf_def slot)
683       apply (case_tac cte'a)
684       apply (rename_tac cap node)
685       apply (case_tac ctea)
686       apply clarsimp
687       apply (subgoal_tac "sameRegionAs cap s_cap")
688        prefer 2
689        apply (insert chunked)[1]
690        apply (simp add: mdb_chunked_def)
691        apply (erule_tac x="p" in allE)
692        apply (erule_tac x="mdbNext s_node" in allE)
693        apply simp
694        apply (drule isMDBParent_sameRegion)+
695        apply clarsimp
696        apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ slot")
697         prefer 2
698         apply (rule trancl_trans)
699          apply (erule subtree_mdb_next)
700         apply (rule r_into_trancl)
701         apply (rule prev_slot_next)
702         apply clarsimp
703        apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node")
704         prefer 2
705         apply (erule trancl_trans)
706         apply fastforce
707        apply simp
708        apply (erule impE)
709         apply clarsimp
710        apply clarsimp
711        apply (thin_tac "s \<longrightarrow> t" for s t)
712        apply (simp add: is_chunk_def)
713        apply (erule_tac x=slot in allE)
714        apply (erule impE, fastforce)
715        apply (erule impE, fastforce)
716        apply (clarsimp simp: slot)
717       apply (clarsimp simp: isMDBParentOf_CTE)
718       apply (insert valid_badges, simp add: valid_badges_def2)
719       apply (drule spec[where x=slot], drule spec[where x="mdbNext s_node"])
720       apply (simp add: slot m_slot_next)
721       apply (case_tac cte, case_tac cte')
722       apply (rename_tac cap'' node'')
723       apply (clarsimp simp: isMDBParentOf_CTE)
724       apply (frule n_cap, drule n_badged)
725       apply (frule n_cap, drule n_badged)
726       apply (clarsimp split: if_split_asm)
727        apply (drule subtree_mdb_next)
728        apply (drule no_loops_tranclE[OF no_loops])
729        apply (erule notE, rule trancl_into_rtrancl)
730        apply (rule trancl.intros(2)[OF _ m_slot_next])
731        apply (rule trancl.intros(1), rule prev_slot_next)
732        apply simp
733       apply (case_tac cap'', simp_all add: isCap_simps)[1]
734        apply (clarsimp simp: sameRegionAs_def3 isCap_simps)
735       apply (clarsimp simp: sameRegionAs_def3 isCap_simps)
736      apply (rule m_slot_next)
737     apply simp
738    apply (erule n_parent_of, simp, simp)
739    done
740qed
741
742lemma parency_m:
743  assumes "m \<turnstile> p \<rightarrow> p'"
744  shows "p \<noteq> slot \<longrightarrow> (if p' \<noteq> slot then n \<turnstile> p \<rightarrow> p' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)"
745using assms
746proof induct
747  case (direct_parent c)
748  thus ?case
749    apply clarsimp
750    apply (rule conjI)
751     apply clarsimp
752     apply (rule subtree.direct_parent)
753       apply (simp add: n_next_eq)
754       apply clarsimp
755       apply (subgoal_tac "mdbPrev s_node \<noteq> 0")
756        prefer 2
757        apply (clarsimp simp: mdb_next_unfold)
758       apply (drule prev_slot_next)
759       apply (clarsimp simp: mdb_next_unfold)
760      apply assumption
761     apply (erule m_parent_of, simp, simp)
762      apply clarsimp
763     apply clarsimp
764     apply (drule dlist_next_src_unique)
765       apply fastforce
766      apply clarsimp
767     apply simp
768    apply clarsimp
769    apply (rule subtree.direct_parent)
770      apply (simp add: n_next_eq)
771     apply (drule subtree_parent)
772     apply (clarsimp simp: parentOf_def)
773    apply (drule subtree_parent)
774    apply (erule (1) m_parent_of_next)
775     apply clarsimp
776    apply clarsimp
777    done
778next
779  case (trans_parent c c')
780  thus ?case
781    apply clarsimp
782    apply (rule conjI)
783     apply clarsimp
784     apply (cases "c=slot")
785      apply simp
786      apply (erule impE)
787       apply (erule subtree.trans_parent)
788         apply fastforce
789        apply (clarsimp simp: slot mdb_next_unfold)
790       apply (clarsimp simp: slot mdb_next_unfold)
791      apply (clarsimp simp: slot mdb_next_unfold)
792     apply clarsimp
793     apply (erule subtree.trans_parent)
794       apply (simp add: n_next_eq)
795       apply clarsimp
796       apply (subgoal_tac "mdbPrev s_node \<noteq> 0")
797        prefer 2
798        apply (clarsimp simp: mdb_next_unfold)
799       apply (drule prev_slot_next)
800       apply (clarsimp simp: mdb_next_unfold)
801      apply assumption
802     apply (erule m_parent_of, simp, simp)
803      apply clarsimp
804      apply (drule subtree_mdb_next)
805      apply (drule trancl_trans)
806       apply (erule r_into_trancl)
807      apply simp
808     apply clarsimp
809     apply (drule dlist_next_src_unique)
810       apply fastforce
811      apply clarsimp
812     apply simp
813    apply clarsimp
814    apply (erule subtree.trans_parent)
815      apply (simp add: n_next_eq)
816     apply clarsimp
817    apply (rule m_parent_of_next, erule subtree_parent, assumption, assumption)
818    apply clarsimp
819    done
820qed
821
822lemma parency:
823  "n \<turnstile> p \<rightarrow> p' = (p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p')"
824  by (auto dest!: parency_n parency_m)
825
826lemma descendants:
827  "descendants_of' p n =
828  (if p = slot then {} else descendants_of' p m - {slot})"
829  by (auto simp add: parency descendants_of'_def)
830
831lemma n_tranclD:
832  "n \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> p' \<noteq> slot"
833  apply (erule trancl_induct)
834   apply (clarsimp simp add: n_next_eq split: if_split_asm)
835     apply (rule mdb_chain_0D)
836      apply (rule chain)
837     apply (clarsimp simp: slot)
838    apply (blast intro: trancl_trans prev_slot_next)
839   apply fastforce
840  apply (clarsimp simp: n_next_eq split: if_split_asm)
841   apply (erule trancl_trans)
842   apply (blast intro: trancl_trans prev_slot_next)
843  apply (fastforce intro: trancl_trans)
844  done
845
846lemma m_tranclD:
847  "m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow>
848  if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* p'
849  else if p' = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
850  else n \<turnstile> p \<leadsto>\<^sup>+ p'"
851  using no_0_n
852  apply -
853  apply (erule trancl_induct)
854   apply clarsimp
855   apply (rule conjI)
856    apply clarsimp
857    apply (rule r_into_trancl)
858    apply (clarsimp simp: n_next_eq)
859   apply clarsimp
860   apply (rule conjI)
861    apply (insert m_slot_next)[1]
862    apply (clarsimp simp: mdb_next_unfold)
863   apply clarsimp
864   apply (rule r_into_trancl)
865   apply (clarsimp simp: n_next_eq)
866   apply (rule context_conjI)
867    apply (clarsimp simp: mdb_next_unfold)
868   apply (drule prev_slot_next)
869   apply (clarsimp simp: mdb_next_unfold)
870  apply clarsimp
871  apply (rule conjI)
872   apply clarsimp
873   apply (rule conjI)
874    apply clarsimp
875    apply (drule prev_slot_next)
876    apply (drule trancl_trans, erule r_into_trancl)
877    apply simp
878   apply clarsimp
879   apply (erule trancl_trans)
880   apply (rule r_into_trancl)
881   apply (simp add: n_next_eq)
882  apply clarsimp
883  apply (rule conjI)
884   apply clarsimp
885   apply (erule rtrancl_trans)
886   apply (rule r_into_rtrancl)
887   apply (simp add: n_next_eq)
888   apply (rule conjI)
889    apply clarsimp
890    apply (rule context_conjI)
891     apply (clarsimp simp: mdb_next_unfold)
892    apply (drule prev_slot_next)
893    apply (clarsimp simp: mdb_next_unfold)
894   apply clarsimp
895  apply clarsimp
896  apply (simp split: if_split_asm)
897   apply (clarsimp simp: mdb_next_unfold slot)
898  apply (erule trancl_trans)
899  apply (rule r_into_trancl)
900  apply (clarsimp simp add: n_next_eq)
901  apply (rule context_conjI)
902   apply (clarsimp simp: mdb_next_unfold)
903  apply (drule prev_slot_next)
904  apply (clarsimp simp: mdb_next_unfold)
905  done
906
907lemma n_trancl_eq:
908  "n \<turnstile> p \<leadsto>\<^sup>+ p' = (m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot)"
909  using no_0_n
910  apply -
911  apply (rule iffI)
912   apply (frule n_tranclD)
913   apply clarsimp
914   apply (drule tranclD)
915   apply (clarsimp simp: n_next_eq)
916   apply (simp add: rtrancl_eq_or_trancl)
917  apply clarsimp
918  apply (drule m_tranclD)
919  apply (simp split: if_split_asm)
920  apply (rule r_into_trancl)
921  apply (simp add: n_next_eq)
922  done
923
924lemma n_rtrancl_eq:
925  "n \<turnstile> p \<leadsto>\<^sup>* p' =
926  (m \<turnstile> p \<leadsto>\<^sup>* p' \<and>
927   (p = slot \<longrightarrow> p' = 0 \<or> p' = slot) \<and>
928   (p' = slot \<longrightarrow> p = slot))"
929  by (auto simp: rtrancl_eq_or_trancl n_trancl_eq)
930
931lemma mdb_chain_0_n:
932  "mdb_chain_0 n"
933  using chain
934  apply (clarsimp simp: mdb_chain_0_def)
935  apply (drule bspec)
936   apply (fastforce simp: n_def modify_map_if split: if_split_asm)
937  apply (simp add: n_trancl_eq)
938  done
939
940lemma mdb_chunked_n:
941  "mdb_chunked n"
942  using chunked
943  apply (clarsimp simp: mdb_chunked_def)
944  apply (drule n_cap)+
945  apply (clarsimp split: if_split_asm)
946  apply (case_tac "p=slot", clarsimp)
947  apply clarsimp
948  apply (erule_tac x=p in allE)
949  apply (erule_tac x=p' in allE)
950  apply (clarsimp simp: is_chunk_def)
951  apply (simp add: n_trancl_eq n_rtrancl_eq)
952  apply (rule conjI)
953   apply clarsimp
954   apply (erule_tac x=p'' in allE)
955   apply clarsimp
956   apply (drule_tac p=p'' in m_cap)
957   apply clarsimp
958  apply clarsimp
959  apply (erule_tac x=p'' in allE)
960  apply clarsimp
961  apply (drule_tac p=p'' in m_cap)
962  apply clarsimp
963  done
964
965lemma untyped_mdb_n:
966  "untyped_mdb' n"
967  using untyped_mdb
968  apply (simp add: untyped_mdb'_def descendants_of'_def parency)
969  apply clarsimp
970  apply (drule n_cap)+
971  apply (clarsimp split: if_split_asm)
972  apply (case_tac "p=slot", simp)
973  apply clarsimp
974  done
975
976lemma untyped_inc_n:
977  "untyped_inc' n"
978  using untyped_inc
979  apply (simp add: untyped_inc'_def descendants_of'_def parency)
980  apply clarsimp
981  apply (drule n_cap)+
982  apply (clarsimp split: if_split_asm)
983  apply (case_tac "p=slot", simp)
984  apply clarsimp
985  apply (erule_tac x=p in allE)
986  apply (erule_tac x=p' in allE)
987  apply simp
988  done
989
990lemmas vn_prev [dest!] = valid_nullcaps_prev [OF _ slot no_0 dlist nullcaps]
991lemmas vn_next [dest!] = valid_nullcaps_next [OF _ slot no_0 dlist nullcaps]
992
993lemma nullcaps_n: "valid_nullcaps n"
994proof -
995  from valid have "valid_nullcaps m" ..
996  thus ?thesis
997    apply (clarsimp simp: valid_nullcaps_def nullMDBNode_def nullPointer_def)
998    apply (frule n_cap)
999    apply (frule n_next)
1000    apply (frule n_badged)
1001    apply (frule n_revokable)
1002    apply (drule n_prev)
1003    apply (case_tac n)
1004    apply (insert slot)
1005    apply (fastforce split: if_split_asm)
1006    done
1007qed
1008
1009lemma ut_rev_n: "ut_revocable' n"
1010  apply(insert valid)
1011  apply(clarsimp simp: ut_revocable'_def)
1012  apply(frule n_cap)
1013  apply(drule n_revokable)
1014  apply(clarsimp simp: isCap_simps split: if_split_asm)
1015  apply(simp add: valid_mdb_ctes_def ut_revocable'_def)
1016  done
1017
1018lemma class_links_n: "class_links n"
1019  using valid slot
1020  apply (clarsimp simp: valid_mdb_ctes_def class_links_def)
1021  apply (case_tac cte, case_tac cte')
1022  apply (drule n_nextD)
1023  apply (clarsimp simp: split: if_split_asm)
1024    apply (simp add: no_0_n)
1025   apply (drule n_cap)+
1026   apply clarsimp
1027   apply (frule spec[where x=slot],
1028          drule spec[where x="mdbNext s_node"],
1029          simp, simp add: m_slot_next)
1030   apply (drule spec[where x="mdbPrev s_node"],
1031          drule spec[where x=slot], simp)
1032  apply (drule n_cap)+
1033  apply clarsimp
1034  apply (fastforce split: if_split_asm)
1035  done
1036
1037lemma distinct_zombies_m: "distinct_zombies m"
1038  using valid by (simp add: valid_mdb_ctes_def)
1039
1040lemma distinct_zombies_n[simp]:
1041  "distinct_zombies n"
1042  using distinct_zombies_m
1043  apply (simp add: n_def distinct_zombies_nonCTE_modify_map)
1044  apply (subst modify_map_apply[where p=slot])
1045   apply (simp add: modify_map_def slot)
1046  apply simp
1047  apply (rule distinct_zombies_sameMasterE)
1048    apply (simp add: distinct_zombies_nonCTE_modify_map)
1049   apply (simp add: modify_map_def slot)
1050  apply simp
1051  done
1052
1053lemma irq_control_n [simp]: "irq_control n"
1054  using slot
1055  apply (clarsimp simp: irq_control_def)
1056  apply (frule n_revokable)
1057  apply (drule n_cap)
1058  apply (clarsimp split: if_split_asm)
1059  apply (frule irq_revocable, rule irq_control)
1060  apply clarsimp
1061  apply (drule n_cap)
1062  apply (clarsimp simp: if_split_asm)
1063  apply (erule (1) irq_controlD, rule irq_control)
1064  done
1065
1066lemma reply_masters_rvk_fb_m: "reply_masters_rvk_fb m"
1067  using valid by auto
1068
1069lemma reply_masters_rvk_fb_n [simp]: "reply_masters_rvk_fb n"
1070  using reply_masters_rvk_fb_m
1071  apply (simp add: reply_masters_rvk_fb_def n_def
1072                   ball_ran_modify_map_eq
1073                   modify_map_comp[symmetric])
1074  apply (subst ball_ran_modify_map_eq)
1075   apply (frule bspec, rule ranI, rule slot)
1076   apply (simp add: nullMDBNode_def isCap_simps modify_map_def
1077                    slot)
1078  apply (subst ball_ran_modify_map_eq)
1079   apply (clarsimp simp add: modify_map_def)
1080   apply fastforce
1081  apply (simp add: ball_ran_modify_map_eq)
1082  done
1083
1084lemma vmdb_n: "valid_mdb_ctes n"
1085  by (simp add: valid_mdb_ctes_def valid_dlist_n
1086                no_0_n mdb_chain_0_n valid_badges_n
1087                caps_contained_n mdb_chunked_n
1088                untyped_mdb_n untyped_inc_n
1089                nullcaps_n ut_rev_n class_links_n)
1090
1091end
1092
1093context begin interpretation Arch .
1094crunch ctes_of[wp]: postCapDeletion, clearUntypedFreeIndex "\<lambda>s. P (ctes_of s)"
1095
1096lemma emptySlot_mdb [wp]:
1097  "\<lbrace>valid_mdb'\<rbrace>
1098  emptySlot sl opt
1099  \<lbrace>\<lambda>_. valid_mdb'\<rbrace>"
1100  unfolding emptySlot_def
1101  apply (simp only: case_Null_If valid_mdb'_def)
1102  apply (wp updateCap_ctes_of_wp getCTE_wp'
1103            opt_return_pres_lift | simp add: cte_wp_at_ctes_of)+
1104  apply (clarsimp)
1105  apply (case_tac cte)
1106  apply (rename_tac cap node)
1107  apply (simp)
1108  apply (subgoal_tac "mdb_empty (ctes_of s) sl cap node")
1109   prefer 2
1110   apply (rule mdb_empty.intro)
1111   apply (rule mdb_ptr.intro)
1112    apply (rule vmdb.intro)
1113    apply (simp add: valid_mdb_ctes_def)
1114   apply (rule mdb_ptr_axioms.intro)
1115   apply (simp add: cte_wp_at_ctes_of)
1116  apply (rule conjI, clarsimp simp: valid_mdb_ctes_def)
1117  apply (erule mdb_empty.vmdb_n[unfolded const_def])
1118  done
1119end
1120
1121lemma if_live_then_nonz_cap'_def2:
1122  "if_live_then_nonz_cap' = (\<lambda>s. \<forall>ptr. ko_wp_at' live' ptr s
1123                               \<longrightarrow> (\<exists>p zr. (option_map zobj_refs' o cteCaps_of s) p = Some zr \<and> ptr \<in> zr))"
1124  by (fastforce intro!: ext
1125                 simp: if_live_then_nonz_cap'_def ex_nonz_cap_to'_def
1126                       cte_wp_at_ctes_of cteCaps_of_def)
1127
1128lemma updateMDB_ko_wp_at_live[wp]:
1129  "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace>
1130      updateMDB p m
1131   \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>"
1132  unfolding updateMDB_def Let_def
1133  apply (rule hoare_pre, wp)
1134  apply simp
1135  done
1136
1137lemma updateCap_ko_wp_at_live[wp]:
1138  "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace>
1139      updateCap p cap
1140   \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>"
1141  unfolding updateCap_def
1142  by wp
1143
1144primrec
1145  threadCapRefs :: "capability \<Rightarrow> word32 set"
1146where
1147  "threadCapRefs (ThreadCap r)                  = {r}"
1148| "threadCapRefs (ReplyCap t m)                 = {}"
1149| "threadCapRefs NullCap                        = {}"
1150| "threadCapRefs (UntypedCap d r n i)             = {}"
1151| "threadCapRefs (EndpointCap r badge x y z)    = {}"
1152| "threadCapRefs (NotificationCap r badge x y) = {}"
1153| "threadCapRefs (CNodeCap r b g gsz)           = {}"
1154| "threadCapRefs (Zombie r b n)                 = {}"
1155| "threadCapRefs (ArchObjectCap ac)             = {}"
1156| "threadCapRefs (IRQHandlerCap irq)            = {}"
1157| "threadCapRefs (IRQControlCap)                = {}"
1158| "threadCapRefs (DomainCap)                    = {}"
1159
1160lemma threadCapRefs_def2:
1161  "threadCapRefs cap = (case cap of ThreadCap r \<Rightarrow> {r} | _ \<Rightarrow> {})"
1162  by (simp split: capability.split)
1163
1164definition
1165  "isFinal cap p m \<equiv>
1166  \<not>isUntypedCap cap \<and>
1167  (\<forall>p' c. m p' = Some c \<longrightarrow>
1168          p \<noteq> p' \<longrightarrow> \<not>isUntypedCap c \<longrightarrow>
1169          \<not> sameObjectAs cap c)"
1170
1171lemma not_FinalE:
1172  "\<lbrakk> \<not> isFinal cap sl cps; isUntypedCap cap \<Longrightarrow> P;
1173     \<And>p c. \<lbrakk> cps p = Some c; p \<noteq> sl; \<not> isUntypedCap c; sameObjectAs cap c \<rbrakk> \<Longrightarrow> P
1174    \<rbrakk> \<Longrightarrow> P"
1175  by (fastforce simp: isFinal_def)
1176
1177definition
1178 "removeable' sl \<equiv> \<lambda>s cap.
1179    (\<exists>p. p \<noteq> sl \<and> cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capMasterCap cap) p s)
1180    \<or> ((\<forall>p \<in> cte_refs' cap (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) p s)
1181         \<and> (\<forall>p \<in> zobj_refs' cap. ko_wp_at' (Not \<circ> live') p s)
1182         \<and> (\<forall>t \<in> threadCapRefs cap. \<forall>p. t \<notin> set (ksReadyQueues s p)))"
1183
1184lemma not_Final_removeable:
1185  "\<not> isFinal cap sl (cteCaps_of s)
1186    \<Longrightarrow> removeable' sl s cap"
1187  apply (erule not_FinalE)
1188   apply (clarsimp simp: removeable'_def isCap_simps)
1189  apply (clarsimp simp: cteCaps_of_def sameObjectAs_def2 removeable'_def
1190                        cte_wp_at_ctes_of)
1191  apply fastforce
1192  done
1193
1194context begin interpretation Arch .
1195crunch ko_wp_at'[wp]: postCapDeletion "\<lambda>s. P (ko_wp_at' P' p s)"
1196crunch cteCaps_of[wp]: postCapDeletion "\<lambda>s. P (cteCaps_of s)"
1197  (simp: cteCaps_of_def o_def)
1198end
1199
1200crunch ko_at_live[wp]: clearUntypedFreeIndex "\<lambda>s. P (ko_wp_at' live' ptr s)"
1201
1202lemma clearUntypedFreeIndex_cteCaps_of[wp]:
1203  "\<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace>
1204       clearUntypedFreeIndex sl \<lbrace>\<lambda>y s. P (cteCaps_of s)\<rbrace>"
1205  by (simp add: cteCaps_of_def, wp)
1206
1207lemma emptySlot_iflive'[wp]:
1208  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace>
1209     emptySlot sl opt
1210   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
1211  apply (simp add: emptySlot_def case_Null_If if_live_then_nonz_cap'_def2
1212              del: comp_apply)
1213  apply (rule hoare_pre)
1214   apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
1215             getCTE_wp opt_return_pres_lift
1216             clearUntypedFreeIndex_ctes_of
1217             clearUntypedFreeIndex_cteCaps_of
1218             hoare_vcg_ex_lift
1219             | wp_once hoare_vcg_imp_lift
1220             | simp add: cte_wp_at_ctes_of del: comp_apply)+
1221  apply (clarsimp simp: modify_map_same
1222    imp_conjR[symmetric])
1223  apply (drule spec, drule(1) mp)
1224  apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def split: if_split_asm)
1225  apply (case_tac "p \<noteq> sl")
1226   apply blast
1227  apply (simp add: removeable'_def cteCaps_of_def)
1228  apply (erule disjE)
1229   apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def
1230                  dest!: capMaster_same_refs)
1231   apply fastforce
1232  apply clarsimp
1233  apply (drule(1) bspec)
1234  apply (clarsimp simp: ko_wp_at'_def)
1235  done
1236
1237crunch irq_node'[wp]: doMachineOp "\<lambda>s. P (irq_node' s)"
1238
1239lemma setIRQState_irq_node'[wp]:
1240  "\<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setIRQState state irq \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace>"
1241  apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def)
1242  apply wp
1243  apply simp
1244  done
1245
1246context begin interpretation Arch .
1247crunch irq_node'[wp]: emptySlot "\<lambda>s. P (irq_node' s)"
1248end
1249
1250lemma emptySlot_ifunsafe'[wp]:
1251  "\<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace>
1252     emptySlot sl opt
1253   \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>"
1254  apply (simp add: ifunsafe'_def3)
1255  apply (rule hoare_pre, rule hoare_use_eq_irq_node'[OF emptySlot_irq_node'])
1256   apply (simp add: emptySlot_def case_Null_If)
1257   apply (wp opt_return_pres_lift | simp add: o_def)+
1258   apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of)+
1259  apply (clarsimp simp: tree_cte_cteCap_eq[unfolded o_def]
1260                        modify_map_same
1261                        modify_map_comp[symmetric]
1262                 split: option.split_asm if_split_asm
1263                 dest!: modify_map_K_D)
1264  apply (clarsimp simp: modify_map_def)
1265  apply (drule_tac x=cref in spec, clarsimp)
1266  apply (case_tac "cref' \<noteq> sl")
1267   apply (rule_tac x=cref' in exI)
1268   apply (clarsimp simp: modify_map_def)
1269  apply (simp add: removeable'_def)
1270  apply (erule disjE)
1271   apply (clarsimp simp: modify_map_def)
1272   apply (subst(asm) tree_cte_cteCap_eq[unfolded o_def])
1273   apply (clarsimp split: option.split_asm dest!: capMaster_same_refs)
1274   apply fastforce
1275  apply clarsimp
1276  apply (drule(1) bspec)
1277  apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def)
1278  done
1279
1280lemma ex_nonz_cap_to'_def2:
1281  "ex_nonz_cap_to' p = (\<lambda>s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> zobj_refs' c)"
1282  by (fastforce simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of cteCaps_of_def
1283             intro!: ext)
1284
1285lemma ctes_of_valid'[elim]:
1286  "\<lbrakk>ctes_of s p = Some cte; valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' cteCap cte"
1287  by (cases cte, simp) (rule ctes_of_valid_cap')
1288
1289crunch ksrq[wp]: postCapDeletion "\<lambda>s. P (ksReadyQueues s)"
1290
1291crunch valid_idle'[wp]: setInterruptState "valid_idle'"
1292  (simp: valid_idle'_def)
1293
1294context begin interpretation Arch .
1295crunch valid_idle'[wp]: emptySlot "valid_idle'"
1296
1297crunch ksArch[wp]: emptySlot "\<lambda>s. P (ksArchState s)"
1298crunch ksIdle[wp]: emptySlot "\<lambda>s. P (ksIdleThread s)"
1299crunch gsMaxObjectSize[wp]: emptySlot "\<lambda>s. P (gsMaxObjectSize s)"
1300end
1301
1302lemma emptySlot_cteCaps_of:
1303  "\<lbrace>\<lambda>s. P (cteCaps_of s(p \<mapsto> NullCap))\<rbrace>
1304     emptySlot p opt
1305   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>"
1306  apply (simp add: emptySlot_def case_Null_If)
1307  apply (wp opt_return_pres_lift getCTE_cteCap_wp
1308            clearUntypedFreeIndex_cteCaps_of)
1309  apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of)
1310  apply (auto elim!: rsubst[where P=P]
1311               simp: modify_map_def fun_upd_def[symmetric] o_def
1312                     fun_upd_idem cteCaps_of_def
1313              split: option.splits)
1314  done
1315
1316lemma emptySlot_valid_global_refs[wp]:
1317  "\<lbrace>valid_global_refs' and cte_at' sl\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>"
1318  apply (simp add: valid_global_refs'_def global_refs'_def)
1319  apply (rule hoare_pre)
1320   apply (rule hoare_use_eq_irq_node' [OF emptySlot_irq_node'])
1321   apply (rule hoare_use_eq [where f=ksArchState, OF emptySlot_ksArch])
1322   apply (rule hoare_use_eq [where f=ksIdleThread, OF emptySlot_ksIdle])
1323   apply (rule hoare_use_eq [where f=gsMaxObjectSize], wp)
1324   apply (simp add: valid_refs'_cteCaps valid_cap_sizes_cteCaps)
1325   apply (rule emptySlot_cteCaps_of)
1326  apply (clarsimp simp: cte_wp_at_ctes_of)
1327  apply (frule(1) cte_at_valid_cap_sizes_0)
1328  apply (clarsimp simp: valid_refs'_cteCaps valid_cap_sizes_cteCaps ball_ran_eq)
1329  done
1330
1331lemmas doMachineOp_irq_handlers[wp]
1332    = valid_irq_handlers_lift'' [OF doMachineOp_ctes doMachineOp_ksInterruptState]
1333
1334lemma deletedIRQHandler_irq_handlers'[wp]:
1335  "\<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (IRQHandlerCap irq \<notin> ran (cteCaps_of s))\<rbrace>
1336       deletedIRQHandler irq
1337   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>"
1338  apply (simp add: deletedIRQHandler_def setIRQState_def setInterruptState_def getInterruptState_def)
1339  apply wp
1340  apply (clarsimp simp: valid_irq_handlers'_def irq_issued'_def ran_def cteCaps_of_def)
1341  done
1342
1343context begin interpretation Arch .
1344
1345lemma postCapDeletion_irq_handlers'[wp]:
1346  "\<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (cap \<noteq> NullCap \<longrightarrow> cap \<notin> ran (cteCaps_of s))\<rbrace>
1347       postCapDeletion cap
1348   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>"
1349  by (wpsimp simp: Retype_H.postCapDeletion_def ARM_H.postCapDeletion_def)
1350
1351end
1352
1353crunch ksInterruptState[wp]: clearUntypedFreeIndex "\<lambda>s. P (ksInterruptState s)"
1354
1355lemma emptySlot_valid_irq_handlers'[wp]:
1356  "\<lbrace>\<lambda>s. valid_irq_handlers' s
1357          \<and> (\<forall>sl'. info \<noteq> NullCap \<longrightarrow> sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)\<rbrace>
1358     emptySlot sl info
1359   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>"
1360  apply (simp add: emptySlot_def case_Null_If)
1361  apply (wp | wpc)+
1362        apply (unfold valid_irq_handlers'_def irq_issued'_def)
1363        apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of
1364          | wps clearUntypedFreeIndex_ksInterruptState)+
1365  apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of ran_def modify_map_def
1366                 split: option.split)
1367  apply auto
1368  done
1369
1370declare setIRQState_irq_states' [wp]
1371
1372context begin interpretation Arch .
1373crunch irq_states' [wp]: emptySlot valid_irq_states'
1374
1375crunch no_0_obj' [wp]: emptySlot no_0_obj'
1376 (wp: crunch_wps)
1377
1378crunch valid_queues'[wp]: setInterruptState "valid_queues'"
1379  (simp: valid_queues'_def)
1380
1381crunch valid_queues'[wp]: emptySlot "valid_queues'"
1382
1383crunch pde_mappings'[wp]: emptySlot "valid_pde_mappings'"
1384end
1385
1386lemma deletedIRQHandler_irqs_masked'[wp]:
1387  "\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>"
1388  apply (simp add: deletedIRQHandler_def setIRQState_def getInterruptState_def setInterruptState_def)
1389  apply (wp dmo_maskInterrupt)
1390  apply (simp add: irqs_masked'_def)
1391  done
1392
1393context begin interpretation Arch . (*FIXME: arch_split*)
1394crunch irqs_masked'[wp]: emptySlot "irqs_masked'"
1395
1396lemma setIRQState_umm:
1397 "\<lbrace>\<lambda>s. P (underlying_memory (ksMachineState s))\<rbrace>
1398   setIRQState irqState irq
1399  \<lbrace>\<lambda>_ s. P (underlying_memory (ksMachineState s))\<rbrace>"
1400  by (simp add: setIRQState_def maskInterrupt_def
1401                setInterruptState_def getInterruptState_def
1402      | wp dmo_lift')+
1403
1404crunch umm[wp]: emptySlot "\<lambda>s. P (underlying_memory (ksMachineState s))"
1405  (wp: setIRQState_umm)
1406
1407lemma emptySlot_vms'[wp]:
1408  "\<lbrace>valid_machine_state'\<rbrace> emptySlot slot irq \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>"
1409  by (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def)
1410     (wp hoare_vcg_all_lift hoare_vcg_disj_lift)
1411
1412crunch pspace_domain_valid[wp]: emptySlot "pspace_domain_valid"
1413
1414lemma ct_not_inQ_ksInterruptState_update[simp]:
1415  "ct_not_inQ (s\<lparr>ksInterruptState := v\<rparr>) = ct_not_inQ s"
1416  by (simp add: ct_not_inQ_def)
1417
1418crunch nosch[wp]: emptySlot "\<lambda>s. P (ksSchedulerAction s)"
1419crunch ct[wp]: emptySlot "\<lambda>s. P (ksCurThread s)"
1420crunch ksCurDomain[wp]: emptySlot "\<lambda>s. P (ksCurDomain s)"
1421crunch ksDomSchedule[wp]: emptySlot "\<lambda>s. P (ksDomSchedule s)"
1422crunch ksDomScheduleIdx[wp]: emptySlot "\<lambda>s. P (ksDomScheduleIdx s)"
1423
1424lemma deletedIRQHandler_ct_not_inQ[wp]:
1425  "\<lbrace>ct_not_inQ\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
1426  apply (rule ct_not_inQ_lift [OF deletedIRQHandler_nosch])
1427  apply (rule hoare_weaken_pre)
1428   apply (wps deletedIRQHandler_ct)
1429   apply (simp add: deletedIRQHandler_def setIRQState_def)
1430   apply (wp)
1431  apply (simp add: comp_def)
1432  done
1433
1434crunch ct_not_inQ[wp]: emptySlot "ct_not_inQ"
1435
1436crunch tcbDomain[wp]: emptySlot "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t"
1437
1438lemma emptySlot_ct_idle_or_in_cur_domain'[wp]:
1439  "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> emptySlot sl opt \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>"
1440apply (wp ct_idle_or_in_cur_domain'_lift2 tcb_in_cur_domain'_lift | simp)+
1441done
1442
1443crunch gsUntypedZeroRanges[wp]: postCapDeletion "\<lambda>s. P (gsUntypedZeroRanges s)"
1444  (wp: crunch_wps simp: crunch_simps)
1445
1446lemma untypedZeroRange_modify_map_isUntypedCap:
1447  "m sl = Some v \<Longrightarrow> \<not> isUntypedCap v \<Longrightarrow> \<not> isUntypedCap (f v)
1448    \<Longrightarrow> (untypedZeroRange \<circ>\<^sub>m modify_map m sl f) = (untypedZeroRange \<circ>\<^sub>m m)"
1449  by (simp add: modify_map_def map_comp_def fun_eq_iff untypedZeroRange_def)
1450
1451lemma emptySlot_untyped_ranges[wp]:
1452  "\<lbrace>untyped_ranges_zero' and valid_objs' and valid_mdb'\<rbrace>
1453     emptySlot sl opt \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>"
1454  apply (simp add: emptySlot_def case_Null_If)
1455  apply (rule hoare_pre)
1456   apply (rule hoare_seq_ext)
1457    apply (rule untyped_ranges_zero_lift)
1458     apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of
1459       | wpc | simp add: clearUntypedFreeIndex_def updateTrackedFreeIndex_def
1460                         getSlotCap_def
1461                  split: option.split)+
1462  apply (clarsimp simp: modify_map_comp[symmetric] modify_map_same)
1463  apply (case_tac "\<not> isUntypedCap (the (cteCaps_of s sl))")
1464   apply (case_tac "the (cteCaps_of s sl)",
1465     simp_all add: untyped_ranges_zero_inv_def
1466                   untypedZeroRange_modify_map_isUntypedCap isCap_simps)[1]
1467  apply (clarsimp simp: isCap_simps untypedZeroRange_def modify_map_def)
1468  apply (strengthen untyped_ranges_zero_fun_upd[mk_strg I E])
1469  apply simp
1470  apply (simp add: untypedZeroRange_def isCap_simps)
1471  done
1472
1473lemma emptySlot_invs'[wp]:
1474  "\<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s
1475            \<and> (\<forall>sl'. info \<noteq> NullCap \<longrightarrow> sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)\<rbrace>
1476     emptySlot sl info
1477   \<lbrace>\<lambda>rv. invs'\<rbrace>"
1478  apply (simp add: invs'_def valid_state'_def valid_pspace'_def)
1479  apply (rule hoare_pre)
1480   apply (wp valid_arch_state_lift' valid_irq_node_lift cur_tcb_lift)
1481  apply (clarsimp simp: cte_wp_at_ctes_of)
1482  done
1483
1484lemma deleted_irq_corres:
1485  "corres dc \<top> \<top>
1486    (deleted_irq_handler irq)
1487    (deletedIRQHandler irq)"
1488  apply (simp add: deleted_irq_handler_def deletedIRQHandler_def)
1489  apply (rule set_irq_state_corres)
1490  apply (simp add: irq_state_relation_def)
1491  done
1492
1493lemma arch_post_cap_deletion_corres:
1494  "acap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (arch_post_cap_deletion cap) (ARM_H.postCapDeletion cap')"
1495  by (corressimp simp: arch_post_cap_deletion_def ARM_H.postCapDeletion_def)
1496
1497lemma post_cap_deletion_corres:
1498  "cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')"
1499  apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def)
1500   apply (corressimp corres: deleted_irq_corres)
1501  by (corressimp corres: arch_post_cap_deletion_corres)
1502
1503lemma exec_update_cdt_list:
1504  "\<lbrakk>\<exists>x\<in>fst (g r (s\<lparr>cdt_list := (f (cdt_list s))\<rparr>)). P x\<rbrakk>
1505\<Longrightarrow> \<exists>x\<in>fst (((update_cdt_list f) >>= g) (s::det_state)). P x"
1506  apply (clarsimp simp: update_cdt_list_def set_cdt_list_def exec_gets exec_get put_def bind_assoc)
1507  apply (clarsimp simp: bind_def)
1508  apply (erule bexI)
1509  apply simp
1510  done
1511
1512lemma set_cap_trans_state:
1513  "((),s') \<in> fst (set_cap c p s) \<Longrightarrow> ((),trans_state f s') \<in> fst (set_cap c p (trans_state f s))"
1514  apply (cases p)
1515  apply (clarsimp simp add: set_cap_def in_monad get_object_def)
1516  apply (case_tac y)
1517  apply (auto simp add: in_monad set_object_def split: if_split_asm)
1518  done
1519
1520lemma clearUntypedFreeIndex_corres_noop:
1521  "corres dc \<top> (cte_at' (cte_map slot))
1522    (return ()) (clearUntypedFreeIndex (cte_map slot))"
1523  apply (simp add: clearUntypedFreeIndex_def)
1524  apply (rule corres_guard_imp)
1525    apply (rule corres_bind_return2)
1526    apply (rule corres_symb_exec_r_conj[where P'="cte_at' (cte_map slot)"])
1527       apply (rule corres_trivial, simp)
1528      apply (wp getCTE_wp' | wpc
1529        | simp add: updateTrackedFreeIndex_def getSlotCap_def)+
1530     apply (clarsimp simp: state_relation_def)
1531    apply (rule no_fail_pre)
1532     apply (wp no_fail_getSlotCap getCTE_wp'
1533       | wpc | simp add: updateTrackedFreeIndex_def getSlotCap_def)+
1534  done
1535
1536lemma clearUntypedFreeIndex_valid_pspace'[wp]:
1537  "\<lbrace>valid_pspace'\<rbrace> clearUntypedFreeIndex slot \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
1538  apply (simp add: valid_pspace'_def)
1539  apply (rule hoare_pre)
1540   apply (wp | simp add: valid_mdb'_def)+
1541  done
1542
1543lemma empty_slot_corres:
1544  "cap_relation info info' \<Longrightarrow> corres dc (einvs and cte_at slot) (invs' and cte_at' (cte_map slot))
1545             (empty_slot slot info) (emptySlot (cte_map slot) info')"
1546  unfolding emptySlot_def empty_slot_def
1547  apply (simp add: case_Null_If)
1548  apply (rule corres_guard_imp)
1549    apply (rule corres_split_noop_rhs[OF _ clearUntypedFreeIndex_corres_noop])
1550     apply (rule_tac R="\<lambda>cap. einvs and cte_wp_at ((=) cap) slot" and
1551                     R'="\<lambda>cte. valid_pspace' and cte_wp_at' ((=) cte) (cte_map slot)" in
1552                     corres_split [OF _ get_cap_corres])
1553       defer
1554       apply (wp get_cap_wp getCTE_wp')+
1555     apply (simp add: cte_wp_at_ctes_of)
1556     apply (wp hoare_vcg_imp_lift clearUntypedFreeIndex_valid_pspace')
1557    apply fastforce
1558   apply (fastforce simp: cte_wp_at_ctes_of)
1559  apply simp
1560  apply (rule conjI, clarsimp)
1561   defer
1562  apply clarsimp
1563  apply (rule conjI, clarsimp)
1564  apply clarsimp
1565  apply (simp only: bind_assoc[symmetric])
1566  apply (rule corres_split'[where r'=dc, OF _ post_cap_deletion_corres])
1567    defer
1568    apply wpsimp+
1569  apply (rule corres_no_failI)
1570   apply (rule no_fail_pre, wp static_imp_wp)
1571   apply (clarsimp simp: cte_wp_at_ctes_of valid_pspace'_def)
1572   apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def)
1573   apply (rule conjI, clarsimp)
1574    apply (erule (2) valid_dlistEp)
1575    apply simp
1576   apply clarsimp
1577   apply (erule (2) valid_dlistEn)
1578   apply simp
1579  apply (clarsimp simp: in_monad bind_assoc exec_gets)
1580  apply (subgoal_tac "mdb_empty_abs a")
1581   prefer 2
1582   apply (rule mdb_empty_abs.intro)
1583   apply (rule vmdb_abs.intro)
1584   apply fastforce
1585  apply (frule mdb_empty_abs'.intro)
1586  apply (simp add: mdb_empty_abs'.empty_slot_ext_det_def2 update_cdt_list_def set_cdt_list_def exec_gets set_cdt_def bind_assoc exec_get exec_put set_original_def modify_def del: fun_upd_apply | subst bind_def, simp, simp add: mdb_empty_abs'.empty_slot_ext_det_def2)+
1587  apply (simp add: put_def)
1588  apply (simp add: exec_gets exec_get exec_put del: fun_upd_apply | subst bind_def)+
1589  apply (clarsimp simp: state_relation_def)
1590  apply (drule updateMDB_the_lot, fastforce simp: pspace_relations_def, fastforce, fastforce)
1591   apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def
1592                         valid_mdb'_def valid_mdb_ctes_def)
1593  apply (elim conjE)
1594  apply (drule (4) updateMDB_the_lot, elim conjE)
1595  apply clarsimp
1596  apply (drule_tac s'=s''a and c=cap.NullCap in set_cap_not_quite_corres)
1597                     subgoal by simp
1598                    subgoal by simp
1599                   subgoal by simp
1600                  subgoal by fastforce
1601                 subgoal by fastforce
1602                subgoal by fastforce
1603               subgoal by fastforce
1604              subgoal by fastforce
1605             apply fastforce
1606            subgoal by fastforce
1607           subgoal by fastforce
1608          subgoal by fastforce
1609         apply (erule cte_wp_at_weakenE, rule TrueI)
1610        apply assumption
1611       subgoal by simp
1612      subgoal by simp
1613     subgoal by simp
1614    subgoal by simp
1615   apply (rule refl)
1616  apply clarsimp
1617  apply (drule updateCap_stuff, elim conjE, erule (1) impE)
1618  apply clarsimp
1619  apply (drule updateMDB_the_lot, force simp: pspace_relations_def, assumption+, simp)
1620  apply (rule bexI)
1621   prefer 2
1622   apply (simp only: trans_state_update[symmetric])
1623   apply (rule set_cap_trans_state)
1624   apply (rule set_cap_revokable_update)
1625   apply (erule set_cap_cdt_update)
1626  apply clarsimp
1627  apply (thin_tac "ctes_of t = s" for t s)+
1628  apply (thin_tac "ksMachineState t = p" for t p)+
1629  apply (thin_tac "ksCurThread t = p" for t p)+
1630  apply (thin_tac "ksReadyQueues t = p" for t p)+
1631  apply (thin_tac "ksSchedulerAction t = p" for t p)+
1632  apply (clarsimp simp: cte_wp_at_ctes_of)
1633  apply (case_tac rv')
1634  apply (rename_tac s_cap s_node)
1635  apply (subgoal_tac "cte_at slot a")
1636   prefer 2
1637   apply (fastforce elim: cte_wp_at_weakenE)
1638  apply (subgoal_tac "mdb_empty (ctes_of b) (cte_map slot) s_cap s_node")
1639   prefer 2
1640   apply (rule mdb_empty.intro)
1641   apply (rule mdb_ptr.intro)
1642    apply (rule vmdb.intro)
1643    subgoal by (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def)
1644   apply (rule mdb_ptr_axioms.intro)
1645   subgoal by simp
1646  apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv)
1647  apply (simp add: pspace_relations_def)
1648  apply (rule conjI)
1649   apply (clarsimp simp: data_at_def ghost_relation_typ_at set_cap_a_type_inv)
1650  apply (rule conjI)
1651   prefer 2
1652   apply (rule conjI)
1653    apply (clarsimp simp: cdt_list_relation_def)
1654    apply(frule invs_valid_pspace, frule invs_mdb)
1655    apply(subgoal_tac "no_mloop (cdt a) \<and> finite_depth (cdt a)")
1656     prefer 2
1657     subgoal by(simp add: finite_depth valid_mdb_def)
1658    apply(subgoal_tac "valid_mdb_ctes (ctes_of b)")
1659     prefer 2
1660     subgoal by(simp add: mdb_empty_def mdb_ptr_def vmdb_def)
1661    apply(clarsimp simp: valid_pspace_def)
1662
1663    apply(case_tac "cdt a slot")
1664     apply(simp add: next_slot_eq[OF mdb_empty_abs'.next_slot_no_parent])
1665     apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a)")
1666      subgoal by (simp)
1667     apply(clarsimp)
1668     apply(frule(1) mdb_empty.n_next)
1669     apply(clarsimp)
1670     apply(erule_tac x=aa in allE, erule_tac x=bb in allE)
1671     apply(simp split: if_split_asm)
1672      apply(drule cte_map_inj_eq)
1673           apply(drule cte_at_next_slot)
1674             apply(assumption)+
1675      apply(simp)
1676     apply(subgoal_tac "(ab, bc) = slot")
1677      prefer 2
1678      apply(drule_tac cte="CTE s_cap s_node" in valid_mdbD2')
1679        subgoal by (clarsimp simp: valid_mdb_ctes_def no_0_def)
1680       subgoal by (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
1681      apply(clarsimp)
1682      apply(rule cte_map_inj_eq)
1683           apply(assumption)
1684          apply(drule(3) cte_at_next_slot', assumption)
1685         apply(assumption)+
1686     apply(simp)
1687     apply(drule_tac p="(aa, bb)" in no_parent_not_next_slot)
1688        apply(assumption)+
1689     apply(clarsimp)
1690
1691    apply(simp add: next_slot_eq[OF mdb_empty_abs'.next_slot] split del: if_split)
1692    apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a)")
1693     subgoal by (simp)
1694    apply(case_tac "(aa, bb) = slot", simp)
1695    apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a) = Some slot")
1696     apply(simp)
1697     apply(case_tac "next_slot ac (cdt_list a) (cdt a)", simp)
1698     apply(simp)
1699     apply(frule(1) mdb_empty.n_next)
1700     apply(clarsimp)
1701     apply(erule_tac x=aa in allE', erule_tac x=bb in allE)
1702     apply(erule_tac x=ac in allE, erule_tac x=bd in allE)
1703     apply(clarsimp split: if_split_asm)
1704      apply(drule(1) no_self_loop_next)
1705      apply(simp)
1706     apply(drule_tac cte="CTE cap' node'" in valid_mdbD1')
1707       apply(fastforce simp: valid_mdb_ctes_def no_0_def)
1708      subgoal by (simp add: valid_mdb'_def)
1709     apply(clarsimp)
1710    apply(simp)
1711    apply(frule(1) mdb_empty.n_next)
1712    apply(erule_tac x=aa in allE, erule_tac x=bb in allE)
1713    apply(clarsimp split: if_split_asm)
1714     apply(drule(1) no_self_loop_prev)
1715     apply(clarsimp)
1716     apply(drule_tac cte="CTE s_cap s_node" in valid_mdbD2')
1717       apply(clarsimp simp: valid_mdb_ctes_def no_0_def)
1718      apply clarify
1719     apply(clarsimp)
1720     apply(drule cte_map_inj_eq)
1721          apply(drule(3) cte_at_next_slot')
1722          apply(assumption)+
1723     apply(simp)
1724    apply(erule disjE)
1725     apply(drule cte_map_inj_eq)
1726          apply(drule(3) cte_at_next_slot)
1727          apply(assumption)+
1728     apply(simp)
1729    subgoal by (simp)
1730   apply (simp add: revokable_relation_def)
1731   apply (clarsimp simp: in_set_cap_cte_at)
1732   apply (rule conjI)
1733    apply clarsimp
1734    apply (drule(1) mdb_empty.n_revokable)
1735    subgoal by clarsimp
1736   apply clarsimp
1737   apply (drule (1) mdb_empty.n_revokable)
1738   apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
1739    prefer 2
1740    apply (drule set_cap_caps_of_state_monad)
1741    subgoal by (force simp: null_filter_def)
1742   apply clarsimp
1743   apply (subgoal_tac "cte_at (aa, bb) a")
1744    prefer 2
1745    apply (drule null_filter_caps_of_stateD, erule cte_wp_cte_at)
1746   apply (drule (2) cte_map_inj_ps, fastforce)
1747   subgoal by simp
1748  apply (clarsimp simp add: cdt_relation_def)
1749  apply (subst mdb_empty_abs.descendants, assumption)
1750  apply (subst mdb_empty.descendants, assumption)
1751  apply clarsimp
1752  apply (frule_tac p="(aa, bb)" in in_set_cap_cte_at)
1753  apply clarsimp
1754  apply (frule (2) cte_map_inj_ps, fastforce)
1755  apply simp
1756  apply (case_tac "slot \<in> descendants_of (aa,bb) (cdt a)")
1757   apply (subst inj_on_image_set_diff)
1758      apply (rule inj_on_descendants_cte_map)
1759         apply fastforce
1760        apply fastforce
1761       apply fastforce
1762      apply fastforce
1763     apply fastforce
1764    subgoal by simp
1765   subgoal by simp
1766  apply simp
1767  apply (subgoal_tac "cte_map slot \<notin> descendants_of' (cte_map (aa,bb)) (ctes_of b)")
1768   subgoal by simp
1769  apply (erule_tac x=aa in allE, erule allE, erule (1) impE)
1770  apply (drule_tac s="cte_map ` u" for u in sym)
1771  apply clarsimp
1772  apply (drule cte_map_inj_eq, assumption)
1773      apply (erule descendants_of_cte_at, fastforce)
1774     apply fastforce
1775    apply fastforce
1776   apply fastforce
1777  apply simp
1778  done
1779
1780
1781
1782text {* Some facts about is_final_cap/isFinalCapability *}
1783
1784lemma isFinalCapability_inv:
1785  "\<lbrace>P\<rbrace> isFinalCapability cap \<lbrace>\<lambda>_. P\<rbrace>"
1786  apply (simp add: isFinalCapability_def Let_def
1787              split del: if_split cong: if_cong)
1788  apply (rule hoare_pre, wp)
1789   apply (rule hoare_post_imp [where Q="\<lambda>s. P"], simp)
1790   apply wp
1791  apply simp
1792  done
1793
1794definition
1795  final_matters' :: "capability \<Rightarrow> bool"
1796where
1797 "final_matters' cap \<equiv> case cap of
1798    EndpointCap ref bdg s r g \<Rightarrow> True
1799  | NotificationCap ref bdg s r \<Rightarrow> True
1800  | ThreadCap ref \<Rightarrow> True
1801  | CNodeCap ref bits gd gs \<Rightarrow> True
1802  | Zombie ptr zb n \<Rightarrow> True
1803  | IRQHandlerCap irq \<Rightarrow> True
1804  | ArchObjectCap acap \<Rightarrow> (case acap of
1805    PageCap d ref rghts sz mapdata \<Rightarrow> False
1806  | ASIDControlCap \<Rightarrow> False
1807  | _ \<Rightarrow> True)
1808  | _ \<Rightarrow> False"
1809
1810lemma final_matters_Master:
1811  "final_matters' (capMasterCap cap) = final_matters' cap"
1812  by (simp add: capMasterCap_def split: capability.split arch_capability.split,
1813      simp add: final_matters'_def)
1814
1815lemma final_matters_sameRegion_sameObject:
1816  "final_matters' cap \<Longrightarrow> sameRegionAs cap cap' = sameObjectAs cap cap'"
1817  apply (rule iffI)
1818   apply (erule sameRegionAsE)
1819      apply (simp add: sameObjectAs_def3)
1820      apply (clarsimp simp: isCap_simps sameObjectAs_sameRegionAs final_matters'_def
1821        split:capability.splits arch_capability.splits)+
1822  done
1823
1824lemma final_matters_sameRegion_sameObject2:
1825  "\<lbrakk> final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap' \<rbrakk>
1826     \<Longrightarrow> sameRegionAs cap cap' = sameObjectAs cap cap'"
1827  apply (rule iffI)
1828   apply (erule sameRegionAsE)
1829      apply (simp add: sameObjectAs_def3)
1830      apply (fastforce simp: isCap_simps final_matters'_def)
1831     apply simp
1832    apply (clarsimp simp: final_matters'_def isCap_simps)
1833   apply (clarsimp simp: final_matters'_def isCap_simps)
1834  apply (erule sameObjectAs_sameRegionAs)
1835  done
1836
1837lemma notFinal_prev_or_next:
1838  "\<lbrakk> \<not> isFinal cap x (cteCaps_of s); mdb_chunked (ctes_of s);
1839      valid_dlist (ctes_of s); no_0 (ctes_of s);
1840      ctes_of s x = Some (CTE cap node); final_matters' cap \<rbrakk>
1841     \<Longrightarrow> (\<exists>cap' node'. ctes_of s (mdbPrev node) = Some (CTE cap' node')
1842              \<and> sameObjectAs cap cap')
1843      \<or> (\<exists>cap' node'. ctes_of s (mdbNext node) = Some (CTE cap' node')
1844              \<and> sameObjectAs cap cap')"
1845  apply (erule not_FinalE)
1846   apply (clarsimp simp: isCap_simps final_matters'_def)
1847  apply (clarsimp simp: mdb_chunked_def cte_wp_at_ctes_of cteCaps_of_def
1848                   del: disjCI)
1849  apply (erule_tac x=x in allE, erule_tac x=p in allE)
1850  apply simp
1851  apply (case_tac z, simp add: sameObjectAs_sameRegionAs)
1852  apply (elim conjE disjE, simp_all add: is_chunk_def)
1853   apply (rule disjI2)
1854   apply (drule tranclD)
1855   apply (clarsimp simp: mdb_next_unfold)
1856   apply (drule spec[where x="mdbNext node"])
1857   apply simp
1858   apply (drule mp[where P="ctes_of s \<turnstile> x \<leadsto>\<^sup>+ mdbNext node"])
1859    apply (rule trancl.intros(1), simp add: mdb_next_unfold)
1860   apply clarsimp
1861   apply (drule rtranclD)
1862   apply (erule disjE, clarsimp+)
1863   apply (drule tranclD)
1864   apply (clarsimp simp: mdb_next_unfold final_matters_sameRegion_sameObject)
1865  apply (rule disjI1)
1866  apply clarsimp
1867  apply (drule tranclD2)
1868  apply clarsimp
1869  apply (frule vdlist_nextD0)
1870    apply clarsimp
1871   apply assumption
1872  apply (clarsimp simp: mdb_prev_def)
1873  apply (drule rtranclD)
1874  apply (erule disjE, clarsimp+)
1875  apply (drule spec, drule(1) mp)
1876  apply (drule mp, rule trancl_into_rtrancl, erule trancl.intros(1))
1877  apply clarsimp
1878  apply (drule iffD1 [OF final_matters_sameRegion_sameObject, rotated])
1879   apply (subst final_matters_Master[symmetric])
1880   apply (subst(asm) final_matters_Master[symmetric])
1881   apply (clarsimp simp: sameObjectAs_def3)
1882  apply (clarsimp simp: sameObjectAs_def3)
1883  done
1884
1885lemma isFinal:
1886  "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s
1887          \<and> final_matters' (cteCap cte)
1888          \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace>
1889    isFinalCapability cte
1890   \<lbrace>Q\<rbrace>"
1891  unfolding isFinalCapability_def
1892  apply (cases cte)
1893  apply (rename_tac cap node)
1894  apply (unfold Let_def)
1895  apply (simp only: if_False)
1896  apply (wp getCTE_wp')
1897  apply (cases "mdbPrev (cteMDBNode cte) = nullPointer")
1898   apply simp
1899   apply (clarsimp simp: valid_mdb_ctes_def valid_mdb'_def
1900                         cte_wp_at_ctes_of)
1901   apply (rule conjI, clarsimp simp: nullPointer_def)
1902    apply (erule rsubst[where P="\<lambda>x. Q x s" for s], simp)
1903    apply (rule classical)
1904    apply (drule(5) notFinal_prev_or_next)
1905    apply clarsimp
1906   apply (clarsimp simp: nullPointer_def)
1907   apply (erule rsubst[where P="\<lambda>x. Q x s" for s])
1908   apply (rule sym, rule iffI)
1909    apply (rule classical)
1910    apply (drule(5) notFinal_prev_or_next)
1911    apply clarsimp
1912   apply clarsimp
1913   apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def)
1914   apply (case_tac cte)
1915   apply clarsimp
1916   apply (clarsimp simp add: isFinal_def)
1917   apply (erule_tac x="mdbNext node" in allE)
1918   apply simp
1919   apply (erule impE)
1920    apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def)
1921    apply (drule (1) mdb_chain_0_no_loops)
1922    apply simp
1923   apply (clarsimp simp: sameObjectAs_def3 isCap_simps)
1924  apply simp
1925  apply (clarsimp simp: cte_wp_at_ctes_of
1926                        valid_mdb_ctes_def valid_mdb'_def)
1927  apply (case_tac cte)
1928  apply clarsimp
1929  apply (rule conjI)
1930   apply clarsimp
1931   apply (erule rsubst[where P="\<lambda>x. Q x s" for s])
1932   apply clarsimp
1933   apply (clarsimp simp: isFinal_def cteCaps_of_def)
1934   apply (erule_tac x="mdbPrev node" in allE)
1935   apply simp
1936   apply (erule impE)
1937    apply clarsimp
1938    apply (drule (1) mdb_chain_0_no_loops)
1939    apply (subgoal_tac "ctes_of s (mdbNext node) = Some (CTE cap node)")
1940     apply clarsimp
1941    apply (erule (1) valid_dlistEp)
1942     apply clarsimp
1943    apply (case_tac cte')
1944    apply clarsimp
1945   apply (clarsimp simp add: sameObjectAs_def3 isCap_simps)
1946  apply clarsimp
1947  apply (rule conjI)
1948   apply clarsimp
1949   apply (erule rsubst[where P="\<lambda>x. Q x s" for s], simp)
1950   apply (rule classical, drule(5) notFinal_prev_or_next)
1951   apply (clarsimp simp: sameObjectAs_sym nullPointer_def)
1952  apply (clarsimp simp: nullPointer_def)
1953  apply (erule rsubst[where P="\<lambda>x. Q x s" for s])
1954  apply (rule sym, rule iffI)
1955   apply (rule classical, drule(5) notFinal_prev_or_next)
1956   apply (clarsimp simp: sameObjectAs_sym)
1957   apply auto[1]
1958  apply (clarsimp simp: isFinal_def cteCaps_of_def)
1959  apply (case_tac cte)
1960  apply (erule_tac x="mdbNext node" in allE)
1961  apply simp
1962  apply (erule impE)
1963   apply clarsimp
1964   apply (drule (1) mdb_chain_0_no_loops)
1965   apply simp
1966  apply clarsimp
1967  apply (clarsimp simp: isCap_simps sameObjectAs_def3)
1968  done
1969end
1970
1971lemma (in vmdb) isFinal_no_subtree:
1972  "\<lbrakk> m \<turnstile> sl \<rightarrow> p; isFinal cap sl (option_map cteCap o m);
1973      m sl = Some (CTE cap n); final_matters' cap \<rbrakk> \<Longrightarrow> False"
1974  apply (erule subtree.induct)
1975   apply (case_tac "c'=sl", simp)
1976   apply (clarsimp simp: isFinal_def parentOf_def mdb_next_unfold cteCaps_of_def)
1977   apply (erule_tac x="mdbNext n" in allE)
1978   apply simp
1979   apply (clarsimp simp: isMDBParentOf_CTE final_matters_sameRegion_sameObject)
1980   apply (clarsimp simp: isCap_simps sameObjectAs_def3)
1981  apply clarsimp
1982  done
1983
1984lemma isFinal_no_descendants:
1985  "\<lbrakk> isFinal cap sl (cteCaps_of s); ctes_of s sl = Some (CTE cap n);
1986      valid_mdb' s; final_matters' cap \<rbrakk>
1987  \<Longrightarrow> descendants_of' sl (ctes_of s) = {}"
1988  apply (clarsimp simp add: descendants_of'_def cteCaps_of_def)
1989  apply (erule(3) vmdb.isFinal_no_subtree[rotated])
1990  apply unfold_locales[1]
1991  apply (simp add: valid_mdb'_def)
1992  done
1993
1994lemma (in vmdb) isFinal_untypedParent:
1995  assumes x: "m slot = Some cte" "isFinal (cteCap cte) slot (option_map cteCap o m)"
1996             "final_matters' (cteCap cte) \<and> \<not> isIRQHandlerCap (cteCap cte)"
1997  shows
1998  "m \<turnstile> x \<rightarrow> slot \<Longrightarrow>
1999  (\<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> RetypeDecls_H.sameRegionAs (cteCap cte') (cteCap cte))"
2000  apply (cases "x=slot", simp)
2001  apply (insert x)
2002  apply (frule subtree_mdb_next)
2003  apply (drule subtree_parent)
2004  apply (drule tranclD)
2005  apply clarsimp
2006  apply (clarsimp simp: mdb_next_unfold parentOf_def isFinal_def)
2007  apply (case_tac cte')
2008  apply (rename_tac c' n')
2009  apply (cases cte)
2010  apply (rename_tac c n)
2011  apply simp
2012  apply (erule_tac x=x in allE)
2013  apply clarsimp
2014  apply (drule isMDBParent_sameRegion)
2015  apply simp
2016  apply (rule classical, simp)
2017  apply (simp add: final_matters_sameRegion_sameObject2
2018                   sameObjectAs_sym)
2019  done
2020
2021lemma isFinal2:
2022  "\<lbrace>\<lambda>s. cte_wp_at' ((=) cte) sl s \<and> valid_mdb' s\<rbrace>
2023     isFinalCapability cte
2024   \<lbrace>\<lambda>rv s. rv \<and> final_matters' (cteCap cte) \<longrightarrow>
2025             isFinal (cteCap cte) sl (cteCaps_of s)\<rbrace>"
2026  apply (cases "final_matters' (cteCap cte)")
2027   apply simp
2028   apply (wp isFinal[where x=sl])
2029   apply simp
2030  apply (simp|wp)+
2031  done
2032
2033context begin interpretation Arch . (*FIXME: arch_split*)
2034
2035lemma no_fail_isFinalCapability [wp]:
2036  "no_fail (valid_mdb' and cte_wp_at' ((=) cte) p) (isFinalCapability cte)"
2037  apply (simp add: isFinalCapability_def)
2038  apply (clarsimp simp: Let_def split del: if_split)
2039  apply (rule no_fail_pre, wp getCTE_wp')
2040  apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def cte_wp_at_ctes_of nullPointer_def)
2041  apply (rule conjI)
2042   apply clarsimp
2043   apply (erule (2) valid_dlistEp)
2044   apply simp
2045  apply clarsimp
2046  apply (rule conjI)
2047   apply (erule (2) valid_dlistEn)
2048   apply simp
2049  apply clarsimp
2050  apply (rule valid_dlistEn, assumption+)
2051  apply (erule (2) valid_dlistEp)
2052  apply simp
2053  done
2054
2055lemma corres_gets_lift:
2056  assumes inv: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>"
2057  assumes res: "\<lbrace>Q'\<rbrace> g \<lbrace>\<lambda>r s. r = g' s\<rbrace>"
2058  assumes Q: "\<And>s. Q s \<Longrightarrow> Q' s"
2059  assumes nf: "no_fail Q g"
2060  shows "corres r P Q f (gets g') \<Longrightarrow> corres r P Q f g"
2061  apply (clarsimp simp add: corres_underlying_def simpler_gets_def)
2062  apply (drule (1) bspec)
2063  apply (rule conjI)
2064   apply clarsimp
2065   apply (rule bexI)
2066    prefer 2
2067    apply assumption
2068   apply simp
2069   apply (frule in_inv_by_hoareD [OF inv])
2070   apply simp
2071   apply (drule use_valid, rule res)
2072    apply (erule Q)
2073   apply simp
2074  apply (insert nf)
2075  apply (clarsimp simp: no_fail_def)
2076  done
2077
2078lemma obj_refs_Master:
2079  "\<lbrakk> cap_relation cap cap'; P cap \<rbrakk>
2080      \<Longrightarrow> obj_refs cap =
2081           (if capClass (capMasterCap cap') = PhysicalClass
2082                  \<and> \<not> isUntypedCap (capMasterCap cap')
2083            then {capUntypedPtr (capMasterCap cap')} else {})"
2084  by (clarsimp simp: isCap_simps
2085              split: cap_relation_split_asm arch_cap.split_asm)
2086
2087lemma final_cap_corres':
2088  "final_matters' (cteCap cte) \<Longrightarrow>
2089   corres (=) (invs and cte_wp_at ((=) cap) ptr)
2090               (invs' and cte_wp_at' ((=) cte) (cte_map ptr))
2091       (is_final_cap cap) (isFinalCapability cte)"
2092  apply (rule corres_gets_lift)
2093      apply (rule isFinalCapability_inv)
2094     apply (rule isFinal[where x="cte_map ptr"])
2095    apply clarsimp
2096    apply (rule conjI, clarsimp)
2097    apply (rule refl)
2098   apply (rule no_fail_pre, wp, fastforce)
2099  apply (simp add: is_final_cap_def)
2100  apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def state_relation_def)
2101  apply (frule (1) pspace_relation_ctes_ofI)
2102    apply fastforce
2103   apply fastforce
2104  apply clarsimp
2105  apply (rule iffI)
2106   apply (simp add: is_final_cap'_def2 isFinal_def)
2107   apply clarsimp
2108   apply (subgoal_tac "obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {} \<or> arch_gen_refs cap \<noteq> {}")
2109    prefer 2
2110    apply (erule_tac x=a in allE)
2111    apply (erule_tac x=b in allE)
2112    apply (clarsimp simp: cte_wp_at_def gen_obj_refs_Int)
2113   apply (subgoal_tac "ptr = (a,b)")
2114    prefer 2
2115    apply (erule_tac x="fst ptr" in allE)
2116    apply (erule_tac x="snd ptr" in allE)
2117    apply (clarsimp simp: cte_wp_at_def gen_obj_refs_Int)
2118   apply clarsimp
2119   apply (rule context_conjI)
2120    apply (clarsimp simp: isCap_simps)
2121    apply (cases cap, auto)[1]
2122   apply clarsimp
2123   apply (drule_tac x=p' in pspace_relation_cte_wp_atI, assumption)
2124    apply fastforce
2125   apply clarsimp
2126   apply (erule_tac x=aa in allE)
2127   apply (erule_tac x=ba in allE)
2128   apply (clarsimp simp: cte_wp_at_caps_of_state)
2129   apply (clarsimp simp: sameObjectAs_def3 obj_refs_Master cap_irqs_relation_Master
2130                         arch_gen_refs_relation_Master gen_obj_refs_Int
2131                   cong: if_cong
2132                  split: capability.split_asm)
2133  apply (clarsimp simp: isFinal_def is_final_cap'_def3)
2134  apply (rule_tac x="fst ptr" in exI)
2135  apply (rule_tac x="snd ptr" in exI)
2136  apply (rule conjI)
2137   apply (clarsimp simp: cte_wp_at_def final_matters'_def
2138                         gen_obj_refs_Int
2139                  split: cap_relation_split_asm arch_cap.split_asm)
2140  apply clarsimp
2141  apply (drule_tac p="(a,b)" in cte_wp_at_eqD)
2142  apply clarsimp
2143  apply (frule_tac slot="(a,b)" in pspace_relation_ctes_ofI, assumption)
2144    apply fastforce
2145   apply fastforce
2146  apply clarsimp
2147  apply (frule_tac p="(a,b)" in cte_wp_valid_cap, fastforce)
2148  apply (erule_tac x="cte_map (a,b)" in allE)
2149  apply simp
2150  apply (erule impCE, simp, drule cte_map_inj_eq)
2151        apply (erule cte_wp_at_weakenE, rule TrueI)
2152       apply (erule cte_wp_at_weakenE, rule TrueI)
2153      apply fastforce
2154     apply fastforce
2155    apply (erule invs_distinct)
2156   apply simp
2157  apply (frule_tac p=ptr in cte_wp_valid_cap, fastforce)
2158  apply (clarsimp simp: cte_wp_at_def gen_obj_refs_Int)
2159  apply (rule conjI)
2160   apply (rule classical)
2161   apply (frule(1) zombies_finalD2[OF _ _ _ invs_zombies],
2162          simp?, clarsimp, assumption+)
2163   subgoal by (clarsimp simp: sameObjectAs_def3 isCap_simps valid_cap_def
2164                         obj_at_def is_obj_defs a_type_def final_matters'_def
2165                  split: cap.split_asm arch_cap.split_asm
2166                         option.split_asm if_split_asm,
2167          simp_all add: is_cap_defs)
2168  apply (rule classical)
2169  by (clarsimp simp: cap_irqs_def cap_irq_opt_def sameObjectAs_def3 isCap_simps arch_gen_obj_refs_def
2170                 split: cap.split_asm)
2171
2172lemma final_cap_corres:
2173  "corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv')
2174          (invs and cte_wp_at ((=) cap) ptr)
2175          (invs' and cte_wp_at' ((=) cte) (cte_map ptr))
2176       (is_final_cap cap) (isFinalCapability cte)"
2177  apply (cases "final_matters' (cteCap cte)")
2178   apply simp
2179   apply (erule final_cap_corres')
2180  apply (subst bind_return[symmetric],
2181         rule corres_symb_exec_r)
2182     apply (rule corres_no_failI)
2183      apply wp
2184     apply (clarsimp simp: in_monad is_final_cap_def simpler_gets_def)
2185    apply (wp isFinalCapability_inv)+
2186  apply fastforce
2187  done
2188
2189text {* Facts about finalise_cap/finaliseCap and
2190        cap_delete_one/cteDelete in no particular order *}
2191
2192
2193definition
2194  finaliseCapTrue_standin_simple_def:
2195  "finaliseCapTrue_standin cap fin \<equiv> finaliseCap cap fin True"
2196
2197context
2198begin
2199
2200declare if_cong [cong]
2201
2202lemmas finaliseCapTrue_standin_def
2203    = finaliseCapTrue_standin_simple_def
2204        [unfolded finaliseCap_def, simplified]
2205
2206lemmas cteDeleteOne_def'
2207    = eq_reflection [OF cteDeleteOne_def]
2208lemmas cteDeleteOne_def
2209    = cteDeleteOne_def'[folded finaliseCapTrue_standin_simple_def]
2210
2211crunch typ_at'[wp]: cteDeleteOne, suspend, prepareThreadDelete "\<lambda>s. P (typ_at' T p s)"
2212  (wp: crunch_wps getObject_inv loadObject_default_inv
2213   simp: crunch_simps unless_def o_def
2214   ignore: getObject)
2215
2216end
2217
2218lemmas cancelAllIPC_typs[wp] = typ_at_lifts [OF cancelAllIPC_typ_at']
2219lemmas cancelAllSignals_typs[wp] = typ_at_lifts [OF cancelAllSignals_typ_at']
2220lemmas suspend_typs[wp] = typ_at_lifts [OF suspend_typ_at']
2221
2222definition
2223  arch_cap_has_cleanup' :: "arch_capability \<Rightarrow> bool"
2224where
2225  "arch_cap_has_cleanup' acap \<equiv> False"
2226
2227definition
2228  cap_has_cleanup' :: "capability \<Rightarrow> bool"
2229where
2230  "cap_has_cleanup' cap \<equiv> case cap of
2231     IRQHandlerCap _ \<Rightarrow> True
2232   | ArchObjectCap acap \<Rightarrow> arch_cap_has_cleanup' acap
2233   | _ \<Rightarrow> False"
2234
2235lemmas cap_has_cleanup'_simps[simp] = cap_has_cleanup'_def[split_simps capability.split]
2236
2237lemma finaliseCap_cases[wp]:
2238  "\<lbrace>\<top>\<rbrace>
2239     finaliseCap cap final flag
2240   \<lbrace>\<lambda>rv s. fst rv = NullCap \<and> (snd rv \<noteq> NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd rv = cap)
2241     \<or>
2242       isZombie (fst rv) \<and> final \<and> \<not> flag \<and> snd rv = NullCap
2243        \<and> capUntypedPtr (fst rv) = capUntypedPtr cap
2244        \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)\<rbrace>"
2245  apply (simp add: finaliseCap_def ARM_H.finaliseCap_def Let_def
2246                   getThreadCSpaceRoot
2247             cong: if_cong split del: if_split)
2248  apply (rule hoare_pre)
2249   apply ((wp | simp add: isCap_simps split del: if_split
2250              | wpc
2251              | simp only: valid_NullCap fst_conv snd_conv)+)[1]
2252  apply (simp only: simp_thms fst_conv snd_conv option.simps if_cancel
2253                    o_def)
2254  apply (intro allI impI conjI TrueI)
2255  apply (auto simp add: isCap_simps cap_has_cleanup'_def)
2256  done
2257
2258crunch aligned'[wp]: finaliseCap "pspace_aligned'"
2259  (simp: crunch_simps assertE_def unless_def o_def
2260 ignore: getObject setObject forM ignoreFailure
2261     wp: getObject_inv loadObject_default_inv crunch_wps)
2262
2263crunch distinct'[wp]: finaliseCap "pspace_distinct'"
2264  (ignore: getObject setObject forM ignoreFailure
2265     simp: crunch_simps assertE_def unless_def o_def
2266       wp: getObject_inv loadObject_default_inv crunch_wps)
2267
2268crunch typ_at'[wp]: finaliseCap "\<lambda>s. P (typ_at' T p s)"
2269  (simp: crunch_simps assertE_def ignore: getObject setObject
2270     wp: getObject_inv loadObject_default_inv crunch_wps)
2271lemmas finaliseCap_typ_ats[wp] = typ_at_lifts[OF finaliseCap_typ_at']
2272
2273crunch it'[wp]: finaliseCap "\<lambda>s. P (ksIdleThread s)"
2274  (ignore: getObject setObject forM ignoreFailure maskInterrupt
2275   wp: mapM_x_wp_inv mapM_wp' hoare_drop_imps getObject_inv loadObject_default_inv
2276   simp: crunch_simps o_def)
2277
2278crunch vs_lookup[wp]: flush_space "\<lambda>s. P (vs_lookup s)"
2279  (wp: crunch_wps)
2280
2281declare doUnbindNotification_def[simp]
2282
2283lemma ntfn_q_refs_of'_mult:
2284  "ntfn_q_refs_of' ntfn = (case ntfn of Structures_H.WaitingNtfn q \<Rightarrow> set q | _ \<Rightarrow> {}) \<times> {NTFNSignal}"
2285  by (cases ntfn, simp_all)
2286
2287lemma tcb_st_not_Bound:
2288  "(p, NTFNBound) \<notin> tcb_st_refs_of' ts"
2289  "(p, TCBBound) \<notin> tcb_st_refs_of' ts"
2290  by (auto simp: tcb_st_refs_of'_def split: Structures_H.thread_state.split)
2291
2292lemma unbindNotification_invs[wp]:
2293  "\<lbrace>invs'\<rbrace> unbindNotification tcb \<lbrace>\<lambda>rv. invs'\<rbrace>"
2294  apply (simp add: unbindNotification_def invs'_def valid_state'_def)
2295  apply (rule hoare_seq_ext[OF _ gbn_sp'])
2296  apply (case_tac ntfnPtr, clarsimp, wp, clarsimp)
2297  apply clarsimp
2298  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
2299  apply (rule hoare_pre)
2300  apply (wp sbn'_valid_pspace'_inv sbn_sch_act' sbn_valid_queues valid_irq_node_lift
2301            irqs_masked_lift setBoundNotification_ct_not_inQ
2302            untyped_ranges_zero_lift | clarsimp simp: cteCaps_of_def o_def)+
2303  apply (rule conjI)
2304   apply (clarsimp elim!: obj_atE'
2305                    simp: projectKOs
2306                   dest!: pred_tcb_at')
2307  apply (clarsimp simp: pred_tcb_at' conj_comms)
2308  apply (frule bound_tcb_ex_cap'', clarsimp+)
2309  apply (frule(1) sym_refs_bound_tcb_atD')
2310  apply (frule(1) sym_refs_obj_atD')
2311  apply (clarsimp simp: refs_of_rev')
2312  apply normalise_obj_at'
2313  apply (subst delta_sym_refs, assumption)
2314    apply (auto split: if_split_asm)[1]
2315   apply (auto simp: tcb_st_not_Bound ntfn_q_refs_of'_mult split: if_split_asm)[1]
2316  apply (frule obj_at_valid_objs', clarsimp+)
2317  apply (simp add: valid_ntfn'_def valid_obj'_def projectKOs
2318            split: ntfn.splits)
2319  apply (erule if_live_then_nonz_capE')
2320  apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs)
2321  done
2322
2323lemma ntfn_bound_tcb_at':
2324  "\<lbrakk>sym_refs (state_refs_of' s); valid_objs' s; ko_at' ntfn ntfnptr s;
2325    ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk>
2326  \<Longrightarrow> bound_tcb_at' P tcbptr s"
2327  apply (drule_tac x=ntfnptr in sym_refsD[rotated])
2328   apply (clarsimp simp: obj_at'_def projectKOs)
2329   apply (fastforce simp: state_refs_of'_def)
2330  apply (auto simp: pred_tcb_at'_def obj_at'_def valid_obj'_def valid_ntfn'_def
2331                    state_refs_of'_def refs_of_rev' projectKOs
2332          simp del: refs_of_simps
2333             elim!: valid_objsE
2334             split: option.splits if_split_asm)
2335  done
2336
2337
2338lemma unbindMaybeNotification_invs[wp]:
2339  "\<lbrace>invs'\<rbrace> unbindMaybeNotification ntfnptr \<lbrace>\<lambda>rv. invs'\<rbrace>"
2340  apply (simp add: unbindMaybeNotification_def invs'_def valid_state'_def)
2341  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
2342  apply (rule hoare_pre)
2343   apply (wp sbn'_valid_pspace'_inv sbn_sch_act' sbn_valid_queues valid_irq_node_lift
2344             irqs_masked_lift setBoundNotification_ct_not_inQ
2345             untyped_ranges_zero_lift
2346             | wpc | clarsimp simp: cteCaps_of_def o_def)+
2347  apply safe[1]
2348           defer 3
2349           defer 7
2350           apply (fold_subgoals (prefix))[8]
2351           subgoal premises prems using prems by (auto simp: pred_tcb_at' valid_pspace'_def projectKOs valid_obj'_def valid_ntfn'_def
2352                             ko_wp_at'_def
2353                      elim!: obj_atE' valid_objsE' if_live_then_nonz_capE'
2354                      split: option.splits ntfn.splits)
2355   apply (rule delta_sym_refs, assumption)
2356    apply (fold_subgoals (prefix))[2]
2357    subgoal premises prems using prems by (fastforce simp: symreftype_inverse' ntfn_q_refs_of'_def
2358                    split: ntfn.splits if_split_asm
2359                     dest!: ko_at_state_refs_ofD')+
2360  apply (rule delta_sym_refs, assumption)
2361   apply (clarsimp split: if_split_asm)
2362   apply (frule ko_at_state_refs_ofD', simp)
2363  apply (clarsimp split: if_split_asm)
2364   apply (frule_tac P="(=) (Some ntfnptr)" in ntfn_bound_tcb_at', simp_all add: valid_pspace'_def)[1]
2365   subgoal by (fastforce simp: ntfn_q_refs_of'_def state_refs_of'_def tcb_ntfn_is_bound'_def
2366                          tcb_st_refs_of'_def
2367                   dest!: bound_tcb_at_state_refs_ofD'
2368                   split: ntfn.splits thread_state.splits)
2369  apply (frule ko_at_state_refs_ofD', simp)
2370  done
2371
2372(* Ugh, required to be able to split out the abstract invs *)
2373lemma finaliseCap_True_invs[wp]:
2374  "\<lbrace>invs'\<rbrace> finaliseCap cap final True \<lbrace>\<lambda>rv. invs'\<rbrace>"
2375  apply (simp add: finaliseCap_def Let_def)
2376  apply safe
2377    apply (wp irqs_masked_lift| simp | wpc)+
2378  done
2379
2380crunch invs'[wp]: flushSpace "invs'" (ignore: doMachineOp)
2381
2382lemma ct_not_inQ_ksArchState_update[simp]:
2383  "ct_not_inQ (s\<lparr>ksArchState := v\<rparr>) = ct_not_inQ s"
2384  by (simp add: ct_not_inQ_def)
2385
2386lemma invs_asid_update_strg':
2387  "invs' s \<and> tab = armKSASIDTable (ksArchState s) \<longrightarrow>
2388   invs' (s\<lparr>ksArchState := armKSASIDTable_update
2389            (\<lambda>_. tab (asid := None)) (ksArchState s)\<rparr>)"
2390  apply (simp add: invs'_def)
2391  apply (simp add: valid_state'_def)
2392  apply (simp add: valid_global_refs'_def global_refs'_def valid_arch_state'_def valid_asid_table'_def valid_machine_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
2393  apply (auto simp add: ran_def split: if_split_asm)
2394  done
2395
2396lemma invalidateASIDEntry_invs' [wp]:
2397  "\<lbrace>invs'\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. invs'\<rbrace>"
2398  apply (simp add: invalidateASIDEntry_def invalidateASID_def
2399                   invalidateHWASIDEntry_def bind_assoc)
2400  apply (wp loadHWASID_wp | simp)+
2401  apply (clarsimp simp: fun_upd_def[symmetric])
2402  apply (rule conjI)
2403   apply (clarsimp simp: invs'_def valid_state'_def)
2404   apply (rule conjI)
2405    apply (simp add: valid_global_refs'_def
2406                     global_refs'_def)
2407   apply (simp add: valid_arch_state'_def ran_def
2408                    valid_asid_table'_def is_inv_None_upd
2409                    valid_machine_state'_def
2410                    comp_upd_simp fun_upd_def[symmetric]
2411                    inj_on_fun_upd_elsewhere
2412                    valid_asid_map'_def
2413                    ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
2414   subgoal by (auto elim!: subset_inj_on)
2415  apply (clarsimp simp: invs'_def valid_state'_def)
2416  apply (rule conjI)
2417   apply (simp add: valid_global_refs'_def
2418                    global_refs'_def)
2419  apply (rule conjI)
2420   apply (simp add: valid_arch_state'_def ran_def
2421                    valid_asid_table'_def None_upd_eq
2422                    fun_upd_def[symmetric] comp_upd_simp)
2423  apply (simp add: valid_machine_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
2424  done
2425
2426lemma deleteASIDPool_invs[wp]:
2427  "\<lbrace>invs'\<rbrace> deleteASIDPool asid pool \<lbrace>\<lambda>rv. invs'\<rbrace>"
2428  apply (simp add: deleteASIDPool_def)
2429  apply wp
2430    apply (simp del: fun_upd_apply)
2431    apply (strengthen invs_asid_update_strg')
2432  apply (wp mapM_wp' getObject_inv loadObject_default_inv
2433              | simp)+
2434  done
2435
2436lemma invalidateASIDEntry_valid_ap' [wp]:
2437  "\<lbrace>valid_asid_pool' p\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. valid_asid_pool' p\<rbrace>"
2438  apply (simp add: invalidateASIDEntry_def invalidateASID_def
2439                   invalidateHWASIDEntry_def bind_assoc)
2440  apply (wp loadHWASID_wp | simp)+
2441  apply (case_tac p)
2442  apply (clarsimp simp del: fun_upd_apply)
2443  done
2444
2445lemmas flushSpace_typ_ats' [wp] = typ_at_lifts [OF flushSpace_typ_at']
2446
2447lemma deleteASID_invs'[wp]:
2448  "\<lbrace>invs'\<rbrace> deleteASID asid pd \<lbrace>\<lambda>rv. invs'\<rbrace>"
2449  apply (simp add: deleteASID_def cong: option.case_cong)
2450  apply (rule hoare_pre)
2451   apply (wp | wpc)+
2452      apply (rule_tac Q="\<lambda>rv. valid_obj' (injectKO rv) and invs'"
2453                in hoare_post_imp)
2454     apply (clarsimp split: if_split_asm del: subsetI)
2455     apply (simp add: fun_upd_def[symmetric] valid_obj'_def)
2456     apply (case_tac r, simp)
2457     apply (subst inv_f_f, rule inj_onI, simp)+
2458     apply (rule conjI)
2459      apply clarsimp
2460      apply (drule subsetD, blast)
2461      apply clarsimp
2462     apply (auto dest!: ran_del_subset)[1]
2463    apply (wp getObject_valid_obj getObject_inv loadObject_default_inv
2464             | simp add: objBits_simps archObjSize_def pageBits_def)+
2465  apply clarsimp
2466  done
2467
2468lemma arch_finaliseCap_invs[wp]:
2469  "\<lbrace>invs' and valid_cap' (ArchObjectCap cap)\<rbrace>
2470     Arch.finaliseCap cap fin
2471   \<lbrace>\<lambda>rv. invs'\<rbrace>"
2472  unfolding ARM_H.finaliseCap_def
2473  apply clarsimp
2474  apply (safe ; wpsimp)
2475  done
2476
2477lemma arch_finaliseCap_removeable[wp]:
2478  "\<lbrace>\<lambda>s. s \<turnstile>' ArchObjectCap cap \<and> invs' s
2479       \<and> (final \<and> final_matters' (ArchObjectCap cap)
2480            \<longrightarrow> isFinal (ArchObjectCap cap) slot (cteCaps_of s))\<rbrace>
2481     Arch.finaliseCap cap final
2482   \<lbrace>\<lambda>rv s. isNullCap (fst rv) \<and> removeable' slot s (ArchObjectCap cap) \<and> isNullCap (snd rv)\<rbrace>"
2483  apply (simp add: ARM_H.finaliseCap_def
2484                   removeable'_def)
2485  apply (safe ; wpsimp)
2486  done
2487
2488lemma isZombie_Null:
2489  "\<not> isZombie NullCap"
2490  by (simp add: isCap_simps)
2491
2492lemma prepares_delete_helper'':
2493  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace>"
2494  shows      "\<lbrace>P and K ((\<forall>x. cte_refs' cap x = {})
2495                          \<and> zobj_refs' cap = {p}
2496                          \<and> threadCapRefs cap = {})\<rbrace>
2497                 f \<lbrace>\<lambda>rv s. removeable' sl s cap\<rbrace>"
2498  apply (rule hoare_gen_asm)
2499  apply (rule hoare_strengthen_post [OF x])
2500  apply (clarsimp simp: removeable'_def)
2501  done
2502
2503lemma ctes_of_cteCaps_of_lift:
2504  "\<lbrakk> \<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> \<rbrakk>
2505     \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>"
2506  by (wp | simp add: cteCaps_of_def)+
2507
2508crunch ctes_of[wp]: finaliseCapTrue_standin, unbindNotification "\<lambda>s. P (ctes_of s)"
2509  (wp: crunch_wps getObject_inv loadObject_default_inv simp: crunch_simps ignore: getObject)
2510
2511lemma cteDeleteOne_cteCaps_of:
2512  "\<lbrace>\<lambda>s. (cte_wp_at' (\<lambda>cte. \<exists>final. finaliseCap (cteCap cte) final True \<noteq> fail) p s \<longrightarrow>
2513          P (cteCaps_of s(p \<mapsto> NullCap)))\<rbrace>
2514     cteDeleteOne p
2515   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>"
2516  apply (simp add: cteDeleteOne_def unless_def split_def)
2517  apply (rule hoare_seq_ext [OF _ getCTE_sp])
2518  apply (case_tac "\<forall>final. finaliseCap (cteCap cte) final True = fail")
2519   apply (simp add: finaliseCapTrue_standin_simple_def)
2520   apply wp
2521   apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def
2522                         finaliseCap_def isCap_simps)
2523   apply (drule_tac x=s in fun_cong)
2524   apply (simp add: return_def fail_def)
2525  apply (wp emptySlot_cteCaps_of)
2526    apply (simp add: cteCaps_of_def)
2527    apply (wp_once hoare_drop_imps)
2528    apply (wp isFinalCapability_inv getCTE_wp')+
2529  apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of)
2530  apply (auto simp: fun_upd_idem fun_upd_def[symmetric] o_def)
2531  done
2532
2533lemma cteDeleteOne_isFinal:
2534  "\<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s)\<rbrace>
2535     cteDeleteOne p
2536   \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace>"
2537  apply (wp cteDeleteOne_cteCaps_of)
2538  apply (clarsimp simp: isFinal_def sameObjectAs_def2)
2539  done
2540
2541lemmas setEndpoint_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF set_ep_ctes_of]
2542lemmas setNotification_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF set_ntfn_ctes_of]
2543lemmas setQueue_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF setQueue_ctes_of]
2544lemmas threadSet_cteCaps_of = ctes_of_cteCaps_of_lift [OF threadSet_ctes_of]
2545
2546crunch isFinal: suspend, prepareThreadDelete "\<lambda>s. isFinal cap slot (cteCaps_of s)"
2547  (ignore: setObject getObject threadSet
2548       wp: threadSet_cteCaps_of crunch_wps
2549     simp: crunch_simps unless_def o_def)
2550
2551lemma isThreadCap_threadCapRefs_tcbptr:
2552  "isThreadCap cap \<Longrightarrow> threadCapRefs cap = {capTCBPtr cap}"
2553  by (clarsimp simp: isCap_simps)
2554
2555lemma isArchObjectCap_Cap_capCap:
2556  "isArchObjectCap cap \<Longrightarrow> ArchObjectCap (capCap cap) = cap"
2557  by (clarsimp simp: isCap_simps)
2558
2559lemma cteDeleteOne_deletes[wp]:
2560  "\<lbrace>\<top>\<rbrace> cteDeleteOne p \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. cteCap c = NullCap) p s\<rbrace>"
2561  apply (subst tree_cte_cteCap_eq[unfolded o_def])
2562  apply (wp cteDeleteOne_cteCaps_of)
2563  apply clarsimp
2564  done
2565
2566crunch irq_node'[wp]: finaliseCap "\<lambda>s. P (irq_node' s)"
2567  (wp: mapM_x_wp crunch_wps getObject_inv loadObject_default_inv
2568       updateObject_default_inv setObject_ksInterrupt
2569       ignore: getObject setObject
2570       simp: crunch_simps unless_def o_def)
2571
2572lemma deletingIRQHandler_removeable':
2573  "\<lbrace>invs' and (\<lambda>s. isFinal (IRQHandlerCap irq) slot (cteCaps_of s))
2574          and K (cap = IRQHandlerCap irq)\<rbrace>
2575     deletingIRQHandler irq
2576   \<lbrace>\<lambda>rv s. removeable' slot s cap\<rbrace>"
2577  apply (rule hoare_gen_asm)
2578  apply (simp add: deletingIRQHandler_def getIRQSlot_def locateSlot_conv
2579                   getInterruptState_def getSlotCap_def)
2580  apply (simp add: removeable'_def tree_cte_cteCap_eq[unfolded o_def])
2581  apply (subst tree_cte_cteCap_eq[unfolded o_def])+
2582  apply (wp hoare_use_eq_irq_node' [OF cteDeleteOne_irq_node' cteDeleteOne_cteCaps_of]
2583            getCTE_wp')
2584  apply (clarsimp simp: cte_level_bits_def ucast_nat_def split: option.split_asm)
2585  done
2586
2587lemma finaliseCap_cte_refs:
2588  "\<lbrace>\<lambda>s. s \<turnstile>' cap\<rbrace>
2589     finaliseCap cap final flag
2590   \<lbrace>\<lambda>rv s. fst rv \<noteq> NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' cap\<rbrace>"
2591  apply (simp  add: finaliseCap_def Let_def getThreadCSpaceRoot
2592                    ARM_H.finaliseCap_def
2593             cong: if_cong split del: if_split)
2594  apply (rule hoare_pre)
2595   apply (wp | wpc | simp only: o_def)+
2596  apply (frule valid_capAligned)
2597  apply (cases cap, simp_all add: isCap_simps)
2598   apply (clarsimp simp: tcb_cte_cases_def word_count_from_top objBits_defs)
2599  apply clarsimp
2600  apply (rule ext, simp)
2601  apply (rule image_cong [OF _ refl])
2602  apply (fastforce simp: capAligned_def objBits_simps shiftL_nat)
2603  done
2604
2605lemma deletingIRQHandler_final:
2606  "\<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s)
2607             \<and> (\<forall>final. finaliseCap cap final True = fail)\<rbrace>
2608     deletingIRQHandler irq
2609   \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace>"
2610  apply (simp add: deletingIRQHandler_def isFinal_def getIRQSlot_def
2611                   getInterruptState_def locateSlot_conv getSlotCap_def)
2612  apply (wp cteDeleteOne_cteCaps_of getCTE_wp')
2613  apply (auto simp: sameObjectAs_def3)
2614  done
2615
2616declare suspend_unqueued [wp]
2617
2618lemma unbindNotification_valid_objs'_helper:
2619  "valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbBoundNotification_update (\<lambda>_. None) tcb) s "
2620  by (clarsimp simp: valid_bound_ntfn'_def valid_tcb'_def tcb_cte_cases_def
2621                  split: option.splits ntfn.splits)
2622
2623lemma unbindNotification_valid_objs'_helper':
2624  "valid_ntfn' tcb s \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) tcb) s "
2625  by (clarsimp simp: valid_bound_tcb'_def valid_ntfn'_def
2626                  split: option.splits ntfn.splits)
2627
2628lemma typ_at'_valid_tcb'_lift:
2629  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
2630  shows      "\<lbrace>\<lambda>s. valid_tcb' tcb s\<rbrace> f \<lbrace>\<lambda>rv s. valid_tcb' tcb s\<rbrace>"
2631  including no_pre
2632  apply (simp add: valid_tcb'_def)
2633  apply (case_tac "tcbState tcb", simp_all add: valid_tcb_state'_def split_def valid_bound_ntfn'_def)
2634         apply (wp hoare_vcg_const_Ball_lift typ_at_lifts[OF P]
2635               | case_tac "tcbBoundNotification tcb", simp_all)+
2636  done
2637
2638lemmas setNotification_valid_tcb' = typ_at'_valid_tcb'_lift [OF setNotification_typ_at']
2639
2640lemma unbindNotification_valid_objs'[wp]:
2641  "\<lbrace>valid_objs'\<rbrace>
2642     unbindNotification t
2643   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
2644  apply (simp add: unbindNotification_def)
2645  apply (rule hoare_pre)
2646  apply (wp threadSet_valid_objs' gbn_wp' set_ntfn_valid_objs' hoare_vcg_all_lift
2647            setNotification_valid_tcb' getNotification_wp
2648        | wpc | clarsimp simp: setBoundNotification_def unbindNotification_valid_objs'_helper)+
2649  apply (clarsimp elim!: obj_atE' simp: projectKOs)
2650  apply (rule valid_objsE', assumption+)
2651  apply (clarsimp simp: valid_obj'_def unbindNotification_valid_objs'_helper')
2652  done
2653
2654lemma unbindMaybeNotification_valid_objs'[wp]:
2655  "\<lbrace>valid_objs'\<rbrace>
2656     unbindMaybeNotification t
2657   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
2658  apply (simp add: unbindMaybeNotification_def)
2659  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
2660  apply (rule hoare_pre)
2661  apply (wp threadSet_valid_objs' gbn_wp' set_ntfn_valid_objs' hoare_vcg_all_lift
2662            setNotification_valid_tcb' getNotification_wp
2663        | wpc | clarsimp simp: setBoundNotification_def unbindNotification_valid_objs'_helper)+
2664  apply (clarsimp elim!: obj_atE' simp: projectKOs)
2665  apply (rule valid_objsE', assumption+)
2666  apply (clarsimp simp: valid_obj'_def unbindNotification_valid_objs'_helper')
2667  done
2668
2669lemma unbindNotification_sch_act_wf[wp]:
2670  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> unbindNotification t
2671  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
2672  apply (simp add: unbindNotification_def)
2673  apply (rule hoare_pre)
2674  apply (wp sbn_sch_act' | wpc | simp)+
2675  done
2676
2677lemma unbindMaybeNotification_sch_act_wf[wp]:
2678  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> unbindMaybeNotification t
2679  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
2680  apply (simp add: unbindMaybeNotification_def)
2681  apply (rule hoare_pre)
2682  apply (wp sbn_sch_act' | wpc | simp)+
2683  done
2684
2685lemma valid_cong:
2686  "\<lbrakk> \<And>s. P s = P' s; \<And>s. P' s \<Longrightarrow> f s = f' s;
2687        \<And>rv s' s. \<lbrakk> (rv, s') \<in> fst (f' s); P' s \<rbrakk> \<Longrightarrow> Q rv s' = Q' rv s' \<rbrakk>
2688    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> = \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>"
2689  by (clarsimp simp add: valid_def, blast)
2690
2691lemma sym_refs_ntfn_bound_eq: "sym_refs (state_refs_of' s)
2692    \<Longrightarrow> obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = Some t) x s
2693    = bound_tcb_at' (\<lambda>st. st = Some x) t s"
2694  apply (rule iffI)
2695   apply (drule (1) sym_refs_obj_atD')
2696   apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs
2697                         refs_of_rev')
2698  apply (drule(1) sym_refs_bound_tcb_atD')
2699  apply (clarsimp simp: obj_at'_def projectKOs ko_wp_at'_def refs_of_rev')
2700  done
2701
2702lemma unbindNotification_obj_at'_boundedness:
2703  "\<lbrace>obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = Some t \<or> ntfnBoundTCB ntfn = None) x
2704        and sym_refs o state_refs_of'\<rbrace>
2705     unbindNotification t
2706   \<lbrace>\<lambda>_ s. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) x s\<rbrace>"
2707  apply (simp add: unbindNotification_def)
2708  apply (rule hoare_seq_ext[OF _ gbn_sp'])
2709  apply (case_tac ntfnPtr)
2710   apply (wp | simp)+
2711   apply clarsimp
2712   apply (frule sym_refs_ntfn_bound_eq[where t=t and x=x])
2713   apply (clarsimp simp: obj_at'_def pred_tcb_at'_def)
2714  apply simp
2715  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
2716  apply (simp add: setBoundNotification_def threadSet_def setNotification_def)
2717  apply (wp obj_at_setObject2)
2718    apply (clarsimp simp: updateObject_default_def in_monad)
2719   apply wp
2720  apply (simp add: obj_at'_real_def cong: valid_cong)
2721  apply (wp setObject_ko_wp_at, (simp add: objBits_simps')+)
2722  apply clarsimp
2723  apply (frule sym_refs_ntfn_bound_eq[where t=t and x=x])
2724  apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs)
2725  done
2726
2727lemma unbindMaybeNotification_obj_at'_bound:
2728  "\<lbrace>\<top>\<rbrace>
2729     unbindMaybeNotification r
2730   \<lbrace>\<lambda>_ s. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r s\<rbrace>"
2731  apply (simp add: unbindMaybeNotification_def)
2732  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
2733  apply (rule hoare_pre)
2734   apply (wp obj_at_setObject2
2735        | wpc
2736        | simp add: setBoundNotification_def threadSet_def updateObject_default_def in_monad projectKOs)+
2737  apply (simp add: setNotification_def obj_at'_real_def cong: valid_cong)
2738   apply (wp setObject_ko_wp_at, (simp add: objBits_simps')+)
2739  apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs)
2740  done
2741
2742crunch isFinal[wp]: unbindNotification, unbindMaybeNotification "\<lambda>s. isFinal cap slot (cteCaps_of s)"
2743  (wp: sts_bound_tcb_at' threadSet_cteCaps_of crunch_wps getObject_inv
2744       loadObject_default_inv
2745   ignore: getObject setObject threadSet)
2746
2747crunch bound_tcb_at'[wp]: cancelSignal, cancelAllIPC "bound_tcb_at' P t"
2748  (wp: sts_bound_tcb_at' threadSet_cteCaps_of crunch_wps getObject_inv
2749       loadObject_default_inv
2750   ignore: getObject setObject threadSet)
2751
2752lemma finaliseCapTrue_standin_bound_tcb_at':
2753  "\<lbrace>\<lambda>s. bound_tcb_at' P t s \<and> (\<exists>tt b. cap = ReplyCap tt b) \<rbrace> finaliseCapTrue_standin cap final \<lbrace>\<lambda>_. bound_tcb_at' P t\<rbrace>"
2754  apply (case_tac cap, simp_all add:finaliseCapTrue_standin_def)
2755  apply (clarsimp simp: isNotificationCap_def)
2756  apply (wp, clarsimp)
2757  done
2758
2759lemma capDeleteOne_bound_tcb_at':
2760  "\<lbrace>bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap\<rbrace>
2761      cteDeleteOne callerCap \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>"
2762  apply (simp add: cteDeleteOne_def unless_def)
2763  apply (rule hoare_pre)
2764   apply (wp finaliseCapTrue_standin_bound_tcb_at' hoare_vcg_all_lift
2765            hoare_vcg_if_lift2 getCTE_cteCap_wp
2766        | wpc | simp | wp_once hoare_drop_imp)+
2767  apply (clarsimp simp:  cteCaps_of_def projectKOs isReplyCap_def cte_wp_at_ctes_of
2768                 split: option.splits)
2769  apply (case_tac "cteCap cte", simp_all)
2770  done
2771
2772lemma cancelIPC_bound_tcb_at'[wp]:
2773  "\<lbrace>bound_tcb_at' P tptr\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>"
2774  apply (simp add: cancelIPC_def Let_def)
2775  apply (rule hoare_seq_ext[OF _ gts_sp'])
2776  apply (case_tac "state", simp_all)
2777         defer 2
2778         apply (rule hoare_pre)
2779          apply ((wp sts_bound_tcb_at' getEndpoint_wp | wpc | simp)+)[8]
2780  apply (simp add: getThreadReplySlot_def locateSlot_conv liftM_def)
2781  apply (rule hoare_pre)
2782   apply (wp capDeleteOne_bound_tcb_at' getCTE_ctes_of)
2783   apply (rule_tac Q="\<lambda>_. bound_tcb_at' P tptr" in hoare_post_imp)
2784   apply (clarsimp simp: capHasProperty_def cte_wp_at_ctes_of)
2785   apply (wp threadSet_pred_tcb_no_state | simp)+
2786  done
2787
2788crunch bound_tcb_at'[wp]: suspend, prepareThreadDelete "bound_tcb_at' P t"
2789  (wp: sts_bound_tcb_at' cancelIPC_bound_tcb_at'
2790   ignore: getObject setObject threadSet)
2791
2792lemma unbindNotification_bound_tcb_at':
2793  "\<lbrace>\<lambda>_. True\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. bound_tcb_at' ((=) None) t\<rbrace>"
2794  apply (simp add: unbindNotification_def)
2795  apply (wp setBoundNotification_bound_tcb gbn_wp' | wpc | simp)+
2796  done
2797
2798lemma unbindMaybeNotification_bound_tcb_at':
2799  "\<lbrace>bound_tcb_at' (\<lambda>ntfn. ntfn = Some a \<or> ntfn = None) t
2800        and sym_refs o state_refs_of'\<rbrace>
2801     unbindMaybeNotification a
2802   \<lbrace>\<lambda>rv s. bound_tcb_at' ((=) None) t s\<rbrace>"
2803  apply (simp add: unbindMaybeNotification_def)
2804  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
2805  apply (case_tac "ntfnBoundTCB ntfn")
2806   apply (((wp threadSet_pred_tcb_at_state static_imp_wp hoare_drop_imps
2807            | clarsimp simp: setBoundNotification_def)+,
2808           drule (1) sym_refs_bound_tcb_atD',
2809           auto simp: tcb_ntfn_is_bound'_def obj_at'_def projectKOs ko_wp_at'_def
2810                      pred_tcb_at'_def ntfn_q_refs_of'_def
2811               split: ntfn.splits)[1])+
2812  done
2813
2814crunch valid_queues[wp]: unbindNotification, unbindMaybeNotification "Invariants_H.valid_queues"
2815  (wp: sbn_valid_queues)
2816
2817crunch weak_sch_act_wf[wp]: unbindNotification, unbindMaybeNotification "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"
2818
2819lemma unbindNotification_tcb_at'[wp]:
2820  "\<lbrace>tcb_at' t'\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>"
2821  apply (simp add: unbindNotification_def)
2822  apply (wp gbn_wp' | wpc | simp)+
2823  done
2824
2825lemma unbindMaybeNotification_tcb_at'[wp]:
2826  "\<lbrace>tcb_at' t'\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>"
2827  apply (simp add: unbindMaybeNotification_def)
2828  apply (wp gbn_wp' | wpc | simp)+
2829  done
2830
2831crunch cte_wp_at'[wp]: prepareThreadDelete "cte_wp_at' P p"
2832crunch valid_cap'[wp]: prepareThreadDelete "valid_cap' cap"
2833crunch invs[wp]: prepareThreadDelete "invs'"
2834
2835end
2836
2837lemma (in delete_one_conc_pre) finaliseCap_replaceable:
2838  "\<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s
2839       \<and> (final_matters' cap \<longrightarrow> (final = isFinal cap slot (cteCaps_of s)))
2840       \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
2841     finaliseCap cap final flag
2842   \<lbrace>\<lambda>rv s. (isNullCap (fst rv) \<and> removeable' slot s cap
2843                \<and> (snd rv \<noteq> NullCap \<longrightarrow> snd rv = cap \<and> cap_has_cleanup' cap
2844                                      \<and> isFinal cap slot (cteCaps_of s)))
2845        \<or>
2846          (isZombie (fst rv) \<and> snd rv = NullCap
2847            \<and> isFinal cap slot (cteCaps_of s)
2848            \<and> capClass cap = capClass (fst rv)
2849            \<and> capUntypedPtr (fst rv) = capUntypedPtr cap
2850            \<and> capBits (fst rv) = capBits cap
2851            \<and> capRange (fst rv) = capRange cap
2852            \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)
2853            \<and> (\<forall>p \<in> threadCapRefs cap. st_tcb_at' ((=) Inactive) p s
2854                     \<and> obj_at' (Not \<circ> tcbQueued) p s
2855                     \<and> bound_tcb_at' ((=) None) p s
2856                     \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr))))\<rbrace>"
2857  apply (simp add: finaliseCap_def Let_def getThreadCSpaceRoot
2858             cong: if_cong split del: if_split)
2859  apply (rule hoare_pre)
2860   apply (wp prepares_delete_helper'' [OF cancelAllIPC_unlive]
2861             prepares_delete_helper'' [OF cancelAllSignals_unlive]
2862             suspend_isFinal prepareThreadDelete_unqueued prepareThreadDelete_nonq
2863             prepareThreadDelete_inactive prepareThreadDelete_isFinal
2864             suspend_makes_inactive suspend_nonq
2865             deletingIRQHandler_removeable'
2866             deletingIRQHandler_final[where slot=slot ]
2867             unbindNotification_obj_at'_boundedness
2868             unbindMaybeNotification_obj_at'_bound
2869             getNotification_wp
2870             suspend_bound_tcb_at'
2871             unbindNotification_bound_tcb_at'
2872           | simp add: isZombie_Null isThreadCap_threadCapRefs_tcbptr
2873                       isArchObjectCap_Cap_capCap
2874           | (rule hoare_strengthen_post [OF arch_finaliseCap_removeable[where slot=slot]],
2875                  clarsimp simp: isCap_simps)
2876           | wpc)+
2877
2878  apply clarsimp
2879  apply (frule cte_wp_at_valid_objs_valid_cap', clarsimp+)
2880  apply (case_tac "cteCap cte",
2881         simp_all add: isCap_simps capRange_def cap_has_cleanup'_def
2882                       final_matters'_def objBits_simps
2883                       not_Final_removeable finaliseCap_def,
2884         simp_all add: removeable'_def)
2885     (* thread *)
2886     apply (frule capAligned_capUntypedPtr [OF valid_capAligned], simp)
2887     apply (clarsimp simp: valid_cap'_def)
2888     apply (drule valid_globals_cte_wpD'[rotated], clarsimp)
2889     apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
2890    apply (clarsimp simp: obj_at'_def | rule conjI)+
2891  done
2892
2893lemma cteDeleteOne_cte_wp_at_preserved:
2894  assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail"
2895  shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>
2896           cteDeleteOne ptr
2897         \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>"
2898  apply (simp add: tree_cte_cteCap_eq[unfolded o_def])
2899  apply (rule hoare_pre, wp cteDeleteOne_cteCaps_of)
2900  apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of x)
2901  done
2902
2903crunch ctes_of[wp]: cancelSignal "\<lambda>s. P (ctes_of s)"
2904  (simp: crunch_simps wp: crunch_wps)
2905
2906lemma cancelIPC_cteCaps_of:
2907  "\<lbrace>\<lambda>s. (\<forall>p. cte_wp_at' (\<lambda>cte. \<exists>final. finaliseCap (cteCap cte) final True \<noteq> fail) p s \<longrightarrow>
2908          P (cteCaps_of s(p \<mapsto> NullCap))) \<and>
2909     P (cteCaps_of s)\<rbrace>
2910     cancelIPC t
2911   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>"
2912  apply (simp add: cancelIPC_def Let_def capHasProperty_def
2913                   getThreadReplySlot_def locateSlot_conv)
2914  apply (rule hoare_pre)
2915   apply (wp cteDeleteOne_cteCaps_of getCTE_wp' | wpcw
2916        | simp add: cte_wp_at_ctes_of
2917        | wp_once hoare_drop_imps ctes_of_cteCaps_of_lift)+
2918          apply (wp hoare_convert_imp hoare_vcg_all_lift
2919                    threadSet_ctes_of threadSet_cteCaps_of
2920               | clarsimp)+
2921    apply (wp cteDeleteOne_cteCaps_of getCTE_wp' | wpcw | simp
2922       | wp_once hoare_drop_imps ctes_of_cteCaps_of_lift)+
2923  apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def)
2924  apply (drule_tac x="mdbNext (cteMDBNode x)" in spec)
2925  apply clarsimp
2926  apply (auto simp: o_def map_option_case fun_upd_def[symmetric])
2927  done
2928
2929lemma cancelIPC_cte_wp_at':
2930  assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail"
2931  shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>
2932           cancelIPC t
2933         \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>"
2934  apply (simp add: tree_cte_cteCap_eq[unfolded o_def])
2935  apply (rule hoare_pre, wp cancelIPC_cteCaps_of)
2936  apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of x)
2937  done
2938
2939crunch cte_wp_at'[wp]: tcbSchedDequeue "cte_wp_at' P p"
2940
2941lemma suspend_cte_wp_at':
2942  assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail"
2943  shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>
2944           suspend t
2945         \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>"
2946  apply (simp add: suspend_def unless_def)
2947  apply (rule hoare_pre)
2948   apply (wp threadSet_cte_wp_at' cancelIPC_cte_wp_at'
2949             | simp add: x)+
2950  done
2951
2952context begin interpretation Arch . (*FIXME: arch_split*)
2953
2954crunch cte_wp_at'[wp]: deleteASIDPool "cte_wp_at' P p"
2955  (simp: crunch_simps assertE_def
2956         wp: crunch_wps getObject_inv loadObject_default_inv
2957     ignore: getObject setObject)
2958
2959lemma deleteASID_cte_wp_at'[wp]:
2960  "\<lbrace>cte_wp_at' P p\<rbrace> deleteASID param_a param_b \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace>"
2961  apply (simp add: deleteASID_def invalidateHWASIDEntry_def invalidateASID_def
2962              cong: option.case_cong)
2963  apply (wp setObject_cte_wp_at'[where Q="\<top>"] getObject_inv
2964            loadObject_default_inv setVMRoot_cte_wp_at'
2965          | clarsimp simp: updateObject_default_def in_monad
2966                           projectKOs
2967          | rule equals0I
2968          | wpc)+
2969  done
2970
2971crunch cte_wp_at'[wp]: unmapPageTable, unmapPage, unbindNotification, finaliseCapTrue_standin
2972            "cte_wp_at' P p"
2973  (simp: crunch_simps wp: crunch_wps getObject_inv loadObject_default_inv
2974     ignore: getObject setObject)
2975
2976lemma arch_finaliseCap_cte_wp_at[wp]:
2977  "\<lbrace>cte_wp_at' P p\<rbrace> Arch.finaliseCap cap fin \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>"
2978  apply (simp add: ARM_H.finaliseCap_def)
2979  apply (safe ; wpsimp wp: unmapPage_cte_wp_at')
2980  done
2981
2982lemma deletingIRQHandler_cte_preserved:
2983  assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail"
2984  shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>
2985           deletingIRQHandler irq
2986         \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>"
2987  apply (simp add: deletingIRQHandler_def getSlotCap_def
2988                   getIRQSlot_def locateSlot_conv getInterruptState_def)
2989  apply (wp cteDeleteOne_cte_wp_at_preserved getCTE_wp'
2990              | simp add: x)+
2991  done
2992
2993lemma finaliseCap_equal_cap[wp]:
2994  "\<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>
2995     finaliseCap cap fin flag
2996   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>"
2997  apply (simp add: finaliseCap_def Let_def
2998             cong: if_cong split del: if_split)
2999  apply (rule hoare_pre)
3000   apply (wp suspend_cte_wp_at' deletingIRQHandler_cte_preserved
3001        | clarsimp simp: finaliseCap_def | wpc)+
3002  apply (case_tac cap)
3003  apply auto
3004  done
3005
3006lemma setThreadState_st_tcb_at_simplish':
3007  "simple' st \<Longrightarrow>
3008   \<lbrace>st_tcb_at' (P or simple') t\<rbrace>
3009     setThreadState st t'
3010   \<lbrace>\<lambda>rv. st_tcb_at' (P or simple') t\<rbrace>"
3011  apply (wp sts_st_tcb_at'_cases)
3012  apply clarsimp
3013  done
3014
3015lemmas setThreadState_st_tcb_at_simplish
3016    = setThreadState_st_tcb_at_simplish'[unfolded pred_disj_def]
3017
3018crunch st_tcb_at_simplish: cteDeleteOne
3019            "st_tcb_at' (\<lambda>st. P st \<or> simple' st) t"
3020  (wp: crunch_wps getObject_inv loadObject_default_inv threadSet_pred_tcb_no_state
3021   simp: crunch_simps unless_def ignore: getObject threadSet)
3022
3023lemma cteDeleteOne_st_tcb_at[wp]:
3024  assumes x[simp]: "\<And>st. simple' st \<longrightarrow> P st" shows
3025  "\<lbrace>st_tcb_at' P t\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>"
3026  apply (subgoal_tac "\<exists>Q. P = (Q or simple')")
3027   apply (clarsimp simp: pred_disj_def)
3028   apply (rule cteDeleteOne_st_tcb_at_simplish)
3029  apply (rule_tac x=P in exI)
3030  apply (auto intro!: ext)
3031  done
3032
3033lemma cteDeleteOne_reply_pred_tcb_at:
3034  "\<lbrace>\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t'. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t' False) slot s)\<rbrace>
3035    cteDeleteOne slot
3036   \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>"
3037  apply (simp add: cteDeleteOne_def unless_def isFinalCapability_def)
3038  apply (rule hoare_seq_ext [OF _ getCTE_sp])
3039  apply (rule hoare_assume_pre)
3040  apply (clarsimp simp: cte_wp_at_ctes_of when_def isCap_simps
3041                        Let_def finaliseCapTrue_standin_def)
3042  apply (intro impI conjI, (wp | simp)+)
3043  done
3044
3045crunch sch_act_simple[wp]: cteDeleteOne, unbindNotification sch_act_simple
3046  (wp: crunch_wps ssa_sch_act_simple sts_sch_act_simple getObject_inv
3047       loadObject_default_inv
3048   simp: crunch_simps unless_def
3049   rule: sch_act_simple_lift
3050   ignore: getObject)
3051
3052crunch valid_queues[wp]: setSchedulerAction "Invariants_H.valid_queues"
3053  (simp: Invariants_H.valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def)
3054
3055lemma rescheduleRequired_sch_act_not[wp]:
3056  "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_not t\<rbrace>"
3057  apply (simp add: rescheduleRequired_def setSchedulerAction_def)
3058  apply (wp hoare_post_taut | simp)+
3059  done
3060
3061crunch sch_act_not[wp]: cteDeleteOne "sch_act_not t"
3062  (simp: crunch_simps case_Null_If unless_def
3063   wp: crunch_wps getObject_inv loadObject_default_inv
3064   ignore: getObject)
3065
3066lemma cancelAllIPC_mapM_x_valid_queues:
3067  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)\<rbrace>
3068   mapM_x (\<lambda>t. do
3069                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
3070                 tcbSchedEnqueue t
3071               od) q
3072   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
3073  apply (rule_tac R="\<lambda>_ s. (\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s"
3074               in hoare_post_add)
3075  apply (rule hoare_pre)
3076  apply (rule mapM_x_wp')
3077  apply (rule hoare_name_pre_state)
3078  apply (wp hoare_vcg_const_Ball_lift
3079            tcbSchedEnqueue_valid_queues tcbSchedEnqueue_not_st
3080            sts_valid_queues sts_st_tcb_at'_cases setThreadState_not_st
3081       | simp
3082       | ((elim conjE)?, drule (1) bspec, clarsimp elim!: obj_at'_weakenE simp: valid_tcb_state'_def))+
3083  done
3084
3085lemma cancelAllIPC_mapM_x_ksSchedulerAction:
3086  "\<lbrace>sch_act_simple\<rbrace>
3087   mapM_x (\<lambda>t. do
3088                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
3089                 tcbSchedEnqueue t
3090               od) q
3091   \<lbrace>\<lambda>_. sch_act_simple\<rbrace>"
3092  apply (rule mapM_x_wp_inv)
3093  apply (wp tcbSchedEnqueue_nosch)
3094  done
3095
3096lemma cancelAllIPC_mapM_x_sch_act:
3097  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
3098   mapM_x (\<lambda>t. do
3099                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
3100                 tcbSchedEnqueue t
3101               od) q
3102   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
3103  apply (rule mapM_x_wp_inv)
3104  apply (wp)
3105  apply (clarsimp)
3106 done
3107
3108lemma cancelAllIPC_mapM_x_weak_sch_act:
3109  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
3110   mapM_x (\<lambda>t. do
3111                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
3112                 tcbSchedEnqueue t
3113               od) q
3114   \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
3115  apply (rule mapM_x_wp_inv)
3116  apply (wp)
3117  apply (clarsimp)
3118  done
3119
3120lemma cancelAllIPC_mapM_x_valid_objs':
3121  "\<lbrace>valid_objs'\<rbrace>
3122   mapM_x (\<lambda>t. do
3123                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
3124                 tcbSchedEnqueue t
3125               od) q
3126   \<lbrace>\<lambda>_. valid_objs'\<rbrace>"
3127  apply (wp mapM_x_wp' sts_valid_objs')
3128   apply (clarsimp simp: valid_tcb_state'_def)+
3129  done
3130
3131lemma cancelAllIPC_mapM_x_tcbDomain_obj_at':
3132  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
3133   mapM_x (\<lambda>t. do
3134                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
3135                 tcbSchedEnqueue t
3136               od) q
3137  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
3138apply (wp mapM_x_wp' tcbSchedEnqueue_not_st setThreadState_oa_queued | simp)+
3139done
3140
3141lemma rescheduleRequired_oa_queued':
3142  "\<lbrace>obj_at' (\<lambda>tcb. Q (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace>
3143    rescheduleRequired
3144   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. Q (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace>"
3145apply (simp add: rescheduleRequired_def)
3146apply (wp tcbSchedEnqueue_not_st
3147     | wpc
3148     | simp)+
3149done
3150
3151lemma cancelAllIPC_tcbDomain_obj_at':
3152  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
3153     cancelAllIPC epptr
3154   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
3155apply (simp add: cancelAllIPC_def)
3156apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift
3157          rescheduleRequired_oa_queued' cancelAllIPC_mapM_x_tcbDomain_obj_at' cancelAllIPC_mapM_x_ksSchedulerAction
3158          getEndpoint_wp
3159     | wpc
3160     | simp)+
3161done
3162
3163lemma cancelAllIPC_valid_queues[wp]:
3164  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
3165   cancelAllIPC ep_ptr
3166   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
3167  apply (simp add: cancelAllIPC_def ep'_Idle_case_helper)
3168  apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift
3169            cancelAllIPC_mapM_x_valid_queues cancelAllIPC_mapM_x_valid_objs' cancelAllIPC_mapM_x_weak_sch_act
3170            set_ep_valid_objs' getEndpoint_wp)
3171  apply (clarsimp simp: valid_ep'_def)
3172  apply (drule (1) ko_at_valid_objs')
3173  apply (auto simp: valid_obj'_def valid_ep'_def valid_tcb'_def projectKOs
3174             split: endpoint.splits
3175              elim: valid_objs_valid_tcbE)
3176  done
3177
3178lemma cancelAllSignals_tcbDomain_obj_at':
3179  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
3180     cancelAllSignals epptr
3181   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
3182apply (simp add: cancelAllSignals_def)
3183apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift
3184          rescheduleRequired_oa_queued' cancelAllIPC_mapM_x_tcbDomain_obj_at' cancelAllIPC_mapM_x_ksSchedulerAction
3185          getNotification_wp
3186     | wpc
3187     | simp)+
3188done
3189
3190lemma unbindNotification_tcbDomain_obj_at':
3191  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
3192     unbindNotification t
3193   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
3194  apply (simp add: unbindNotification_def)
3195  apply (wp setBoundNotification_oa_queued getNotification_wp gbn_wp' | wpc | simp)+
3196  done
3197
3198lemma unbindMaybeNotification_tcbDomain_obj_at':
3199  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
3200     unbindMaybeNotification r
3201   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
3202  apply (simp add: unbindMaybeNotification_def)
3203  apply (wp setBoundNotification_oa_queued getNotification_wp gbn_wp' | wpc | simp)+
3204  done
3205
3206lemma bindNotification_tcbDomain_obj_at':
3207  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
3208     bindNotification t ntfn
3209   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
3210  apply (simp add: bindNotification_def)
3211  apply (wp setBoundNotification_oa_queued getNotification_wp gbn_wp' | wpc | simp)+
3212  done
3213
3214lemma cancelAllSignals_valid_queues[wp]:
3215  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
3216   cancelAllSignals ntfn
3217   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
3218  apply (simp add: cancelAllSignals_def)
3219  apply (rule hoare_seq_ext [OF _ get_ntfn_sp'])
3220  apply (case_tac "ntfnObj ntfna", simp_all)
3221    apply (wp, simp)+
3222    apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift
3223              cancelAllIPC_mapM_x_valid_queues cancelAllIPC_mapM_x_valid_objs' cancelAllIPC_mapM_x_weak_sch_act
3224              set_ntfn_valid_objs'
3225          | simp)+
3226  apply (clarsimp simp: valid_ep'_def)
3227  apply (drule (1) ko_at_valid_objs')
3228  apply (auto simp: valid_obj'_def valid_ntfn'_def valid_tcb'_def projectKOs
3229             split: endpoint.splits
3230              elim: valid_objs_valid_tcbE)
3231  done
3232
3233lemma finaliseCap_True_valid_queues[wp]:
3234  "\<lbrace> Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
3235   finaliseCap cap final True
3236   \<lbrace>\<lambda>_. Invariants_H.valid_queues \<rbrace>"
3237  apply (simp add: finaliseCap_def Let_def)
3238  apply safe
3239    apply (wp irqs_masked_lift| simp | wpc)+
3240  done
3241
3242lemma finaliseCapTrue_standin_valid_queues[wp]:
3243  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
3244   finaliseCapTrue_standin cap final
3245   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>"
3246  apply (simp add: finaliseCapTrue_standin_def Let_def)
3247  apply (safe)
3248       apply (wp | clarsimp | wpc)+
3249  done
3250
3251
3252crunch valid_queues[wp]: isFinalCapability "Invariants_H.valid_queues"
3253  (simp: crunch_simps)
3254
3255crunch sch_act[wp]: isFinalCapability "\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
3256  (simp: crunch_simps)
3257
3258crunch weak_sch_act[wp]:
3259  isFinalCapability "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"
3260  (simp: crunch_simps)
3261
3262lemma cteDeleteOne_queues[wp]:
3263  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
3264   cteDeleteOne sl
3265   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>")
3266  apply (simp add: cteDeleteOne_def unless_def split_def)
3267  apply (wp isFinalCapability_inv getCTE_wp | rule hoare_drop_imps | simp)+
3268  apply (clarsimp simp: cte_wp_at'_def)
3269  done
3270
3271lemma valid_inQ_queues_lift:
3272  assumes tat: "\<And>d p tcb. \<lbrace>obj_at' (inQ d p) tcb\<rbrace> f \<lbrace>\<lambda>_. obj_at' (inQ d p) tcb\<rbrace>"
3273  and     prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
3274  shows   "\<lbrace>valid_inQ_queues\<rbrace> f \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>"
3275  proof -
3276    show ?thesis
3277      apply (clarsimp simp: valid_def valid_inQ_queues_def)
3278      apply safe
3279       apply (rule use_valid [OF _ tat], assumption)
3280       apply (drule spec, drule spec, erule conjE, erule bspec)
3281       apply (rule ccontr)
3282       apply (erule notE[rotated], erule(1) use_valid [OF _ prq])
3283      apply (erule use_valid [OF _ prq])
3284      apply simp
3285      done
3286  qed
3287
3288lemma emptySlot_valid_inQ_queues [wp]:
3289  "\<lbrace>valid_inQ_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>"
3290  unfolding emptySlot_def
3291  by (wp opt_return_pres_lift | wpcw | wp valid_inQ_queues_lift | simp)+
3292
3293crunch valid_inQ_queues[wp]: emptySlot valid_inQ_queues
3294  (simp: crunch_simps ignore: updateObject setObject)
3295
3296lemma cancelAllIPC_mapM_x_valid_inQ_queues:
3297  "\<lbrace>valid_inQ_queues\<rbrace>
3298   mapM_x (\<lambda>t. do
3299                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
3300                 tcbSchedEnqueue t
3301               od) q
3302   \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>"
3303  apply (rule mapM_x_wp_inv)
3304  apply (wp sts_valid_queues [where st="Structures_H.thread_state.Restart", simplified]
3305            setThreadState_st_tcb)
3306   done
3307
3308lemma cancelAllIPC_valid_inQ_queues[wp]:
3309  "\<lbrace>valid_inQ_queues\<rbrace>
3310   cancelAllIPC ep_ptr
3311   \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>"
3312  apply (simp add: cancelAllIPC_def ep'_Idle_case_helper)
3313  apply (wp cancelAllIPC_mapM_x_valid_inQ_queues)
3314  apply (wp hoare_conjI hoare_drop_imp | simp)+
3315  done
3316
3317lemma cancelAllSignals_valid_inQ_queues[wp]:
3318  "\<lbrace>valid_inQ_queues\<rbrace>
3319   cancelAllSignals ntfn
3320   \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>"
3321  apply (simp add: cancelAllSignals_def)
3322  apply (rule hoare_seq_ext [OF _ get_ntfn_sp'])
3323  apply (case_tac "ntfnObj ntfna", simp_all)
3324    apply (wp, simp)+
3325    apply (wp cancelAllIPC_mapM_x_valid_inQ_queues)+
3326   apply (simp)
3327  done
3328
3329crunch valid_inQ_queues[wp]: unbindNotification, unbindMaybeNotification "valid_inQ_queues"
3330
3331lemma finaliseCapTrue_standin_valid_inQ_queues[wp]:
3332  "\<lbrace>valid_inQ_queues\<rbrace>
3333   finaliseCapTrue_standin cap final
3334   \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>"
3335  apply (simp add: finaliseCapTrue_standin_def Let_def)
3336  apply (safe)
3337       apply (wp | clarsimp | wpc)+
3338  done
3339
3340crunch valid_inQ_queues[wp]: isFinalCapability valid_inQ_queues
3341  (simp: crunch_simps)
3342
3343lemma cteDeleteOne_valid_inQ_queues[wp]:
3344  "\<lbrace>valid_inQ_queues\<rbrace>
3345   cteDeleteOne sl
3346   \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>"
3347  apply (simp add: cteDeleteOne_def unless_def)
3348  apply (wpsimp wp: hoare_drop_imp hoare_vcg_all_lift)
3349  done
3350
3351crunch ksCurDomain[wp]: cteDeleteOne "\<lambda>s. P (ksCurDomain s)"
3352  (wp: crunch_wps simp: crunch_simps unless_def)
3353
3354lemma cteDeleteOne_tcbDomain_obj_at':
3355  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
3356  apply (simp add: cteDeleteOne_def unless_def split_def)
3357  apply (wp emptySlot_tcbDomain cancelAllIPC_tcbDomain_obj_at' cancelAllSignals_tcbDomain_obj_at'
3358          isFinalCapability_inv getCTE_wp unbindNotification_tcbDomain_obj_at'
3359          unbindMaybeNotification_tcbDomain_obj_at'
3360     | rule hoare_drop_imp
3361     | simp add: finaliseCapTrue_standin_def Let_def
3362            split del: if_split
3363     | wpc)+
3364  apply (clarsimp simp: cte_wp_at'_def)
3365  done
3366
3367end
3368
3369global_interpretation delete_one_conc_pre
3370  by (unfold_locales, wp) (wp cteDeleteOne_tcbDomain_obj_at' cteDeleteOne_typ_at' cteDeleteOne_reply_pred_tcb_at | simp)+
3371
3372lemma cteDeleteOne_invs[wp]:
3373  "\<lbrace>invs'\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv. invs'\<rbrace>"
3374  apply (simp add: cteDeleteOne_def unless_def
3375                   split_def finaliseCapTrue_standin_simple_def)
3376  apply wp
3377    apply (rule hoare_strengthen_post)
3378     apply (rule hoare_vcg_conj_lift)
3379      apply (rule finaliseCap_True_invs)
3380     apply (rule hoare_vcg_conj_lift)
3381      apply (rule finaliseCap_replaceable[where slot=ptr])
3382     apply (rule hoare_vcg_conj_lift)
3383      apply (rule finaliseCap_cte_refs)
3384     apply (rule finaliseCap_equal_cap[where sl=ptr])
3385    apply (clarsimp simp: cte_wp_at_ctes_of)
3386    apply (erule disjE)
3387     apply simp
3388    apply (clarsimp dest!: isCapDs simp: capRemovable_def)
3389    apply (clarsimp simp: removeable'_def fun_eq_iff[where f="cte_refs' cap" for cap]
3390                     del: disjCI)
3391    apply (rule disjI2)
3392    apply (rule conjI)
3393     subgoal by auto
3394    subgoal by (auto dest!: isCapDs simp: pred_tcb_at'_def obj_at'_def projectKOs
3395                                     ko_wp_at'_def)
3396   apply (wp isFinalCapability_inv getCTE_wp' static_imp_wp
3397        | wp_once isFinal[where x=ptr])+
3398  apply (fastforce simp: cte_wp_at_ctes_of)
3399  done
3400
3401global_interpretation delete_one_conc_fr: delete_one_conc
3402  by unfold_locales wp
3403
3404declare cteDeleteOne_invs[wp]
3405
3406lemma deletingIRQHandler_invs' [wp]:
3407  "\<lbrace>invs'\<rbrace> deletingIRQHandler i \<lbrace>\<lambda>_. invs'\<rbrace>"
3408  apply (simp add: deletingIRQHandler_def getSlotCap_def
3409                   getIRQSlot_def locateSlot_conv getInterruptState_def)
3410  apply (wp getCTE_wp')
3411  apply simp
3412  done
3413
3414crunch tcb_at'[wp]: unbindNotification, unbindMaybeNotification "tcb_at' t"
3415
3416lemma finaliseCap_invs:
3417  "\<lbrace>invs' and sch_act_simple and valid_cap' cap
3418         and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>
3419     finaliseCap cap fin flag
3420   \<lbrace>\<lambda>rv. invs'\<rbrace>"
3421  apply (simp add: finaliseCap_def Let_def
3422             cong: if_cong split del: if_split)
3423  apply (rule hoare_pre)
3424   apply (wp hoare_drop_imps hoare_vcg_all_lift | simp only: o_def | wpc)+
3425
3426  apply clarsimp
3427  apply (intro conjI impI)
3428    apply (clarsimp dest!: isCapDs simp: valid_cap'_def)
3429   apply (drule invs_valid_global', drule(1) valid_globals_cte_wpD')
3430   apply (drule valid_capAligned, drule capAligned_capUntypedPtr)
3431    apply (clarsimp dest!: isCapDs)
3432   apply (clarsimp dest!: isCapDs)
3433  apply (clarsimp dest!: isCapDs)
3434  done
3435
3436lemma finaliseCap_zombie_cap[wp]:
3437  "\<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace>
3438     finaliseCap cap fin flag
3439   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace>"
3440  apply (simp add: finaliseCap_def Let_def
3441             cong: if_cong split del: if_split)
3442  apply (rule hoare_pre)
3443   apply (wp suspend_cte_wp_at'
3444             deletingIRQHandler_cte_preserved
3445                 | clarsimp simp: finaliseCap_def isCap_simps | wpc)+
3446  done
3447
3448lemma finaliseCap_zombie_cap':
3449  "\<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace>
3450     finaliseCap cap fin flag
3451   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) sl\<rbrace>"
3452  apply (rule hoare_strengthen_post)
3453   apply (rule finaliseCap_zombie_cap)
3454  apply (clarsimp simp: cte_wp_at_ctes_of)
3455  done
3456
3457lemma finaliseCap_cte_cap_wp_to[wp]:
3458  "\<lbrace>ex_cte_cap_wp_to' P sl\<rbrace> finaliseCap cap fin flag \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P sl\<rbrace>"
3459  apply (simp add: ex_cte_cap_to'_def)
3460  apply (rule hoare_pre, rule hoare_use_eq_irq_node' [OF finaliseCap_irq_node'])
3461   apply (simp add: finaliseCap_def Let_def
3462              cong: if_cong split del: if_split)
3463   apply (wp suspend_cte_wp_at'
3464             deletingIRQHandler_cte_preserved
3465             hoare_vcg_ex_lift
3466                 | clarsimp simp: finaliseCap_def isCap_simps
3467                 | rule conjI
3468                 | wpc)+
3469  apply fastforce
3470  done
3471
3472crunch valid_cap'[wp]: unbindNotification "valid_cap' cap"
3473
3474lemma finaliseCap_valid_cap[wp]:
3475  "\<lbrace>valid_cap' cap\<rbrace> finaliseCap cap final flag \<lbrace>\<lambda>rv. valid_cap' (fst rv)\<rbrace>"
3476  apply (simp add: finaliseCap_def Let_def
3477                   getThreadCSpaceRoot
3478                   ARM_H.finaliseCap_def
3479             cong: if_cong split del: if_split)
3480  apply (rule hoare_pre)
3481   apply (wp | simp only: valid_NullCap o_def fst_conv | wpc)+
3482  apply simp
3483  apply (intro conjI impI)
3484   apply (clarsimp simp: valid_cap'_def isCap_simps capAligned_def
3485                         objBits_simps shiftL_nat)+
3486  done
3487
3488
3489context begin interpretation Arch . (*FIXME: arch_split*)
3490
3491crunch nosch[wp]: "Arch.finaliseCap" "\<lambda>s. P (ksSchedulerAction s)"
3492  (wp: crunch_wps getObject_inv simp: loadObject_default_def updateObject_default_def
3493   ignore: getObject)
3494
3495crunch sch_act_simple[wp]: finaliseCap sch_act_simple
3496  (simp: crunch_simps
3497   rule: sch_act_simple_lift
3498   wp: getObject_inv loadObject_default_inv crunch_wps
3499   ignore: getObject)
3500
3501end
3502
3503
3504lemma interrupt_cap_null_or_ntfn:
3505  "invs s
3506    \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s"
3507  apply (frule invs_valid_irq_node)
3508  apply (clarsimp simp: valid_irq_node_def)
3509  apply (drule_tac x=irq in spec)
3510  apply (drule cte_at_0)
3511  apply (clarsimp simp: cte_wp_at_caps_of_state)
3512  apply (drule caps_of_state_cteD)
3513  apply (frule if_unsafe_then_capD, clarsimp+)
3514  apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state)
3515  apply (frule cte_refs_obj_refs_elem, erule disjE)
3516   apply (clarsimp | drule caps_of_state_cteD valid_global_refsD[rotated]
3517     | rule irq_node_global_refs[where irq=irq])+
3518   apply (simp add: cap_range_def)
3519  apply (clarsimp simp: appropriate_cte_cap_def
3520                 split: cap.split_asm)
3521  done
3522
3523lemma (in delete_one) deleting_irq_corres:
3524  "corres dc (einvs) (invs')
3525          (deleting_irq_handler irq) (deletingIRQHandler irq)"
3526  apply (simp add: deleting_irq_handler_def deletingIRQHandler_def)
3527  apply (rule corres_guard_imp)
3528    apply (rule corres_split [OF _ get_irq_slot_corres])
3529      apply simp
3530      apply (rule_tac P'="cte_at' (cte_map slot)" in corres_symb_exec_r_conj)
3531         apply (rule_tac F="isNotificationCap rv \<or> rv = capability.NullCap"
3532             and P="cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot
3533                 and einvs"
3534             and P'="invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv)
3535                 (cte_map slot)" in corres_req)
3536          apply (clarsimp simp: cte_wp_at_caps_of_state state_relation_def)
3537          apply (drule caps_of_state_cteD)
3538          apply (drule(1) pspace_relation_cte_wp_at, clarsimp+)
3539          apply (auto simp: cte_wp_at_ctes_of is_cap_simps isCap_simps)[1]
3540         apply simp
3541         apply (rule corres_guard_imp, rule delete_one_corres[unfolded dc_def])
3542          apply (auto simp: cte_wp_at_caps_of_state is_cap_simps can_fast_finalise_def)[1]
3543         apply (clarsimp simp: cte_wp_at_ctes_of)
3544        apply (wp getCTE_wp' | simp add: getSlotCap_def)+
3545     apply (wp | simp add: get_irq_slot_def getIRQSlot_def
3546                           locateSlot_conv getInterruptState_def)+
3547   apply (clarsimp simp: ex_cte_cap_wp_to_def interrupt_cap_null_or_ntfn)
3548  apply (clarsimp simp: cte_wp_at_ctes_of)
3549  done
3550
3551context begin interpretation Arch . (*FIXME: arch_split*)
3552
3553lemma arch_finalise_cap_corres:
3554  "\<lbrakk> final_matters' (ArchObjectCap cap') \<Longrightarrow> final = final'; acap_relation cap cap' \<rbrakk>
3555     \<Longrightarrow> corres (\<lambda>r r'. cap_relation (fst r) (fst r') \<and> cap_relation (snd r) (snd r'))
3556           (\<lambda>s. invs s \<and> valid_etcbs s
3557                       \<and> s \<turnstile> cap.ArchObjectCap cap
3558                       \<and> (final_matters (cap.ArchObjectCap cap)
3559                            \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap cap) s)
3560                       \<and> cte_wp_at ((=) (cap.ArchObjectCap cap)) sl s)
3561           (\<lambda>s. invs' s \<and> s \<turnstile>' ArchObjectCap cap' \<and>
3562                 (final_matters' (ArchObjectCap cap') \<longrightarrow>
3563                      final' = isFinal (ArchObjectCap cap') (cte_map sl) (cteCaps_of s)))
3564           (arch_finalise_cap cap final) (Arch.finaliseCap cap' final')"
3565  apply (cases cap;
3566        clarsimp simp: arch_finalise_cap_def ARM_H.finaliseCap_def
3567                       final_matters'_def case_bool_If liftM_def[symmetric]
3568                       isASIDPoolCap_def isPageCap_def isPageDirectoryCap_def
3569                       isPageTableCap_def
3570                       o_def dc_def[symmetric]
3571                split: option.split)
3572     apply (rule corres_guard_imp, rule delete_asid_pool_corres)
3573      apply (clarsimp simp: valid_cap_def mask_def)
3574     apply (clarsimp simp: valid_cap'_def)
3575     apply auto[1]
3576    apply (rule corres_guard_imp, rule unmap_page_corres)
3577      apply simp
3578     apply (clarsimp simp: valid_cap_def valid_unmap_def)
3579     apply (auto simp: vmsz_aligned_def pbfs_atleast_pageBits mask_def
3580                 elim: is_aligned_weaken invs_valid_asid_map)[2]
3581   apply (rule corres_guard_imp, rule unmap_page_table_corres)
3582    apply (auto simp: valid_cap_def valid_cap'_def mask_def
3583               elim!: is_aligned_weaken invs_valid_asid_map)[2]
3584  apply (rule corres_guard_imp, rule delete_asid_corres)
3585   apply (auto elim!: invs_valid_asid_map simp: mask_def valid_cap_def)[2]
3586  done
3587
3588lemma ntfnBoundTCB_update_ntfnObj_inv[simp]:
3589  "ntfnObj (ntfnBoundTCB_update f ntfn) = ntfnObj ntfn"
3590  by auto
3591
3592lemma unbind_notification_corres:
3593  "corres dc
3594      (invs and tcb_at t)
3595      (invs' and tcb_at' t)
3596      (unbind_notification t)
3597      (unbindNotification t)"
3598  apply (simp add: unbind_notification_def unbindNotification_def)
3599  apply (rule corres_guard_imp)
3600    apply (rule corres_split[OF _ gbn_corres])
3601      apply (rule corres_option_split)
3602        apply simp
3603       apply (rule corres_return_trivial)
3604      apply (rule corres_split[OF _ get_ntfn_corres])
3605        apply clarsimp
3606        apply (rule corres_split[OF _ set_ntfn_corres])
3607           apply (rule sbn_corres)
3608          apply (clarsimp simp: ntfn_relation_def split:Structures_A.ntfn.splits)
3609         apply (wp gbn_wp' gbn_wp)+
3610   apply (clarsimp elim!: obj_at_valid_objsE
3611                   dest!: bound_tcb_at_state_refs_ofD invs_valid_objs
3612                    simp: valid_obj_def is_tcb tcb_ntfn_is_bound_def
3613                          valid_tcb_def valid_bound_ntfn_def
3614                   split: option.splits)
3615  apply (clarsimp dest!: obj_at_valid_objs' bound_tcb_at_state_refs_ofD' invs_valid_objs'
3616                   simp: projectKOs valid_obj'_def valid_tcb'_def valid_bound_ntfn'_def
3617                         tcb_ntfn_is_bound'_def
3618                  split: option.splits)
3619  done
3620
3621lemma unbind_maybe_notification_corres:
3622  "corres dc
3623      (invs and ntfn_at ntfnptr) (invs' and ntfn_at' ntfnptr)
3624      (unbind_maybe_notification ntfnptr)
3625      (unbindMaybeNotification ntfnptr)"
3626  apply (simp add: unbind_maybe_notification_def unbindMaybeNotification_def)
3627  apply (rule corres_guard_imp)
3628    apply (rule corres_split[OF _ get_ntfn_corres])
3629      apply (rule corres_option_split)
3630        apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
3631       apply (rule corres_return_trivial)
3632      apply simp
3633      apply (rule corres_split[OF _ set_ntfn_corres])
3634         apply (rule sbn_corres)
3635        apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
3636       apply (wp get_simple_ko_wp getNotification_wp)+
3637   apply (clarsimp elim!: obj_at_valid_objsE
3638                   dest!: bound_tcb_at_state_refs_ofD invs_valid_objs
3639                    simp: valid_obj_def is_tcb tcb_ntfn_is_bound_def
3640                          valid_tcb_def valid_bound_ntfn_def valid_ntfn_def
3641                   split: option.splits)
3642  apply (clarsimp dest!: obj_at_valid_objs' bound_tcb_at_state_refs_ofD' invs_valid_objs'
3643                   simp: projectKOs valid_obj'_def valid_tcb'_def valid_bound_ntfn'_def
3644                         tcb_ntfn_is_bound'_def valid_ntfn'_def
3645                  split: option.splits)
3646  done
3647
3648lemma fast_finalise_corres:
3649  "\<lbrakk> final_matters' cap' \<longrightarrow> final = final'; cap_relation cap cap';
3650     can_fast_finalise cap \<rbrakk>
3651   \<Longrightarrow> corres dc
3652           (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap
3653                       \<and> cte_wp_at ((=) cap) sl s)
3654           (\<lambda>s. invs' s \<and> s \<turnstile>' cap')
3655           (fast_finalise cap final)
3656           (do
3657               p \<leftarrow> finaliseCap cap' final' True;
3658               assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = NullCap)
3659            od)"
3660  apply (cases cap, simp_all add: finaliseCap_def isCap_simps
3661                                  corres_liftM2_simp[unfolded liftM_def]
3662                                  o_def dc_def[symmetric] when_def
3663                                  can_fast_finalise_def capRemovable_def
3664                       split del: if_split cong: if_cong)
3665   apply (clarsimp simp: final_matters'_def)
3666   apply (rule corres_guard_imp)
3667     apply (rule corres_rel_imp)
3668      apply (rule ep_cancel_corres)
3669     apply simp
3670    apply (simp add: valid_cap_def)
3671   apply (simp add: valid_cap'_def)
3672  apply (clarsimp simp: final_matters'_def)
3673  apply (rule corres_guard_imp)
3674    apply (rule corres_split[OF _ unbind_maybe_notification_corres])
3675         apply (rule ntfn_cancel_corres)
3676       apply (wp abs_typ_at_lifts unbind_maybe_notification_invs typ_at_lifts hoare_drop_imps getNotification_wp
3677            | wpc)+
3678   apply (clarsimp simp: valid_cap_def)
3679  apply (clarsimp simp: valid_cap'_def projectKOs valid_obj'_def
3680                 dest!: invs_valid_objs' obj_at_valid_objs' )
3681  done
3682
3683lemma cap_delete_one_corres:
3684  "corres dc (einvs and cte_wp_at can_fast_finalise ptr)
3685        (invs' and cte_at' (cte_map ptr))
3686        (cap_delete_one ptr) (cteDeleteOne (cte_map ptr))"
3687  apply (simp add: cap_delete_one_def cteDeleteOne_def'
3688                   unless_def when_def)
3689  apply (rule corres_guard_imp)
3690    apply (rule corres_split [OF _ get_cap_corres])
3691      apply (rule_tac F="can_fast_finalise cap" in corres_gen_asm)
3692      apply (rule corres_if)
3693        apply fastforce
3694       apply (rule corres_split [OF _ final_cap_corres[where ptr=ptr]])
3695         apply (simp add: split_def bind_assoc [THEN sym])
3696         apply (rule corres_split [OF _ fast_finalise_corres[where sl=ptr]])
3697              apply (rule empty_slot_corres)
3698             apply simp+
3699          apply (wp hoare_drop_imps)+
3700        apply (wp isFinalCapability_inv | wp_once isFinal[where x="cte_map ptr"])+
3701      apply (rule corres_trivial, simp)
3702     apply (wp get_cap_wp getCTE_wp)+
3703   apply (clarsimp simp: cte_wp_at_caps_of_state can_fast_finalise_Null
3704                  elim!: caps_of_state_valid_cap)
3705  apply (clarsimp simp: cte_wp_at_ctes_of)
3706  apply fastforce
3707  done
3708end
3709(* FIXME: strengthen locale instead *)
3710
3711global_interpretation delete_one
3712  apply unfold_locales
3713  apply (rule corres_guard_imp)
3714    apply (rule cap_delete_one_corres)
3715   apply auto
3716  done
3717
3718lemma finalise_cap_corres:
3719  "\<lbrakk> final_matters' cap' \<Longrightarrow> final = final'; cap_relation cap cap';
3720          flag \<longrightarrow> can_fast_finalise cap \<rbrakk>
3721     \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y))
3722           (\<lambda>s. einvs s \<and> s \<turnstile> cap \<and> (final_matters cap \<longrightarrow> final = is_final_cap' cap s)
3723                       \<and> cte_wp_at ((=) cap) sl s)
3724           (\<lambda>s. invs' s \<and> s \<turnstile>' cap' \<and>
3725                 (final_matters' cap' \<longrightarrow>
3726                      final' = isFinal cap' (cte_map sl) (cteCaps_of s)))
3727           (finalise_cap cap final) (finaliseCap cap' final' flag)"
3728  apply (cases cap, simp_all add: finaliseCap_def isCap_simps
3729                                  corres_liftM2_simp[unfolded liftM_def]
3730                                  o_def dc_def[symmetric] when_def
3731                                  can_fast_finalise_def
3732                       split del: if_split cong: if_cong)
3733        apply (clarsimp simp: final_matters'_def)
3734        apply (rule corres_guard_imp)
3735          apply (rule ep_cancel_corres)
3736         apply (simp add: valid_cap_def)
3737        apply (simp add: valid_cap'_def)
3738       apply (clarsimp simp add: final_matters'_def)
3739       apply (rule corres_guard_imp)
3740         apply (rule corres_split[OF _ unbind_maybe_notification_corres])
3741           apply (rule ntfn_cancel_corres)
3742          apply (wp abs_typ_at_lifts unbind_maybe_notification_invs typ_at_lifts hoare_drop_imps hoare_vcg_all_lift | wpc)+
3743        apply (clarsimp simp: valid_cap_def)
3744       apply (clarsimp simp: valid_cap'_def)
3745      apply (fastforce simp: final_matters'_def shiftL_nat zbits_map_def)
3746     apply (clarsimp simp add: final_matters'_def getThreadCSpaceRoot
3747                               liftM_def[symmetric] o_def zbits_map_def
3748                               dc_def[symmetric])
3749     apply (rule corres_guard_imp)
3750       apply (rule corres_split[OF _ unbind_notification_corres])
3751         apply (rule corres_split[OF _ suspend_corres])
3752            apply (clarsimp simp: liftM_def[symmetric] o_def dc_def[symmetric] zbits_map_def)
3753          apply (rule prepareThreadDelete_corres)
3754        apply (wp unbind_notification_invs unbind_notification_simple_sched_action)+
3755      apply (simp add: valid_cap_def)
3756     apply (simp add: valid_cap'_def)
3757    apply (simp add: final_matters'_def liftM_def[symmetric]
3758                     o_def dc_def[symmetric])
3759    apply (intro impI, rule corres_guard_imp)
3760      apply (rule deleting_irq_corres)
3761     apply simp
3762    apply simp
3763   apply (clarsimp simp: final_matters'_def)
3764   apply (rule_tac F="False" in corres_req)
3765    apply clarsimp
3766    apply (frule zombies_finalD, (clarsimp simp: is_cap_simps)+)
3767    apply (clarsimp simp: cte_wp_at_caps_of_state)
3768   apply simp
3769  apply (clarsimp split del: if_split simp: o_def)
3770  apply (rule corres_guard_imp [OF arch_finalise_cap_corres], (fastforce simp: valid_sched_def)+)
3771  done
3772context begin interpretation Arch . (*FIXME: arch_split*)
3773lemma arch_recycleCap_improve_cases:
3774   "\<lbrakk> \<not> isPageCap cap; \<not> isPageTableCap cap; \<not> isPageDirectoryCap cap;
3775         \<not> isASIDControlCap cap \<rbrakk> \<Longrightarrow> (if isASIDPoolCap cap then v else undefined) = v"
3776  by (cases cap, simp_all add: isCap_simps)
3777
3778crunch queues[wp]: copyGlobalMappings "Invariants_H.valid_queues"
3779  (wp: crunch_wps ignore: storePDE getObject)
3780
3781crunch queues'[wp]: copyGlobalMappings "Invariants_H.valid_queues'"
3782  (wp: crunch_wps ignore: storePDE getObject)
3783
3784crunch ifunsafe'[wp]: copyGlobalMappings "if_unsafe_then_cap'"
3785  (wp: crunch_wps ignore: storePDE getObject)
3786
3787lemma copyGlobalMappings_pde_mappings2':
3788  "\<lbrace>valid_pde_mappings' and valid_arch_state'
3789            and K (is_aligned pd pdBits)\<rbrace>
3790      copyGlobalMappings pd \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
3791  apply (wp copyGlobalMappings_pde_mappings')
3792  apply (clarsimp simp: valid_arch_state'_def page_directory_at'_def)
3793  done
3794
3795crunch pred_tcb_at'[wp]: copyGlobalMappings "pred_tcb_at' proj P t"
3796  (wp: crunch_wps ignore: storePDE getObject)
3797
3798crunch vms'[wp]: copyGlobalMappings "valid_machine_state'"
3799  (wp: crunch_wps ignore: storePDE getObject)
3800
3801crunch ct_not_inQ[wp]: copyGlobalMappings "ct_not_inQ"
3802  (wp: crunch_wps ignore: storePDE getObject)
3803
3804crunch tcb_in_cur_domain'[wp]: copyGlobalMappings "tcb_in_cur_domain' t"
3805  (wp: crunch_wps ignore: getObject)
3806
3807crunch ct__in_cur_domain'[wp]: copyGlobalMappings ct_idle_or_in_cur_domain'
3808  (wp: crunch_wps ignore: getObject)
3809
3810crunch gsUntypedZeroRanges[wp]: copyGlobalMappings "\<lambda>s. P (gsUntypedZeroRanges s)"
3811  (wp: crunch_wps ignore: getObject)
3812
3813lemma copyGlobalMappings_invs'[wp]:
3814  "\<lbrace>invs' and K (is_aligned pd pdBits)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv. invs'\<rbrace>"
3815  apply (simp add: invs'_def valid_state'_def valid_pspace'_def)
3816  apply (rule hoare_pre)
3817   apply (wp valid_irq_node_lift_asm valid_global_refs_lift' sch_act_wf_lift
3818             valid_irq_handlers_lift'' cur_tcb_lift typ_at_lifts irqs_masked_lift
3819             copyGlobalMappings_pde_mappings2'
3820             untyped_ranges_zero_lift
3821        | clarsimp simp: cteCaps_of_def o_def)+
3822  done
3823
3824lemma dmo'_bind_return:
3825  "\<lbrace>P\<rbrace> doMachineOp f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow>
3826   \<lbrace>P\<rbrace> doMachineOp (do _ \<leftarrow> f; return x od) \<lbrace>\<lambda>_. Q\<rbrace>"
3827  by (clarsimp simp: doMachineOp_def bind_def return_def valid_def select_f_def
3828                     split_def)
3829
3830lemma ct_in_current_domain_ArchState_update[simp]:
3831  "ct_idle_or_in_cur_domain' (s\<lparr>ksArchState := v\<rparr>) = ct_idle_or_in_cur_domain' s"
3832  by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
3833
3834lemma threadSet_ct_idle_or_in_cur_domain':
3835  "\<lbrace>ct_idle_or_in_cur_domain' and (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)\<rbrace>
3836    threadSet F t
3837   \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>"
3838apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
3839apply (wp hoare_vcg_disj_lift hoare_vcg_imp_lift)
3840  apply wps
3841  apply wp
3842 apply wps
3843 apply wp
3844apply (auto simp: obj_at'_def)
3845done
3846
3847crunch typ_at'[wp]: invalidateTLBByASID "\<lambda>s. P (typ_at' T p s)"
3848crunch valid_arch_state'[wp]: invalidateTLBByASID "valid_arch_state'"
3849lemmas invalidateTLBByASID_typ_ats[wp] = typ_at_lifts [OF invalidateTLBByASID_typ_at']
3850
3851lemma cte_wp_at_norm_eq':
3852  "cte_wp_at' P p s = (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> P cte)"
3853  by (simp add: cte_wp_at_ctes_of)
3854
3855lemma isFinal_cte_wp_def:
3856  "isFinal cap p (cteCaps_of s) =
3857  (\<not>isUntypedCap cap \<and>
3858   (\<forall>p'. p \<noteq> p' \<longrightarrow>
3859         cte_at' p' s \<longrightarrow>
3860         cte_wp_at' (\<lambda>cte'. \<not> isUntypedCap (cteCap cte') \<longrightarrow>
3861                            \<not> sameObjectAs cap (cteCap cte')) p' s))"
3862  apply (simp add: isFinal_def cte_wp_at_ctes_of cteCaps_of_def)
3863  apply (rule iffI)
3864   apply clarsimp
3865   apply (case_tac cte)
3866   apply fastforce
3867  apply fastforce
3868  done
3869
3870lemma valid_cte_at_neg_typ':
3871  assumes T: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>"
3872  shows "\<lbrace>\<lambda>s. \<not> cte_at' p' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> cte_at' p' s\<rbrace>"
3873  apply (simp add: cte_at_typ')
3874  apply (rule hoare_vcg_conj_lift [OF T])
3875  apply (simp only: imp_conv_disj)
3876  apply (rule hoare_vcg_all_lift)
3877  apply (rule hoare_vcg_disj_lift [OF T])
3878  apply (rule hoare_vcg_prop)
3879  done
3880
3881lemma isFinal_lift:
3882  assumes x: "\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace>"
3883  assumes y: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>"
3884  shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. isFinal (cteCap cte) sl (cteCaps_of s)) sl s\<rbrace>
3885         f
3886         \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>cte. isFinal (cteCap cte) sl (cteCaps_of s)) sl s\<rbrace>"
3887  apply (subst cte_wp_at_norm_eq')
3888  apply (subst cte_wp_at_norm_eq' [where P="\<lambda>cte. isFinal (cteCap cte) sl m" for sl m])
3889  apply (simp only: isFinal_cte_wp_def imp_conv_disj de_Morgan_conj)
3890  apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift x hoare_vcg_disj_lift
3891            valid_cte_at_neg_typ' [OF y])
3892  done
3893
3894crunch cteCaps_of: invalidateTLBByASID "\<lambda>s. P (cteCaps_of s)"
3895
3896crunch valid_etcbs[wp]: invalidate_tlb_by_asid valid_etcbs
3897
3898lemma cteCaps_of_ctes_of_lift:
3899  "(\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s) \<rbrace> f \<lbrace>\<lambda>_ s. P (cteCaps_of s)\<rbrace>"
3900  unfolding cteCaps_of_def .
3901
3902lemmas final_matters'_simps = final_matters'_def [split_simps capability.split arch_capability.split]
3903
3904definition set_thread_all :: "obj_ref \<Rightarrow> Structures_A.tcb \<Rightarrow> etcb
3905                                \<Rightarrow> unit det_ext_monad" where
3906  "set_thread_all ptr tcb etcb \<equiv>
3907     do s \<leftarrow> get;
3908       kh \<leftarrow> return $ kheap s(ptr \<mapsto> (TCB tcb));
3909       ekh \<leftarrow> return $ (ekheap s)(ptr \<mapsto> etcb);
3910       put (s\<lparr>kheap := kh, ekheap := ekh\<rparr>)
3911     od"
3912
3913definition thread_gets_the_all :: "obj_ref \<Rightarrow> (Structures_A.tcb \<times> etcb) det_ext_monad" where
3914  "thread_gets_the_all tptr \<equiv>
3915          do tcb \<leftarrow> gets_the $ get_tcb tptr;
3916             etcb \<leftarrow> gets_the $ get_etcb tptr;
3917             return $ (tcb, etcb) od"
3918
3919definition thread_set_all :: "(Structures_A.tcb \<Rightarrow> Structures_A.tcb) \<Rightarrow> (etcb \<Rightarrow> etcb)
3920                  \<Rightarrow> obj_ref \<Rightarrow> unit det_ext_monad" where
3921  "thread_set_all f g tptr \<equiv>
3922     do (tcb, etcb) \<leftarrow> thread_gets_the_all tptr;
3923        set_thread_all tptr (f tcb) (g etcb)
3924     od"
3925
3926lemma thread_set_ethread_set_all:
3927  "do thread_set f t; ethread_set g t od
3928   = thread_set_all f g t"
3929  by (rule ext) (clarsimp simp: thread_set_def ethread_set_def gets_the_def set_object_def set_object_def fail_def assert_opt_def split_def do_extended_op_def thread_set_all_def set_thread_all_def set_eobject_def thread_gets_the_all_def bind_def gets_def get_def return_def put_def get_etcb_def split: option.splits)
3930
3931lemma set_thread_all_corres:
3932  fixes ob' :: "'a :: pspace_storable"
3933  assumes x: "updateObject ob' = updateObject_default ob'"
3934  assumes z: "\<And>s. obj_at' P ptr s
3935               \<Longrightarrow> map_to_ctes ((ksPSpace s) (ptr \<mapsto> injectKO ob')) = map_to_ctes (ksPSpace s)"
3936  assumes b: "\<And>ko. P ko \<Longrightarrow> objBits ko = objBits ob'"
3937  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
3938  assumes e: "etcb_relation etcb tcb'"
3939  assumes is_t: "injectKO (ob' :: 'a :: pspace_storable) = KOTCB tcb'"
3940  shows      "other_obj_relation (TCB tcb) (injectKO (ob' :: 'a :: pspace_storable)) \<Longrightarrow>
3941  corres dc (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr)
3942            (obj_at' (P :: 'a \<Rightarrow> bool) ptr)
3943            (set_thread_all ptr tcb etcb) (setObject ptr ob')"
3944  apply (rule corres_no_failI)
3945   apply (rule no_fail_pre)
3946    apply wp
3947    apply (rule x)
3948   apply (clarsimp simp: b elim!: obj_at'_weakenE)
3949  apply (unfold set_thread_all_def setObject_def)
3950  apply (clarsimp simp: in_monad split_def bind_def gets_def get_def Bex_def
3951                        put_def return_def modify_def get_object_def x
3952                        projectKOs
3953                        updateObject_default_def in_magnitude_check [OF _ P])
3954  apply (clarsimp simp add: state_relation_def z)
3955  apply (simp add: trans_state_update'[symmetric] trans_state_update[symmetric]
3956         del: trans_state_update)
3957  apply (clarsimp simp add: swp_def fun_upd_def obj_at_def is_etcb_at_def)
3958  apply (subst cte_wp_at_after_update,fastforce simp add: obj_at_def)
3959  apply (subst caps_of_state_after_update,fastforce simp add: obj_at_def)
3960  apply clarsimp
3961  apply (subst conj_assoc[symmetric])
3962  apply (rule conjI[rotated])
3963   apply (clarsimp simp add: ghost_relation_def)
3964   apply (erule_tac x=ptr in allE)+
3965   apply (clarsimp simp: obj_at_def
3966                   split: Structures_A.kernel_object.splits if_split_asm)
3967
3968  apply (fold fun_upd_def)
3969  apply (simp only: pspace_relation_def dom_fun_upd2 simp_thms)
3970  apply (subst pspace_dom_update)
3971    apply assumption
3972   apply simp
3973  apply (simp only: dom_fun_upd2 simp_thms)
3974  apply (elim conjE)
3975  apply (frule bspec, erule domI)
3976  apply (rule conjI)
3977   apply (rule ballI, drule(1) bspec)
3978   apply (drule domD)
3979   apply (clarsimp simp: is_other_obj_relation_type)
3980   apply (drule(1) bspec)
3981   apply clarsimp
3982   apply (frule_tac ko'="TCB tcb'" and x'=ptr in obj_relation_cut_same_type,
3983           (fastforce simp add: is_other_obj_relation_type)+)[1]
3984  apply (simp only: ekheap_relation_def dom_fun_upd2 simp_thms)
3985  apply (frule bspec, erule domI)
3986  apply (rule ballI, drule(1) bspec)
3987  apply (drule domD)
3988  apply (clarsimp simp: obj_at'_def)
3989  apply (clarsimp simp: projectKOs)
3990  apply (insert e is_t)
3991  by (clarsimp simp: other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_A.arch_kernel_obj.splits)
3992
3993lemma tcb_update_all_corres':
3994  assumes tcbs: "tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'"
3995  assumes tables: "\<forall>(getF, v) \<in> ran tcb_cap_cases. getF tcbu = getF tcb"
3996  assumes tables': "\<forall>(getF, v) \<in> ran tcb_cte_cases. getF tcbu' = getF tcb'"
3997  assumes r: "r () ()"
3998  assumes e: "etcb_relation etcb tcb' \<Longrightarrow> etcb_relation etcbu tcbu'"
3999  shows "corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb))
4000                  (ko_at' tcb' add)
4001                  (set_thread_all add tcbu etcbu) (setObject add tcbu')"
4002  apply (rule_tac F="tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu'" in corres_req)
4003   apply (clarsimp simp: state_relation_def obj_at_def obj_at'_def)
4004   apply (frule(1) pspace_relation_absD)
4005   apply (force simp: projectKOs other_obj_relation_def ekheap_relation_def e)
4006  apply (erule conjE)
4007  apply (rule corres_guard_imp)
4008    apply (rule corres_rel_imp)
4009     apply (rule set_thread_all_corres[where P="(=) tcb'"])
4010           apply (rule ext)+
4011           apply simp
4012          defer
4013          apply (simp add: is_other_obj_relation_type_def
4014                           projectKOs objBits_simps'
4015                           other_obj_relation_def tcbs r)+
4016    apply (fastforce simp: is_etcb_at_def elim!: obj_at_weakenE dest: bspec[OF tables])
4017   apply (subst(asm) eq_commute, assumption)
4018  apply (clarsimp simp: projectKOs obj_at'_def objBits_simps)
4019  apply (subst map_to_ctes_upd_tcb, assumption+)
4020   apply (simp add: ps_clear_def3 field_simps objBits_defs mask_def)
4021  apply (subst if_not_P)
4022   apply (fastforce dest: bspec [OF tables', OF ranI])
4023  apply simp
4024  done
4025
4026lemma thread_gets_the_all_corres:
4027  shows      "corres (\<lambda>(tcb, etcb) tcb'. tcb_relation tcb tcb' \<and> etcb_relation etcb tcb')
4028                (tcb_at t and is_etcb_at t) (tcb_at' t)
4029                (thread_gets_the_all t) (getObject t)"
4030  apply (rule corres_no_failI)
4031   apply wp
4032  apply (clarsimp simp add: gets_def get_def return_def bind_def get_tcb_def thread_gets_the_all_def threadGet_def ethread_get_def gets_the_def assert_opt_def get_etcb_def is_etcb_at_def tcb_at_def liftM_def split: option.splits Structures_A.kernel_object.splits)
4033  apply (frule in_inv_by_hoareD [OF getObject_inv_tcb])
4034  apply (clarsimp simp add: obj_at_def is_tcb obj_at'_def projectKO_def
4035                            projectKO_opt_tcb split_def
4036                            getObject_def loadObject_default_def in_monad)
4037  apply (case_tac ko)
4038   apply (simp_all add: fail_def return_def)
4039  apply (clarsimp simp add: state_relation_def pspace_relation_def ekheap_relation_def)
4040  apply (drule bspec)
4041   apply clarsimp
4042   apply blast
4043  apply (drule bspec, erule domI)
4044  apply (clarsimp simp add: other_obj_relation_def
4045                            lookupAround2_known1)
4046  done
4047
4048lemma thread_set_all_corresT:
4049  assumes x: "\<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow>
4050                         tcb_relation (f tcb) (f' tcb')"
4051  assumes y: "\<And>tcb. \<forall>(getF, setF) \<in> ran tcb_cap_cases. getF (f tcb) = getF tcb"
4052  assumes z: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
4053                 getF (f' tcb) = getF tcb"
4054  assumes e: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow>
4055                         etcb_relation (g etcb) (f' tcb')"
4056  shows      "corres dc (tcb_at t and valid_etcbs)
4057                        (tcb_at' t)
4058                    (thread_set_all f g t) (threadSet f' t)"
4059  apply (simp add: thread_set_all_def threadSet_def bind_assoc)
4060  apply (rule corres_guard_imp)
4061    apply (rule corres_split [OF _ thread_gets_the_all_corres])
4062      apply (simp add: split_def)
4063      apply (rule tcb_update_all_corres')
4064          apply (erule x)
4065         apply (rule y)
4066        apply (clarsimp simp: bspec_split [OF spec [OF z]])
4067       apply fastforce
4068      apply (erule e)
4069     apply (simp add: thread_gets_the_all_def, wp+)
4070   apply clarsimp
4071   apply (frule(1) tcb_at_is_etcb_at)
4072   apply (clarsimp simp add: tcb_at_def get_etcb_def obj_at_def)
4073   apply (drule get_tcb_SomeD)
4074   apply fastforce
4075  apply simp
4076  done
4077
4078lemmas thread_set_all_corres =
4079    thread_set_all_corresT [OF _ _ all_tcbI, OF _ ball_tcb_cap_casesI ball_tcb_cte_casesI]
4080
4081lemma thread_get_thread_get:
4082  "do x \<leftarrow> thread_get f tptr; y \<leftarrow> thread_get g tptr; h x y od
4083    = do tcb \<leftarrow> thread_get id tptr; h (f tcb) (g tcb) od"
4084  apply (rule ext)
4085  apply (clarsimp simp: thread_get_def gets_the_def bind_assoc
4086                        exec_gets assert_opt_def
4087         split: option.split)
4088  done
4089
4090lemma thread_set_gets_futz:
4091  "thread_set F t >>= (\<lambda>_. gets cur_domain >>= g)
4092 = gets cur_domain >>= (\<lambda>cdom. thread_set F t >>= K (g cdom))"
4093apply (rule ext)
4094apply (simp add: assert_opt_def bind_def fail_def get_def gets_def gets_the_def put_def return_def set_object_def thread_set_def split_def
4095          split: option.splits)
4096done
4097
4098lemma tcb_relation_convert_for_recycle_assert:
4099  "\<lbrakk>tcb_relation tcb rv'; inactive (tcb_state tcb); tcb_bound_notification tcb = None\<rbrakk> \<Longrightarrow>
4100       tcbState rv' = Structures_H.thread_state.Inactive \<and> tcbBoundNotification rv' = None"
4101  by (simp add: tcb_relation_def)
4102
4103crunch idle_thread[wp]: deleteCallerCap "\<lambda>s. P (ksIdleThread s)"
4104  (wp: crunch_wps)
4105crunch sch_act_simple: deleteCallerCap sch_act_simple
4106  (wp: crunch_wps)
4107crunch sch_act_not[wp]: deleteCallerCap "sch_act_not t"
4108  (wp: crunch_wps)
4109crunch typ_at'[wp]: deleteCallerCap "\<lambda>s. P (typ_at' T p s)"
4110  (wp: crunch_wps)
4111lemmas deleteCallerCap_typ_ats[wp] = typ_at_lifts [OF deleteCallerCap_typ_at']
4112
4113crunch ksQ[wp]: emptySlot "\<lambda>s. P (ksReadyQueues s p)"
4114
4115lemma setEndpoint_sch_act_not_ct[wp]:
4116  "\<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace>
4117   setEndpoint ptr val \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>"
4118  by (rule hoare_weaken_pre, wps setEndpoint_ct', wp, simp)
4119
4120lemma cancelAll_ct_not_ksQ_helper:
4121  "\<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ksCurThread s \<notin> set q) \<rbrace>
4122   mapM_x (\<lambda>t. do
4123                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
4124                 tcbSchedEnqueue t
4125               od) q
4126   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
4127  apply (rule mapM_x_inv_wp2, simp)
4128  apply (wp)
4129    apply (wps tcbSchedEnqueue_ct')
4130    apply (wp tcbSchedEnqueue_ksQ)
4131   apply (wps setThreadState_ct')
4132   apply (wp sts_ksQ')
4133  apply (clarsimp)
4134  done
4135
4136lemma cancelAllIPC_ct_not_ksQ:
4137  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
4138          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
4139   cancelAllIPC epptr
4140   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
4141  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>")
4142  apply (simp add: cancelAllIPC_def)
4143  apply (wp, wpc, wp)
4144        apply (wps rescheduleRequired_ct')
4145        apply (wp rescheduleRequired_ksQ')
4146       apply (clarsimp simp: forM_x_def)
4147       apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv)
4148      apply (wp hoare_lift_Pf2 [OF setEndpoint_ksQ setEndpoint_ct'])+
4149      apply (wps rescheduleRequired_ct')
4150      apply (wp rescheduleRequired_ksQ')
4151     apply (clarsimp simp: forM_x_def)
4152     apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv)
4153    apply (wp hoare_lift_Pf2 [OF setEndpoint_ksQ setEndpoint_ct'])+
4154   prefer 2
4155   apply assumption
4156  apply (rule_tac Q="\<lambda>ep. ?PRE and ko_at' ep epptr" in hoare_post_imp)
4157   apply (clarsimp)
4158   apply (rule conjI)
4159    apply ((clarsimp simp: invs'_def valid_state'_def
4160                           sch_act_sane_def
4161            | drule(1) ct_not_in_epQueue)+)[2]
4162  apply (wp get_ep_sp')
4163  done
4164
4165lemma cancelAllSignals_ct_not_ksQ:
4166  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
4167          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
4168   cancelAllSignals ntfnptr
4169   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
4170  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>")
4171  apply (simp add: cancelAllSignals_def)
4172  apply (wp, wpc, wp+)
4173      apply (wps rescheduleRequired_ct')
4174      apply (wp rescheduleRequired_ksQ')
4175     apply clarsimp
4176     apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv)
4177    apply (wp hoare_lift_Pf2 [OF setNotification_ksQ setNotification_ksCurThread])
4178    apply (wps setNotification_ksCurThread, wp)
4179   prefer 2
4180   apply assumption
4181  apply (rule_tac Q="\<lambda>ep. ?PRE and ko_at' ep ntfnptr" in hoare_post_imp)
4182   apply ((clarsimp simp: invs'_def valid_state'_def sch_act_sane_def
4183          | drule(1) ct_not_in_ntfnQueue)+)[1]
4184  apply (wp get_ntfn_sp')
4185  done
4186
4187lemma unbindNotification_ct_not_ksQ:
4188 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
4189          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
4190   unbindNotification t
4191   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
4192  apply (simp add: unbindNotification_def)
4193  apply (rule hoare_seq_ext[OF _ gbn_sp'])
4194  apply (case_tac ntfnPtr, simp, wp, simp)
4195  apply (clarsimp)
4196  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
4197  apply (rule hoare_pre)
4198   apply (wp)
4199    apply (wps setBoundNotification_ct')
4200    apply (wp sbn_ksQ)
4201   apply (wps setNotification_ksCurThread, wp)
4202  apply clarsimp
4203  done
4204
4205lemma unbindMaybeNotification_ct_not_ksQ:
4206 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
4207          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
4208   unbindMaybeNotification t
4209   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
4210  apply (simp add: unbindMaybeNotification_def)
4211  apply (rule hoare_seq_ext[OF _ get_ntfn_sp'])
4212  apply (case_tac "ntfnBoundTCB ntfn", simp, wp, simp+)
4213  apply (rule hoare_pre)
4214    apply wp
4215    apply (wps setBoundNotification_ct')
4216    apply (wp sbn_ksQ)
4217   apply (wps setNotification_ksCurThread, wp)
4218  apply clarsimp
4219  done
4220
4221lemma sbn_ct_in_state'[wp]:
4222  "\<lbrace>ct_in_state' P\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>"
4223  apply (simp add: ct_in_state'_def)
4224  apply (rule hoare_pre)
4225   apply (wps setBoundNotification_ct')
4226  apply (wp sbn_st_tcb', clarsimp)
4227  done
4228
4229lemma set_ntfn_ct_in_state'[wp]:
4230  "\<lbrace>ct_in_state' P\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>"
4231  apply (simp add: ct_in_state'_def)
4232  apply (rule hoare_pre)
4233   apply (wps setNotification_ksCurThread, wp, clarsimp)
4234  done
4235
4236lemma unbindNotification_ct_in_state'[wp]:
4237  "\<lbrace>ct_in_state' P\<rbrace> unbindNotification t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>"
4238  apply (simp add: unbindNotification_def)
4239  apply (wp | wpc | simp)+
4240  done
4241
4242lemma unbindMaybeNotification_ct_in_state'[wp]:
4243  "\<lbrace>ct_in_state' P\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>"
4244  apply (simp add: unbindMaybeNotification_def)
4245  apply (wp | wpc | simp)+
4246  done
4247
4248lemma setNotification_sch_act_sane:
4249  "\<lbrace>sch_act_sane\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
4250  by (wp sch_act_sane_lift)
4251
4252crunch sch_act_sane[wp]: unbindNotification, unbindMaybeNotification "sch_act_sane"
4253
4254lemma finaliseCapTrue_standin_ct_not_ksQ:
4255  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
4256          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
4257   finaliseCapTrue_standin cap final
4258   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
4259  apply (simp add: finaliseCapTrue_standin_def Let_def)
4260  apply (safe)
4261      apply (wp cancelAllIPC_ct_not_ksQ cancelAllSignals_ct_not_ksQ unbindNotification_ct_not_ksQ
4262                hoare_drop_imps unbindMaybeNotification_ct_not_ksQ
4263             | wpc
4264             | clarsimp simp: isNotificationCap_def isReplyCap_def split:capability.splits)+
4265  done
4266
4267lemma cteDeleteOne_ct_not_ksQ:
4268  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
4269          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
4270   cteDeleteOne slot
4271   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
4272  apply (simp add: cteDeleteOne_def unless_def split_def)
4273  apply (rule hoare_seq_ext [OF _ getCTE_sp])
4274  apply (case_tac "\<forall>final. finaliseCap (cteCap cte) final True = fail")
4275   apply (simp add: finaliseCapTrue_standin_simple_def)
4276   apply wp
4277   apply (clarsimp)
4278  apply (wp emptySlot_cteCaps_of hoare_lift_Pf2 [OF emptySlot_ksRQ emptySlot_ct])
4279    apply (simp add: cteCaps_of_def)
4280    apply (wp_once hoare_drop_imps)
4281    apply (wp finaliseCapTrue_standin_ct_not_ksQ isFinalCapability_inv)+
4282  apply (clarsimp)
4283  done
4284
4285end
4286
4287end
4288