theory Finalise_R

lemma cteDeleteOne_invs[wp]:
  "\<lbrace>invs'\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: cteDeleteOne_def unless_def
                   split_def finaliseCapTrue_standin_simple_def) apply wp apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule finaliseCap_True_invs) apply (rule hoare_vcg_conj_lift) apply (rule finaliseCap_replaceable[where slot=ptr]) apply (rule hoare_vcg_conj_lift) apply (rule finaliseCap_cte_refs) apply (rule finaliseCap_equal_cap[where sl=ptr]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule disjE) apply simp apply (clarsimp dest!: isCapDs simp: capRemovable_def) apply (clarsimp simp: removeable'_def fun_eq_iff[where f="cte_refs' cap" for cap]
                     del: disjCI) apply (rule disjI2) apply (rule conjI) subgoal by auto subgoal by (auto dest!: isCapDs simp: pred_tcb_at'_def obj_at'_def projectKOs
                                     ko_wp_at'_def) apply (wp isFinalCapability_inv getCTE_wp' hoare_weak_lift_imp
        | wp (once) isFinal[where x=ptr])+ apply (fastforce simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do cte <- getCTE ptr;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- global.finaliseCap (cteCap cte) final True;
y <- assert (capRemovable (fst p) ptr \<and> snd p = capability.NullCap);
emptySlot ptr capability.NullCap
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B3 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>\<lambda>p s. capRemovable (fst p) ptr \<and> snd p = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)\<rbrace>
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>?B3 cte\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?B3 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q8 cte final\<rbrace>
 2. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; ?Q8 cte final rv s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 3. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>?B3 cte\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P11 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q11 cte final\<rbrace>
 2. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P'11 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q'11 cte final\<rbrace>
 3. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; ?Q11 cte final rv s \<and> ?Q'11 cte final rv s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 4. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. ?P11 cte final s \<and> ?P'11 cte final s\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 6. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P'11 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q'11 cte final\<rbrace>
 2. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s \<and> ?Q'11 cte final rv s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 3. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> ?P'11 cte final s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P15 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q15 cte final\<rbrace>
 2. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P'15 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q'15 cte final\<rbrace>
 3. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s \<and> ?Q15 cte final rv s \<and> ?Q'15 cte final rv s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 4. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> ?P15 cte final s \<and> ?P'15 cte final s\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 6. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P'15 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q'15 cte final\<rbrace>
 2. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s \<and> (isNullCap (fst rv) \<and> removeable' ptr s (cteCap cte) \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> snd rv = cteCap cte \<and> cap_has_cleanup' (cteCap cte) \<and> isFinal (cteCap cte) ptr (cteCaps_of s)) \<or> isZombie (fst rv) \<and> snd rv = capability.NullCap \<and> isFinal (cteCap cte) ptr (cteCaps_of s) \<and> capClass (cteCap cte) = capClass (fst rv) \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr (cteCap cte) \<and> capBits (fst rv) = capBits (cteCap cte) \<and> capRange (fst rv) = capRange (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr)))) \<and> ?Q'15 cte final rv s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 3. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> ?P'15 cte final s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P19 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q19 cte final\<rbrace>
 2. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P'19 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q'19 cte final\<rbrace>
 3. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s \<and> (isNullCap (fst rv) \<and> removeable' ptr s (cteCap cte) \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> snd rv = cteCap cte \<and> cap_has_cleanup' (cteCap cte) \<and> isFinal (cteCap cte) ptr (cteCaps_of s)) \<or> isZombie (fst rv) \<and> snd rv = capability.NullCap \<and> isFinal (cteCap cte) ptr (cteCaps_of s) \<and> capClass (cteCap cte) = capClass (fst rv) \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr (cteCap cte) \<and> capBits (fst rv) = capBits (cteCap cte) \<and> capRange (fst rv) = capRange (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr)))) \<and> ?Q19 cte final rv s \<and> ?Q'19 cte final rv s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 4. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> ?P19 cte final s \<and> ?P'19 cte final s\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 6. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?P'19 cte final\<rbrace> global.finaliseCap (cteCap cte) final True \<lbrace>?Q'19 cte final\<rbrace>
 2. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s \<and> (isNullCap (fst rv) \<and> removeable' ptr s (cteCap cte) \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> snd rv = cteCap cte \<and> cap_has_cleanup' (cteCap cte) \<and> isFinal (cteCap cte) ptr (cteCaps_of s)) \<or> isZombie (fst rv) \<and> snd rv = capability.NullCap \<and> isFinal (cteCap cte) ptr (cteCaps_of s) \<and> capClass (cteCap cte) = capClass (fst rv) \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr (cteCap cte) \<and> capBits (fst rv) = capBits (cteCap cte) \<and> capRange (fst rv) = capRange (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr)))) \<and> (fst rv \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' (cteCap cte)) \<and> ?Q'19 cte final rv s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 3. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> ?P'19 cte final s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cte final rv s. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s \<and> (isNullCap (fst rv) \<and> removeable' ptr s (cteCap cte) \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> snd rv = cteCap cte \<and> cap_has_cleanup' (cteCap cte) \<and> isFinal (cteCap cte) ptr (cteCaps_of s)) \<or> isZombie (fst rv) \<and> snd rv = capability.NullCap \<and> isFinal (cteCap cte) ptr (cteCaps_of s) \<and> capClass (cteCap cte) = capClass (fst rv) \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr (cteCap cte) \<and> capBits (fst rv) = capBits (cteCap cte) \<and> capRange (fst rv) = capRange (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr)))) \<and> (fst rv \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' (cteCap cte)) \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrakk> \<Longrightarrow> capRemovable (fst rv) ptr \<and> snd rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. capability.NullCap \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some capability.NullCap)
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cte a s ctea. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; a = capability.NullCap \<and> removeable' ptr s (cteCap cte) \<or> isZombie a \<and> isFinal (cteCap cte) ptr (cteCaps_of s) \<and> capClass (cteCap cte) = capClass a \<and> global.capUntypedPtr a = global.capUntypedPtr (cteCap cte) \<and> capBits a = capBits (cteCap cte) \<and> capRange a = capRange (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b)))); a \<noteq> capability.NullCap \<longrightarrow> cte_refs' a = cte_refs' (cteCap cte); ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; capRemovable a ptr\<rbrakk> \<Longrightarrow> removeable' ptr s (cteCap cte)
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cte a s ctea. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; a \<noteq> capability.NullCap \<longrightarrow> cte_refs' a = cte_refs' (cteCap cte); ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; capRemovable a ptr; a = capability.NullCap \<and> removeable' ptr s (cteCap cte)\<rbrakk> \<Longrightarrow> removeable' ptr s (cteCap cte)
 2. \<And>cte a s ctea. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; a \<noteq> capability.NullCap \<longrightarrow> cte_refs' a = cte_refs' (cteCap cte); ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; capRemovable a ptr; isZombie a \<and> isFinal (cteCap cte) ptr (cteCaps_of s) \<and> capClass (cteCap cte) = capClass a \<and> global.capUntypedPtr a = global.capUntypedPtr (cteCap cte) \<and> capBits a = capBits (cteCap cte) \<and> capRange a = capRange (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))\<rbrakk> \<Longrightarrow> removeable' ptr s (cteCap cte)
 3. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cte a s ctea. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; a \<noteq> capability.NullCap \<longrightarrow> cte_refs' a = cte_refs' (cteCap cte); ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; capRemovable a ptr; isZombie a \<and> isFinal (cteCap cte) ptr (cteCaps_of s) \<and> capClass (cteCap cte) = capClass a \<and> global.capUntypedPtr a = global.capUntypedPtr (cteCap cte) \<and> capBits a = capBits (cteCap cte) \<and> capRange a = capRange (cteCap cte) \<and> (isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte)) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))\<rbrakk> \<Longrightarrow> removeable' ptr s (cteCap cte)
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cte s ctea bits num. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; cte_refs' (capability.Zombie (global.capUntypedPtr (cteCap cte)) bits num) = cte_refs' (cteCap cte); ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; num = 0 \<or> num = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte); isFinal (cteCap cte) ptr (cteCaps_of s); capClass (cteCap cte) = PhysicalClass; zBits bits = capBits (cteCap cte); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte)) bits num) = capRange (cteCap cte); isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte); \<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> removeable' ptr s (cteCap cte)
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cte s ctea bits num. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; \<forall>x. (\<lambda>x. global.capUntypedPtr (cteCap cte) + x * 2 ^ cteSizeBits) ` {0..<word_of_nat num} = cte_refs' (cteCap cte) x; ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; num = 0 \<or> num = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte); isFinal (cteCap cte) ptr (cteCaps_of s); capClass (cteCap cte) = PhysicalClass; zBits bits = capBits (cteCap cte); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte)) bits num) = capRange (cteCap cte); isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte); \<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> (\<exists>p. p \<noteq> ptr \<and> cte_wp_at' (\<lambda>ctea. capMasterCap (cteCap ctea) = capMasterCap (cteCap cte)) p s) \<or> (\<forall>p\<in>{0..<word_of_nat num}. global.capUntypedPtr (cteCap cte) + p * 2 ^ cteSizeBits \<noteq> ptr \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (global.capUntypedPtr (cteCap cte) + p * 2 ^ cteSizeBits) s) \<and> (\<forall>p\<in>zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p s)
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cte s ctea bits num. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; \<forall>x. (\<lambda>x. global.capUntypedPtr (cteCap cte) + x * 2 ^ cteSizeBits) ` {0..<word_of_nat num} = cte_refs' (cteCap cte) x; ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; num = 0 \<or> num = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte); isFinal (cteCap cte) ptr (cteCaps_of s); capClass (cteCap cte) = PhysicalClass; zBits bits = capBits (cteCap cte); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte)) bits num) = capRange (cteCap cte); isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte); \<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> (\<forall>p\<in>{0..<word_of_nat num}. global.capUntypedPtr (cteCap cte) + p * 2 ^ cteSizeBits \<noteq> ptr \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (global.capUntypedPtr (cteCap cte) + p * 2 ^ cteSizeBits) s) \<and> (\<forall>p\<in>zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p s)
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cte s ctea bits num. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; \<forall>x. (\<lambda>x. global.capUntypedPtr (cteCap cte) + x * 2 ^ cteSizeBits) ` {0..<word_of_nat num} = cte_refs' (cteCap cte) x; ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; num = 0 \<or> num = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte); isFinal (cteCap cte) ptr (cteCaps_of s); capClass (cteCap cte) = PhysicalClass; zBits bits = capBits (cteCap cte); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte)) bits num) = capRange (cteCap cte); isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte); \<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<forall>p\<in>{0..<word_of_nat num}. global.capUntypedPtr (cteCap cte) + p * 2 ^ cteSizeBits \<noteq> ptr \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (global.capUntypedPtr (cteCap cte) + p * 2 ^ cteSizeBits) s
 2. \<And>cte s ctea bits num. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; \<forall>x. (\<lambda>x. global.capUntypedPtr (cteCap cte) + x * 2 ^ cteSizeBits) ` {0..<word_of_nat num} = cte_refs' (cteCap cte) x; ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; num = 0 \<or> num = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte); isFinal (cteCap cte) ptr (cteCaps_of s); capClass (cteCap cte) = PhysicalClass; zBits bits = capBits (cteCap cte); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte)) bits num) = capRange (cteCap cte); isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte); \<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<forall>p\<in>zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p s
 3. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte_ \<noteq> capability.NullCap; invs' s_; \<forall>x. (\<lambda>x. global.capUntypedPtr (cteCap cte_) + x * 2 ^ cteSizeBits) ` {0..<word_of_nat num_} = cte_refs' (cteCap cte_) x; ctes_of s_ ptr = Some ctea_; cteCap ctea_ = cteCap cte_; num_ = 0 \<or> num_ = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte_); isFinal (cteCap cte_) ptr (cteCaps_of s_); capClass (cteCap cte_) = PhysicalClass; zBits bits_ = capBits (cteCap cte_); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte_)) bits_ num_) = capRange (cteCap cte_); isThreadCap (cteCap cte_) \<or> isCNodeCap (cteCap cte_) \<or> isZombie (cteCap cte_); \<forall>p\<in>threadCapRefs (cteCap cte_). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s_ \<and> obj_at' (Not \<circ> tcbQueued) p s_ \<and> bound_tcb_at' ((=) None) p s_ \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s_ (a, b)))\<rbrakk> \<Longrightarrow> \<forall>p\<in>{0..<word_of_nat num_}. global.capUntypedPtr (cteCap cte_) + p * 2 ^ cteSizeBits \<noteq> ptr \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (global.capUntypedPtr (cteCap cte_) + p * 2 ^ cteSizeBits) s_ proof (prove)
goal (4 subgoals):
 1. \<And>cte s ctea bits num. \<lbrakk>cteCap cte \<noteq> capability.NullCap; invs' s; \<forall>x. (\<lambda>x. global.capUntypedPtr (cteCap cte) + x * 2 ^ cteSizeBits) ` {0..<word_of_nat num} = cte_refs' (cteCap cte) x; ctes_of s ptr = Some ctea; cteCap ctea = cteCap cte; num = 0 \<or> num = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte); isFinal (cteCap cte) ptr (cteCaps_of s); capClass (cteCap cte) = PhysicalClass; zBits bits = capBits (cteCap cte); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte)) bits num) = capRange (cteCap cte); isThreadCap (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isZombie (cteCap cte); \<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<forall>p\<in>zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p s
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte_ \<noteq> capability.NullCap; invs' s_; \<forall>x. (\<lambda>x. global.capUntypedPtr (cteCap cte_) + x * 2 ^ cteSizeBits) ` {0..<word_of_nat num_} = cte_refs' (cteCap cte_) x; ctes_of s_ ptr = Some ctea_; cteCap ctea_ = cteCap cte_; num_ = 0 \<or> num_ = Suc 0 \<and> ptr = global.capUntypedPtr (cteCap cte_); isFinal (cteCap cte_) ptr (cteCaps_of s_); capClass (cteCap cte_) = PhysicalClass; zBits bits_ = capBits (cteCap cte_); capRange (capability.Zombie (global.capUntypedPtr (cteCap cte_)) bits_ num_) = capRange (cteCap cte_); isThreadCap (cteCap cte_) \<or> isCNodeCap (cteCap cte_) \<or> isZombie (cteCap cte_); \<forall>p\<in>threadCapRefs (cteCap cte_). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s_ \<and> obj_at' (Not \<circ> tcbQueued) p s_ \<and> bound_tcb_at' ((=) None) p s_ \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s_ (a, b)))\<rbrakk> \<Longrightarrow> \<forall>p\<in>zobj_refs' (cteCap cte_). ko_wp_at' (Not \<circ> live') p s_ proof (prove)
goal (3 subgoals):
 1. \<And>cte. cteCap cte \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>?Q2 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final s. invs' s \<and> (invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getCTE ptr \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?Q2 cte else invs'\<rbrace>
 3. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) ptr s \<longrightarrow> (if cteCap cte \<noteq> capability.NullCap then \<lambda>s. invs' s \<and> invs' s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s \<and> (final_matters' (cteCap cte) \<longrightarrow> valid_mdb' s \<and> cte_wp_at' ((=) cte) ptr s \<and> final_matters' (cteCap cte) \<and> isFinal (cteCap cte) ptr (cteCaps_of s) = isFinal (cteCap cte) ptr (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_cap' (cteCap cte) s \<and> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) ptr s else invs') s proof (prove)
goal:
No subgoals!