theory CNodeInv_R

lemma reduceZombie_invs'':
  assumes fin:
  "\<And>s'' rv. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed;
              (Inr rv, s'')
              \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk>
             \<Longrightarrow> s'' \<turnstile> \<lbrace>\<lambda>s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s
                                   \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot s
                                   \<and> ex_cte_cap_to' rv s\<rbrace>
                         finaliseSlot rv False
                \<lbrace>\<lambda>rva s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s
                            \<and> (fst rva \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' rv s (cteCap cte)) rv s)
                            \<and> (\<forall>sl'. snd rva \<noteq> NullCap \<longrightarrow> sl' \<noteq> rv \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rva))\<rbrace>,
                \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>"
  assumes stuff:
    "finalise_prop_stuff Q"
  shows
  "st \<turnstile> \<lbrace>\<lambda>s.
      no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s
              \<and> (exposed \<or> ex_cte_cap_to' slot s)
              \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s
              \<and> (exposed \<or> p = slot \<or>
                  cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)
                                  \<or> (\<exists>zb n cp. cteCap cte = Zombie p zb n
                                       \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>
       reduceZombie cap slot exposed
   \<lbrace>\<lambda>rv s.
      no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s
              \<and> (exposed \<or> ex_cte_cap_to' slot s)
              \<and> (exposed \<or> p = slot \<or>
                  cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)
                                  \<or> (\<exists>zb n cp. cteCap cte = Zombie p zb n
                                       \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>,
   \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>" apply (unfold reduceZombie_def cteDelete_def Let_def
                split_def fst_conv snd_conv haskell_fail_def
                case_Zombie_assert_fold) apply (rule hoare_pre_spec_validE) apply (wp hoare_vcg_disj_lift | simp)+ apply (wp capSwap_cte_wp_cteCap getCTE_wp' | simp)+ apply (wp shrink_zombie_invs')[1] apply (wp | simp)+ apply (rule getCTE_wp) apply (wp | simp)+ apply (rule_tac Q="\<lambda>cte s. rv = capZombiePtr cap +
                                      of_nat (capZombieNumber cap) * 2^cteSizeBits - 2^cteSizeBits
                              \<and> cte_wp_at' (\<lambda>c. c = cte) slot s \<and> invs' s
                              \<and> no_cte_prop Q s \<and> sch_act_simple s"
                  in hoare_post_imp) apply (clarsimp simp: cte_wp_at_ctes_of mult.commute mult.left_commute dest!: isCapDs) apply (simp add: field_simps) apply (wp getCTE_cte_wp_at)+ apply simp apply wp apply (rule spec_strengthen_postE) apply (rule_tac Q="\<lambda>fc s. rv = capZombiePtr cap +
                                      of_nat (capZombieNumber cap) * 2^cteSizeBits - 2^cteSizeBits"
                 in spec_valid_conj_liftE1) apply wp[1] apply (rule fin, assumption+) apply (clarsimp simp: stuff) apply (simp add: locateSlot_conv) apply ((wp | simp)+)[2] apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule conjI) apply (clarsimp dest!: isCapDs) apply (rule conjI) apply (erule(1) ex_Zombie_to) apply clarsimp apply clarsimp apply clarsimp apply (clarsimp dest!: isCapDs) apply (fastforce dest!: ex_Zombie_to2 simp: cte_level_bits_def objBits_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st \<turnstile> \<lbrace>\<lambda>s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace> reduceZombie cap slot exposed \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace> proof (prove)
goal (1 subgoal):
 1. st \<turnstile> \<lbrace>\<lambda>s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace> if isZombie cap \<and> capZombieNumber cap = 0 then fail else if isZombie cap \<and> \<not> exposed then doE haskell_assertE (capZombiePtr cap \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr cap);
assertE (isZombie capAtPtr \<longrightarrow> capZombiePtr capAtPtr \<noteq> capZombiePtr cap);
withoutPreemption $ capSwapForDelete (capZombiePtr cap) slot
odE else if isZombie cap \<and> exposed then doE endSlot <- withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1));
doE p <- finaliseSlot endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr cap = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber cap - 1) cap) >>= updateCap slot
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = slot \<and> capZombiePtr cap \<noteq> slot) [] else fail
odE else fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace> proof (prove)
goal (2 subgoals):
 1. st \<turnstile> \<lbrace>?P'\<rbrace> if isZombie cap \<and> capZombieNumber cap = 0 then fail else if isZombie cap \<and> \<not> exposed then doE haskell_assertE (capZombiePtr cap \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr cap);
assertE (isZombie capAtPtr \<longrightarrow> capZombiePtr capAtPtr \<noteq> capZombiePtr cap);
withoutPreemption $ capSwapForDelete (capZombiePtr cap) slot
odE else if isZombie cap \<and> exposed then doE endSlot <- withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1));
doE p <- finaliseSlot endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr cap = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber cap - 1) cap) >>= updateCap slot
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = slot \<and> capZombiePtr cap \<noteq> slot) [] else fail
odE else fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> ?P' st proof (prove)
goal (6 subgoals):
 1. \<And>s'' rva s''a s''b. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> \<not> exposed; (Inr (), s'') \<in> fst (assertE (capZombiePtr cap \<noteq> slot) st); (rva, s''a) \<in> fst (liftM cteCap (getCTE (capZombiePtr cap)) s''); (Inr (), s''b) \<in> fst (assertE (isZombie rva \<longrightarrow> capZombiePtr rva \<noteq> capZombiePtr cap) s''a)\<rbrakk> \<Longrightarrow> \<lbrace>?P'42 () s'' rva s''a ()\<rbrace> capSwapForDelete (capZombiePtr cap) slot \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); isZombie cap \<and> \<not> exposed; (Inr rv, s'') \<in> fst (haskell_assertE (capZombiePtr cap \<noteq> slot) [] st); (Inr rva, s''a) \<in> fst ((withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr cap)) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B10 rv s'' rva\<rbrace> assertE (isZombie rva \<longrightarrow> capZombiePtr rva \<noteq> capZombiePtr cap) \<lbrace>\<lambda>a b. no_cte_prop Q b \<and> (invs' and ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) and ex_cte_cap_wp_to' (\<lambda>_. True) slot) b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> ?P'42 rv s'' rva s''a a b)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); isZombie cap \<and> \<not> exposed; (Inr rv, s'') \<in> fst (haskell_assertE (capZombiePtr cap \<noteq> slot) [] st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B8 rv\<rbrace> withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr cap) \<lbrace>?B10 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); isZombie cap \<and> \<not> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P7\<rbrace> haskell_assertE (capZombiePtr cap \<noteq> slot) [] \<lbrace>?B8\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'7\<rbrace> if isZombie cap \<and> exposed then doE endSlot <- withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1));
doE p <- finaliseSlot endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr cap = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber cap - 1) cap) >>= updateCap slot
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = slot \<and> capZombiePtr cap \<noteq> slot) [] else fail
odE else fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> ?P7 st) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> ?P'7 st)) proof (prove)
goal (10 subgoals):
 1. \<And>rv s'' s''a rvb s''b endCTE. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s''); (rvb, s''b) \<in> fst (getCTE slot s''a); cteCap rvb \<noteq> capability.NullCap; isZombie (cteCap rvb); capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)\<rbrakk> \<Longrightarrow> \<lbrace>?P'105 rv s'' s''a rvb s''b endCTE ()\<rbrace> updateCap slot (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s'' s''a rvb s''b endCTE. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s''); (rvb, s''b) \<in> fst (getCTE slot s''a); cteCap rvb \<noteq> capability.NullCap; isZombie (cteCap rvb); capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)\<rbrakk> \<Longrightarrow> \<lbrace>?B102 rv s'' s''a rvb s''b endCTE\<rbrace> assert (cteCap endCTE = capability.NullCap) \<lbrace>\<lambda>x s. no_cte_prop Q s \<and> ?P'105 rv s'' s''a rvb s''b endCTE x s\<rbrace>
 3. \<And>rv s'' s''a rvb s''b. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s''); (rvb, s''b) \<in> fst (getCTE slot s''a); cteCap rvb \<noteq> capability.NullCap; isZombie (cteCap rvb); capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)\<rbrakk> \<Longrightarrow> \<lbrace>?P95 rv s'' () s''a rvb\<rbrace> getCTE rv \<lbrace>?B102 rv s'' s''a rvb s''b\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); isZombie (cteCap rvb); \<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb))\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'97 rv s'' rva s''a rvb\<rbrace> haskell_assertE (capZombiePtr (cteCap rvb) = slot \<and> capZombiePtr cap \<noteq> slot) [] \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); \<not> isZombie (cteCap rvb)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'92 rv s'' rva s''a rvb\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B78 rv s'' rva\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rvb s. (isNullCap (cteCap rvb) \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)) \<and> (\<not> isNullCap (cteCap rvb) \<longrightarrow> (isZombie (cteCap rvb) \<longrightarrow> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb) \<longrightarrow> ?P95 rv s'' rva s''a rvb s) \<and> (\<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)) \<longrightarrow> ?P'97 rv s'' rva s''a rvb s)) \<and> (\<not> isZombie (cteCap rvb) \<longrightarrow> ?P'92 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 7. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 8. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 9. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 10. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' s''a rvb s''b endCTE. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s''); (rvb, s''b) \<in> fst (getCTE slot s''a); cteCap rvb \<noteq> capability.NullCap; isZombie (cteCap rvb); capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)\<rbrakk> \<Longrightarrow> \<lbrace>?B102 rv s'' s''a rvb s''b endCTE\<rbrace> assert (cteCap endCTE = capability.NullCap) \<lbrace>\<lambda>x s. no_cte_prop Q s \<and> (invs' and K (isZombie (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (capZombieType (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) + 1)) slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) + 2 ^ cteSizeBits * word_of_nat (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)))) s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s'' s''a rvb s''b. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s''); (rvb, s''b) \<in> fst (getCTE slot s''a); cteCap rvb \<noteq> capability.NullCap; isZombie (cteCap rvb); capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)\<rbrakk> \<Longrightarrow> \<lbrace>?P95 rv s'' () s''a rvb\<rbrace> getCTE rv \<lbrace>?B102 rv s'' s''a rvb s''b\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); isZombie (cteCap rvb); \<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb))\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'97 rv s'' rva s''a rvb\<rbrace> haskell_assertE (capZombiePtr (cteCap rvb) = slot \<and> capZombiePtr cap \<noteq> slot) [] \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); \<not> isZombie (cteCap rvb)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'92 rv s'' rva s''a rvb\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B78 rv s'' rva\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rvb s. (isNullCap (cteCap rvb) \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)) \<and> (\<not> isNullCap (cteCap rvb) \<longrightarrow> (isZombie (cteCap rvb) \<longrightarrow> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb) \<longrightarrow> ?P95 rv s'' rva s''a rvb s) \<and> (\<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)) \<longrightarrow> ?P'97 rv s'' rva s''a rvb s)) \<and> (\<not> isZombie (cteCap rvb) \<longrightarrow> ?P'92 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 7. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 8. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 9. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' s''a rvb s''b. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s''); (rvb, s''b) \<in> fst (getCTE slot s''a); cteCap rvb \<noteq> capability.NullCap; isZombie (cteCap rvb); capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)\<rbrakk> \<Longrightarrow> \<lbrace>?P95 rv s'' () s''a rvb\<rbrace> getCTE rv \<lbrace>\<lambda>endCTE s. cteCap endCTE = capability.NullCap \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> isZombie (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (capZombieType (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (Suc (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)))) slot s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) + 2 ^ cteSizeBits * word_of_nat (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap))) s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); isZombie (cteCap rvb); \<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb))\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'97 rv s'' rva s''a rvb\<rbrace> haskell_assertE (capZombiePtr (cteCap rvb) = slot \<and> capZombiePtr cap \<noteq> slot) [] \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); \<not> isZombie (cteCap rvb)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'92 rv s'' rva s''a rvb\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B78 rv s'' rva\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rvb s. (isNullCap (cteCap rvb) \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)) \<and> (\<not> isNullCap (cteCap rvb) \<longrightarrow> (isZombie (cteCap rvb) \<longrightarrow> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb) \<longrightarrow> ?P95 rv s'' rva s''a rvb s) \<and> (\<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)) \<longrightarrow> ?P'97 rv s'' rva s''a rvb s)) \<and> (\<not> isZombie (cteCap rvb) \<longrightarrow> ?P'92 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 7. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 8. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); isZombie (cteCap rvb); \<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb))\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'97 rv s'' rva s''a rvb\<rbrace> haskell_assertE (capZombiePtr (cteCap rvb) = slot \<and> capZombiePtr cap \<noteq> slot) [] \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ getCTE slot) s''a); \<not> isNullCap (cteCap rvb); \<not> isZombie (cteCap rvb)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'92 rv s'' rva s''a rvb\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B78 rv s'' rva\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rvb s. (isNullCap (cteCap rvb) \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)) \<and> (\<not> isNullCap (cteCap rvb) \<longrightarrow> (isZombie (cteCap rvb) \<longrightarrow> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb) \<longrightarrow> cte_wp_at' (\<lambda>_. True) rv s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) rv s \<and> (cteCap cte = capability.NullCap \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> isZombie (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (capZombieType (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (Suc (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)))) slot s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) + 2 ^ cteSizeBits * word_of_nat (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap))) s \<and> sch_act_simple s))) \<and> (\<not> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb)) \<longrightarrow> ?P'97 rv s'' rva s''a rvb s)) \<and> (\<not> isZombie (cteCap rvb) \<longrightarrow> ?P'92 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 7. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' s''a. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B78 rv s'' ()\<rbrace> getCTE slot \<lbrace>\<lambda>rvb s. (cteCap rvb = capability.NullCap \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s) \<and> (cteCap rvb \<noteq> capability.NullCap \<longrightarrow> isZombie (cteCap rvb) \<longrightarrow> (capZombiePtr cap = capZombiePtr (cteCap rvb) \<and> capZombieNumber (cteCap rvb) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rvb) \<longrightarrow> cte_wp_at' (\<lambda>_. True) rv s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) rv s \<and> (cteCap cte = capability.NullCap \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> isZombie (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (capZombieType (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (Suc (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)))) slot s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) + 2 ^ cteSizeBits * word_of_nat (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap))) s \<and> sch_act_simple s))) \<and> ((capZombieNumber (cteCap rvb) = capZombieNumber cap \<longrightarrow> capZombiePtr cap = capZombiePtr (cteCap rvb) \<longrightarrow> capZombieType cap \<noteq> capZombieType (cteCap rvb)) \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s))\<rbrace>
 2. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' s''a rva s. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s''); rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> cte_wp_at' (\<lambda>c. c = rva) slot s \<and> invs' s \<and> no_cte_prop Q s \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> (cteCap rva = capability.NullCap \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s) \<and> (cteCap rva \<noteq> capability.NullCap \<longrightarrow> isZombie (cteCap rva) \<longrightarrow> (capZombiePtr cap = capZombiePtr (cteCap rva) \<and> capZombieNumber (cteCap rva) = capZombieNumber cap \<and> capZombieType cap = capZombieType (cteCap rva) \<longrightarrow> cte_wp_at' (\<lambda>_. True) rv s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) rv s \<and> (cteCap cte = capability.NullCap \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> isZombie (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (capZombieType (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)) (Suc (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap)))) slot s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (capZombiePtr (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap) + 2 ^ cteSizeBits * word_of_nat (capZombieNumber (capZombieNumber_update (\<lambda>_. capZombieNumber cap - Suc 0) cap))) s \<and> sch_act_simple s))) \<and> ((capZombieNumber (cteCap rva) = capZombieNumber cap \<longrightarrow> capZombiePtr cap = capZombiePtr (cteCap rva) \<longrightarrow> capZombieType cap \<noteq> capZombieType (cteCap rva)) \<longrightarrow> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s))
 2. \<And>rv s'' s''a. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B78 rv s'' ()\<rbrace> getCTE slot \<lbrace>\<lambda>cte s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> cte_wp_at' (\<lambda>c. c = cte) slot s \<and> invs' s \<and> no_cte_prop Q s \<and> sch_act_simple s\<rbrace>
 3. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (6 subgoals):
 1. \<And>s'' s''a rva s num ptra bitsa cte. \<lbrakk>0 < num; (ptra + word_of_nat num * 2 ^ cteSizeBits - 2 ^ cteSizeBits, s'') \<in> fst (locateSlotCap (capability.Zombie ptra bitsa num) (word_of_nat num - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot (ptra + word_of_nat num * 2 ^ cteSizeBits - 2 ^ cteSizeBits) False;
whenE (fst p) (liftE (emptySlot (ptra + word_of_nat num * 2 ^ cteSizeBits - 2 ^ cteSizeBits) (snd p)))
odE) s''); exposed; cap = capability.Zombie ptra bitsa num; ctes_of s slot = Some rva; invs' s; no_cte_prop Q s; sch_act_simple s; cteCap rva = capability.Zombie ptra bitsa num; ctes_of s (ptra + word_of_nat num * 2 ^ cteSizeBits - 2 ^ cteSizeBits) = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s (ptra + (word_of_nat num - 1) * 2 ^ cteSizeBits) = Some cte \<and> cteCap cte = capability.NullCap
 2. \<And>rv s'' s''a. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B78 rv s'' ()\<rbrace> getCTE slot \<lbrace>\<lambda>cte s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> cte_wp_at' (\<lambda>c. c = cte) slot s \<and> invs' s \<and> no_cte_prop Q s \<and> sch_act_simple s\<rbrace>
 3. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' s''a. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr (), s''a) \<in> fst ((doE p <- finaliseSlot rv False;
whenE (fst p) (liftE (emptySlot rv (snd p)))
odE) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B78 rv s'' ()\<rbrace> getCTE slot \<lbrace>\<lambda>cte s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> cte_wp_at' (\<lambda>c. c = cte) slot s \<and> invs' s \<and> no_cte_prop Q s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> doE p <- finaliseSlot rv False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rv (snd p)
odE \<lbrace>?B78 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); (Inr rva, s''a) \<in> fst (finaliseSlot rv False s''); False \<or> fst rva\<rbrakk> \<Longrightarrow> \<lbrace>?P210 rv s'' rva\<rbrace> withoutPreemption (emptySlot rv (snd rva)) \<lbrace>\<lambda>a b. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' b \<and> no_cte_prop Q b \<and> sch_act_simple b\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> finaliseSlot rv False \<lbrace>\<lambda>a b. (False \<or> fst a \<longrightarrow> ?P210 rv s'' a b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' b \<and> no_cte_prop Q b \<and> sch_act_simple b)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed; (rv, s'') \<in> fst (locateSlotCap cap (word_of_nat (capZombieNumber cap) - 1) st); (Inr rva, s''a) \<in> fst (finaliseSlot rv False s''); fst rva\<rbrakk> \<Longrightarrow> \<lbrace>?P210 rv s'' rva\<rbrace> emptySlot rv (snd rva) \<lbrace>\<lambda>a b. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> invs' b \<and> no_cte_prop Q b \<and> sch_act_simple b\<rbrace>
 2. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> finaliseSlot rv False \<lbrace>\<lambda>a b. (False \<or> fst a \<longrightarrow> ?P210 rv s'' a b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' b \<and> no_cte_prop Q b \<and> sch_act_simple b)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (4 subgoals):
 1. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> finaliseSlot rv False \<lbrace>\<lambda>a b. (False \<or> fst a \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> (invs' b \<and> cte_wp_at' (\<lambda>cte. removeable' rv b (cteCap cte)) rv b \<and> (\<forall>sl'. snd a \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> rv \<longrightarrow> cteCaps_of b sl' \<noteq> Some (snd a))) \<and> (no_cte_prop Q and K (finalise_prop_stuff Q)) b \<and> sch_act_simple b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' b \<and> no_cte_prop Q b \<and> sch_act_simple b)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (5 subgoals):
 1. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B77 rv\<rbrace> finaliseSlot rv False \<lbrace>?Q'236 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s'' s r. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); ?Q'236 rv s'' s r\<rbrakk> \<Longrightarrow> (False \<or> fst s \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> (invs' r \<and> cte_wp_at' (\<lambda>cte. removeable' rv r (cteCap cte)) rv r \<and> (\<forall>sl'. snd s \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> rv \<longrightarrow> cteCaps_of r sl' \<noteq> Some (snd s))) \<and> (no_cte_prop Q and K (finalise_prop_stuff Q)) r \<and> sch_act_simple r) \<and> (\<not> (False \<or> fst s) \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' r \<and> no_cte_prop Q r \<and> sch_act_simple r)
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>?B77\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (6 subgoals):
 1. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> \<lbrace>?P241 rv\<rbrace> finaliseSlot rv False \<lbrace>\<lambda>fc s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits\<rbrace>, -
 2. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'242 rv\<rbrace> finaliseSlot rv False \<lbrace>?Q'239 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<And>rv s'' s r. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ?Q'239 rv s'' s r\<rbrakk> \<Longrightarrow> (False \<or> fst s \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> (invs' r \<and> cte_wp_at' (\<lambda>cte. removeable' rv r (cteCap cte)) rv r \<and> (\<forall>sl'. snd s \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> rv \<longrightarrow> cteCaps_of r sl' \<noteq> Some (snd s))) \<and> (no_cte_prop Q and K (finalise_prop_stuff Q)) r \<and> sch_act_simple r) \<and> (\<not> (False \<or> fst s) \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' r \<and> no_cte_prop Q r \<and> sch_act_simple r)
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>\<lambda>rv s. ?P241 rv s \<and> ?P'242 rv s\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 6. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (5 subgoals):
 1. \<And>rv s''. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'242 rv\<rbrace> finaliseSlot rv False \<lbrace>?Q'239 rv s''\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s'' s r. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ?Q'239 rv s'' s r\<rbrakk> \<Longrightarrow> (False \<or> fst s \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> (invs' r \<and> cte_wp_at' (\<lambda>cte. removeable' rv r (cteCap cte)) rv r \<and> (\<forall>sl'. snd s \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> rv \<longrightarrow> cteCaps_of r sl' \<noteq> Some (snd s))) \<and> (no_cte_prop Q and K (finalise_prop_stuff Q)) r \<and> sch_act_simple r) \<and> (\<not> (False \<or> fst s) \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' r \<and> no_cte_prop Q r \<and> sch_act_simple r)
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>\<lambda>rv s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ?P'242 rv s\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 5. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' s r. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) st); rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> no_cte_prop Q r \<and> invs' r \<and> sch_act_simple r \<and> (fst s \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' rv r (cteCap cte)) rv r) \<and> (\<forall>sl'. snd s \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> rv \<longrightarrow> cteCaps_of r sl' \<noteq> Some (snd s))\<rbrakk> \<Longrightarrow> (False \<or> fst s \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> (invs' r \<and> cte_wp_at' (\<lambda>cte. removeable' rv r (cteCap cte)) rv r \<and> (\<forall>sl'. snd s \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> rv \<longrightarrow> cteCaps_of r sl' \<noteq> Some (snd s))) \<and> (no_cte_prop Q and K (finalise_prop_stuff Q)) r \<and> sch_act_simple r) \<and> (\<not> (False \<or> fst s) \<longrightarrow> rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> True \<and> invs' r \<and> no_cte_prop Q r \<and> sch_act_simple r)
 2. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>\<lambda>rv s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) rv s\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 4. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1)) \<lbrace>\<lambda>rv s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) rv s\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < capZombieNumber cap; isZombie cap \<and> exposed\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P76\<rbrace> liftE (do x <- stateAssert (\<lambda>s. (isCNodeCap cap \<or> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap cap \<and> n = capCNodeBits cap \<or> n = zombieCTEBits (capZombieType cap)) \<and> word_of_nat (capZombieNumber cap) - 1 < 2 ^ n) \<or> isThreadCap cap \<or> capZombieType cap = ZombieTCB) [];
return (global.capUntypedPtr cap + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber cap) - 1))
od) \<lbrace>\<lambda>rv s. rv = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) rv s\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); \<not> (isZombie cap \<and> exposed)\<rbrakk> \<Longrightarrow> st \<turnstile> \<lbrace>?P'76\<rbrace> fail \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s)\<rbrace>, \<lbrace>\<lambda>rv s. no_cte_prop Q s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 3. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a b. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q b \<and> invs' b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> sch_act_simple b \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot b \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot b) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p b))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> ?P76 st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> ?P'76 st))) proof (prove)
goal (1 subgoal):
 1. no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot st \<and> (exposed \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p st) \<Longrightarrow> (isZombie cap \<and> capZombieNumber cap = 0 \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> capZombieNumber cap = 0) \<longrightarrow> (isZombie cap \<and> \<not> exposed \<longrightarrow> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr cap) st \<longrightarrow> ((\<lambda>a aa. (isZombie a \<longrightarrow> capZombiePtr a \<noteq> capZombiePtr cap) \<longrightarrow> no_cte_prop Q aa \<and> invs' aa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr cap) aa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot aa \<and> sch_act_simple aa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot aa \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie (capZombiePtr cap) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr cap))) slot aa) \<and> (p \<noteq> capZombiePtr cap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> isZombie (cteCap c) \<or> (\<exists>zb n. cteCap c = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p aa))) \<circ> cteCap) cte st)) \<and> (\<not> (isZombie cap \<and> \<not> exposed) \<longrightarrow> (isZombie cap \<and> exposed \<longrightarrow> (isCNodeCap cap \<or> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap cap \<and> n = capCNodeBits cap \<or> n = zombieCTEBits (capZombieType cap)) \<and> word_of_nat (capZombieNumber cap) - 1 < 2 ^ n) \<or> isThreadCap cap \<or> capZombieType cap = ZombieTCB \<longrightarrow> global.capUntypedPtr cap + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber cap) - 1) = capZombiePtr cap + word_of_nat (capZombieNumber cap) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> no_cte_prop Q st \<and> invs' st \<and> sch_act_simple st \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot st \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr cap + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber cap) - 1)) st) \<and> (\<not> (isZombie cap \<and> exposed) \<longrightarrow> True))) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<and> \<not> exposed \<longrightarrow> (\<forall>ctea. ctes_of st (capZombiePtr (cteCap cte)) = Some ctea \<longrightarrow> (isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> capZombiePtr (cteCap cte)) \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr (cteCap cte)) st \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot st \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr (cteCap cte) \<longrightarrow> P (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie (capZombiePtr (cteCap cte)) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr (cteCap cte)))) \<and> (p \<noteq> capZombiePtr (cteCap cte) \<longrightarrow> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))))))) \<and> ((isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> isZombie (cteCap cte) \<and> \<not> exposed \<longrightarrow> (\<forall>ctea. ctes_of st (capZombiePtr (cteCap cte)) = Some ctea \<longrightarrow> (isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> capZombiePtr (cteCap cte)) \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) (capZombiePtr (cteCap cte)) st \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot st \<and> (p = slot \<or> p \<noteq> slot \<and> (p = capZombiePtr (cteCap cte) \<longrightarrow> P (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie (capZombiePtr (cteCap cte)) zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> capZombiePtr (cteCap cte)))) \<and> (p \<noteq> capZombiePtr (cteCap cte) \<longrightarrow> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))))))
 2. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; ctes_of st slot = Some cte; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr st \<and> (p = slot \<or> p \<noteq> slot \<and> (p = ptr \<longrightarrow> P (capability.Zombie ptr bits num) \<or> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> ptr))) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))))
 2. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) proof (prove)
goal (3 subgoals):
 1. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; ctes_of st slot = Some cte; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr st
 2. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; ctes_of st slot = Some cte; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> p = slot \<or> p \<noteq> slot \<and> (p = ptr \<longrightarrow> P (capability.Zombie ptr bits num) \<or> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> ptr))) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))))
 3. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) proof (prove)
goal (4 subgoals):
 1. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> num \<noteq> 0
 2. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> valid_objs' st
 3. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; ctes_of st slot = Some cte; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> p = slot \<or> p \<noteq> slot \<and> (p = ptr \<longrightarrow> P (capability.Zombie ptr bits num) \<or> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> ptr))) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))))
 4. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) proof (prove)
goal (3 subgoals):
 1. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> valid_objs' st
 2. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; ctes_of st slot = Some cte; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> p = slot \<or> p \<noteq> slot \<and> (p = ptr \<longrightarrow> P (capability.Zombie ptr bits num) \<or> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> ptr))) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))))
 3. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) proof (prove)
goal (2 subgoals):
 1. \<And>cte ctea ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; ctes_of st slot = Some cte; cap = capability.Zombie ptr bits num; 0 < num; \<not> exposed; cteCap cte = capability.Zombie ptr bits num; ctes_of st ptr = Some ctea; isZombie (cteCap ctea) \<longrightarrow> capZombiePtr (cteCap ctea) \<noteq> ptr; ex_cte_cap_wp_to' (\<lambda>_. True) slot st; p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))))\<rbrakk> \<Longrightarrow> p = slot \<or> p \<noteq> slot \<and> (p = ptr \<longrightarrow> P (capability.Zombie ptr bits num) \<or> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> ptr))) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))))
 2. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot st; exposed \<or> p = slot \<or> (\<exists>cte. ctes_of st p = Some cte \<and> (P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)))); ctes_of st slot = Some cte; cap = cteCap cte; isZombie (cteCap cte) \<longrightarrow> 0 < capZombieNumber (cteCap cte)\<rbrakk> \<Longrightarrow> (isZombie (cteCap cte) \<longrightarrow> exposed) \<longrightarrow> isZombie (cteCap cte) \<and> exposed \<longrightarrow> ((isCNodeCap (cteCap cte) \<or> capZombieType (cteCap cte) \<noteq> ZombieTCB) \<and> (case gsCNodes st (global.capUntypedPtr (cteCap cte)) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (cteCap cte) \<and> n = capCNodeBits (cteCap cte) \<or> n = zombieCTEBits (capZombieType (cteCap cte))) \<and> word_of_nat (capZombieNumber (cteCap cte)) - 1 < 2 ^ n) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (isThreadCap (cteCap cte) \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) \<and> (capZombieType (cteCap cte) = ZombieTCB \<longrightarrow> global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1) = capZombiePtr (cteCap cte) + word_of_nat (capZombieNumber (cteCap cte)) * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (global.capUntypedPtr (cteCap cte) + 2 ^ cte_level_bits * (word_of_nat (capZombieNumber (cteCap cte)) - 1)) st) proof (prove)
goal (1 subgoal):
 1. \<And>cte ptr bits num. \<lbrakk>no_cte_prop Q st; invs' st; sch_act_simple st; ctes_of st slot = Some cte; cap = capability.Zombie ptr bits num; 0 < num; exposed; cteCap cte = capability.Zombie ptr bits num\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.Zombie ptr bits num) \<or> bits \<noteq> ZombieTCB) \<and> (case gsCNodes st ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie ptr bits num) \<and> n = capCNodeBits (capability.Zombie ptr bits num) \<or> n = zombieCTEBits bits) \<and> word_of_nat num - 1 < 2 ^ n) \<longrightarrow> 2 ^ cte_level_bits * (word_of_nat num - 1) = word_of_nat num * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * (word_of_nat num - 1)) st) \<and> (isThreadCap (capability.Zombie ptr bits num) \<longrightarrow> 2 ^ cte_level_bits * (word_of_nat num - 1) = word_of_nat num * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * (word_of_nat num - 1)) st) \<and> (bits = ZombieTCB \<longrightarrow> 2 ^ cte_level_bits * (word_of_nat num - 1) = word_of_nat num * 2 ^ cteSizeBits - 2 ^ cteSizeBits \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * (word_of_nat num - 1)) st) proof (prove)
goal:
No subgoals!