theory CNodeInv_R

lemma finaliseSlot_abort_cases':
  "s \<turnstile> \<lbrace>\<top>\<rbrace>
     finaliseSlot' sl ex
   \<lbrace>\<lambda>rv s. fst rv \<or> (\<not> ex \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)
                                \<and> capZombiePtr (cteCap cte) = sl) sl s)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" proof (induct rule: finalise_spec_induct) case (1 slot exp) show ?case apply (subst finaliseSlot'_simps_ext) apply (simp only: split_def) apply (rule hoare_pre_spec_validE) apply (wp | simp)+ apply ((wp "1.hyps" updateCap_cte_wp_at_cases)+,
                 (assumption | rule refl | simp only: split_def fst_conv snd_conv)+) apply (wp | simp)+ apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift[where Q="\<lambda>rv. cte_at' slot"]) apply (wp typ_at_lifts [OF finaliseCap_typ_at'])[1] apply (rule finaliseCap_cases) apply (clarsimp simp: cte_wp_at_ctes_of) apply (wp getCTE_wp isFinalCapability_inv | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> finaliseSlot' sl ex \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = sl) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>x b s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc xa xb y xaa xab xac v sa s'. \<lbrakk>(Inr rv, st) \<in> fst ((withoutPreemption $ getCTE x) s); \<not> (isNullCap $ cteCap rv); (Inr rva, sta) \<in> fst ((withoutPreemption $ isFinalCapability rv) st); (Inr rvb, stb) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) sta); \<not> capRemovable (fst rvb) x; \<not> (\<not> b \<and> capCyclicZombie (fst rvb) x); (Inr rvc, stc) \<in> fst ((withoutPreemption $ updateCap x (fst rvb)) stb); xa = (fst rvb, b); (xb, y) = xa; \<not> (isZombie xb \<and> capZombieNumber xb = 0); \<not> (isZombie xb \<and> \<not> y); isZombie xb \<and> y; xaa = xb; xab = capZombiePtr xaa; xac = capZombieNumber xaa; (Inr v, s') \<in> fst ((withoutPreemption $ locateSlotCap xaa (fromIntegral (xac - 1))) sa)\<rbrakk> \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' v False \<lbrace>\<lambda>a aa. fst a \<or> \<not> False \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = v) v aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, st) \<in> fst ((withoutPreemption $ getCTE x) s); \<not> (isNullCap $ cteCap rv); (Inr rva, sta) \<in> fst ((withoutPreemption $ isFinalCapability rv) st); (Inr rvb, stb) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) sta); \<not> capRemovable (fst rvb) x; \<not> (\<not> b \<and> capCyclicZombie (fst rvb) x); (Inr rvc, stc) \<in> fst ((withoutPreemption $ updateCap x (fst rvb)) stb); (Inr rvd, std) \<in> fst ((let (v33, v34) = (fst rvb, b) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> x) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr x
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE x;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap x
od else haskell_assertE (ptr2 = x \<and> ptr \<noteq> x) [] else haskell_fail []
odE else haskell_fail []) stc); (Inr rve, ste) \<in> fst (preemptionPoint std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a aa. fst a \<or> \<not> b \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = x) x aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a aa. fst a \<or> \<not> b \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = x) x aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap ?rv); (Inr ?rva, ?sta) \<in> fst ((withoutPreemption $ isFinalCapability ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap ?rv) ?rva False) ?sta); \<not> capRemovable (fst ?rvb) slot; \<not> (\<not> exp \<and> capCyclicZombie (fst ?rvb) slot); (Inr ?rvc, ?stc) \<in> fst ((withoutPreemption $ updateCap slot (fst ?rvb)) ?stb); ?xa = (fst ?rvb, exp); (?xb, ?y) = ?xa; \<not> (isZombie ?xb \<and> capZombieNumber ?xb = 0); \<not> (isZombie ?xb \<and> \<not> ?y); isZombie ?xb \<and> ?y; ?xaa = ?xb; ?xab = capZombiePtr ?xaa; ?xac = capZombieNumber ?xaa; (Inr ?v, ?s') \<in> fst ((withoutPreemption $ locateSlotCap ?xaa (fromIntegral (?xac - 1))) ?sa)\<rbrakk> \<Longrightarrow> ?s' \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' ?v False \<lbrace>\<lambda>a b. fst a \<or> \<not> False \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ?v) ?v b\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap ?rv); (Inr ?rva, ?sta) \<in> fst ((withoutPreemption $ isFinalCapability ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap ?rv) ?rva False) ?sta); \<not> capRemovable (fst ?rvb) slot; \<not> (\<not> exp \<and> capCyclicZombie (fst ?rvb) slot); (Inr ?rvc, ?stc) \<in> fst ((withoutPreemption $ updateCap slot (fst ?rvb)) ?stb); (Inr ?rvd, ?std) \<in> fst ((let (v33, v34) = (fst ?rvb, exp) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail []) ?stc); (Inr ?rve, ?ste) \<in> fst (preemptionPoint ?std)\<rbrakk> \<Longrightarrow> ?ste \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' slot exp \<lbrace>\<lambda>a aa. fst a \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>

goal (1 subgoal):
 1. \<And>x b s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc xa xb y xaa xab xac v sa s'. \<lbrakk>(Inr rv, st) \<in> fst ((withoutPreemption $ getCTE x) s); \<not> (isNullCap $ cteCap rv); (Inr rva, sta) \<in> fst ((withoutPreemption $ isFinalCapability rv) st); (Inr rvb, stb) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) sta); \<not> capRemovable (fst rvb) x; \<not> (\<not> b \<and> capCyclicZombie (fst rvb) x); (Inr rvc, stc) \<in> fst ((withoutPreemption $ updateCap x (fst rvb)) stb); xa = (fst rvb, b); (xb, y) = xa; \<not> (isZombie xb \<and> capZombieNumber xb = 0); \<not> (isZombie xb \<and> \<not> y); isZombie xb \<and> y; xaa = xb; xab = capZombiePtr xaa; xac = capZombieNumber xaa; (Inr v, s') \<in> fst ((withoutPreemption $ locateSlotCap xaa (fromIntegral (xac - 1))) sa)\<rbrakk> \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' v False \<lbrace>\<lambda>a aa. fst a \<or> \<not> False \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = v) v aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, st) \<in> fst ((withoutPreemption $ getCTE x) s); \<not> (isNullCap $ cteCap rv); (Inr rva, sta) \<in> fst ((withoutPreemption $ isFinalCapability rv) st); (Inr rvb, stb) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) sta); \<not> capRemovable (fst rvb) x; \<not> (\<not> b \<and> capCyclicZombie (fst rvb) x); (Inr rvc, stc) \<in> fst ((withoutPreemption $ updateCap x (fst rvb)) stb); (Inr rvd, std) \<in> fst ((let (v33, v34) = (fst rvb, b) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> x) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr x
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE x;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap x
od else haskell_assertE (ptr2 = x \<and> ptr \<noteq> x) [] else haskell_fail []
odE else haskell_fail []) stc); (Inr rve, ste) \<in> fst (preemptionPoint std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a aa. fst a \<or> \<not> b \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = x) x aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a aa. fst a \<or> \<not> b \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = x) x aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' slot exp \<lbrace>\<lambda>a b. fst a \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot b\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> doE cte <- withoutPreemption $ getCTE slot;
if isNullCap $ cteCap cte then returnOk (True, capability.NullCap) else doE final <- withoutPreemption $ isFinalCapability cte;
(remainder, info) <- withoutPreemption $ global.finaliseCap (cteCap cte) final False;
if capRemovable remainder slot then returnOk (True, info) else if \<not> exp \<and> capCyclicZombie remainder slot then doE withoutPreemption $ updateCap slot remainder;
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap slot remainder;
let (v33, v34) = (remainder, exp) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot exp
odE
odE
odE \<lbrace>\<lambda>a aa. fst a \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> doE cte <- withoutPreemption $ getCTE slot;
if isNullCap $ cteCap cte then returnOk (True, capability.NullCap) else doE final <- withoutPreemption $ isFinalCapability cte;
p <- withoutPreemption $ global.finaliseCap (cteCap cte) final False;
if capRemovable (fst p) slot then returnOk (True, snd p) else if \<not> exp \<and> capCyclicZombie (fst p) slot then doE withoutPreemption $ updateCap slot (fst p);
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap slot (fst p);
let p = (fst p, exp) in if isZombie (fst p) \<and> capZombieNumber (fst p) = 0 then haskell_fail [] else if isZombie (fst p) \<and> \<not> snd p then let ptr = capZombiePtr (fst p) in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie (fst p) \<and> snd p then let z = fst p; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot exp
odE
odE
odE \<lbrace>\<lambda>a aa. fst a \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. s_ \<turnstile> \<lbrace>?P'\<rbrace> doE cte <- withoutPreemption $ getCTE slot;
if isNullCap $ cteCap cte then returnOk (True, capability.NullCap) else doE final <- withoutPreemption $ isFinalCapability cte;
p <- withoutPreemption $ global.finaliseCap (cteCap cte) final False;
if capRemovable (fst p) slot then returnOk (True, snd p) else if \<not> exp \<and> capCyclicZombie (fst p) slot then doE withoutPreemption $ updateCap slot (fst p);
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap slot (fst p);
let p = (fst p, exp) in if isZombie (fst p) \<and> capZombieNumber (fst p) = 0 then haskell_fail [] else if isZombie (fst p) \<and> \<not> snd p then let ptr = capZombiePtr (fst p) in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie (fst p) \<and> snd p then let z = fst p; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot exp
odE
odE
odE \<lbrace>\<lambda>a aa. fst a \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. True \<Longrightarrow> ?P' s_ proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s''); (rvb, s''b) \<in> fst (global.finaliseCap (cteCap rv) rva False s''a); \<not> capRemovable (fst rvb) slot; \<not> exp \<and> capCyclicZombie (fst rvb) slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'50 rv s'' rva s''a rvb\<rbrace> updateCap slot (fst rvb) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) s''a); \<not> capRemovable (fst rvb) slot; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) slot)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> doE withoutPreemption $ updateCap slot (fst rvb);
let p = (fst rvb, exp) in if isZombie (fst p) \<and> capZombieNumber (fst p) = 0 then haskell_fail [] else if isZombie (fst p) \<and> \<not> snd p then let ptr = capZombiePtr (fst p) in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie (fst p) \<and> snd p then let z = fst p; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot exp
odE \<lbrace>\<lambda>a aa. fst a \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot aa\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) slot \<longrightarrow> True \<and> (fst (True, snd rvb) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> capRemovable (fst rvb) slot \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) slot \<longrightarrow> True \<and> True \<and> ?P'50 rv s'' rva s''a rvb s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) slot) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 5. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 6. True \<Longrightarrow> ?P' s_ proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) s''a); \<not> capRemovable (fst rvb) slot; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) slot); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap slot (fst rvb)) s''b); (Inr rvd, s''d) \<in> fst ((let p = (fst rvb, exp) in if isZombie (fst p) \<and> capZombieNumber (fst p) = 0 then haskell_fail [] else if isZombie (fst p) \<and> \<not> snd p then let ptr = capZombiePtr (fst p) in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie (fst p) \<and> snd p then let z = fst p; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail []) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B72 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemptionPoint \<lbrace>\<lambda>rve a. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) s''a); \<not> capRemovable (fst rvb) slot; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) slot); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap slot (fst rvb)) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B70 rv s'' rva s''a rvb s''b rvc\<rbrace> let p = (fst rvb, exp) in if isZombie (fst p) \<and> capZombieNumber (fst p) = 0 then haskell_fail [] else if isZombie (fst p) \<and> \<not> snd p then let ptr = capZombiePtr (fst p) in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie (fst p) \<and> snd p then let z = fst p; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [] \<lbrace>?B72 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s''); (Inr rvb, s''b) \<in> fst ((withoutPreemption $ global.finaliseCap (cteCap rv) rva False) s''a); \<not> capRemovable (fst rvb) slot; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) slot)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap slot (fst rvb) \<lbrace>?B70 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) slot \<longrightarrow> True \<and> (fst (True, snd rvb) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> capRemovable (fst rvb) slot \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) slot \<longrightarrow> True \<and> True \<and> (slot = slot \<longrightarrow> cte_wp_at' ((\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) \<circ> cteCap_update (K (fst rvb))) slot s) \<and> (slot \<noteq> slot \<longrightarrow> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) slot) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 6. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 7. True \<Longrightarrow> ?P' s_ proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'123 rv s'' rva\<rbrace> global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. \<not> capRemovable (fst rvb) slot \<longrightarrow> \<not> exp \<and> capCyclicZombie (fst rvb) slot \<longrightarrow> cte_wp_at' ((\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) \<circ> cteCap_update (\<lambda>y. fst rvb)) slot s\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>\<lambda>rva s. True \<and> ?P'123 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. True \<Longrightarrow> ?P' s_ proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'123 rv s'' rva\<rbrace> global.finaliseCap (cteCap rv) rva False \<lbrace>?Q135 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s''); ?Q135 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> \<not> capRemovable (fst rvb) slot \<longrightarrow> \<not> exp \<and> capCyclicZombie (fst rvb) slot \<longrightarrow> cte_wp_at' ((\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) \<circ> cteCap_update (\<lambda>y. fst rvb)) slot s
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>\<lambda>rva s. True \<and> ?P'123 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 5. True \<Longrightarrow> ?P' s_ proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P139 rv s'' rva\<rbrace> global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) slot\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'140 rv s'' rva\<rbrace> global.finaliseCap (cteCap rv) rva False \<lbrace>?Q'138 rv s'' rva s''a\<rbrace>
 3. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s''); cte_wp_at' (\<lambda>_. True) slot s \<and> ?Q'138 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> \<not> capRemovable (fst rvb) slot \<longrightarrow> \<not> exp \<and> capCyclicZombie (fst rvb) slot \<longrightarrow> cte_wp_at' ((\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) \<circ> cteCap_update (\<lambda>y. fst rvb)) slot s
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>\<lambda>rva s. True \<and> ?P139 rv s'' rva s \<and> ?P'140 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 5. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 6. True \<Longrightarrow> ?P' s_ proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'140 rv s'' rva\<rbrace> global.finaliseCap (cteCap rv) rva False \<lbrace>?Q'138 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s''); cte_wp_at' (\<lambda>_. True) slot s \<and> ?Q'138 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> \<not> capRemovable (fst rvb) slot \<longrightarrow> \<not> exp \<and> capCyclicZombie (fst rvb) slot \<longrightarrow> cte_wp_at' ((\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) \<circ> cteCap_update (\<lambda>y. fst rvb)) slot s
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>\<lambda>rva s. True \<and> cte_wp_at' (\<lambda>_. True) slot s \<and> ?P'140 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 5. True \<Longrightarrow> ?P' s_ proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (getCTE slot s_); cteCap rv \<noteq> capability.NullCap; (rva, s''a) \<in> fst (isFinalCapability rv s''); cte_wp_at' (\<lambda>_. True) slot s \<and> (fst rvb = capability.NullCap \<and> (snd rvb \<noteq> capability.NullCap \<longrightarrow> rva \<and> cap_has_cleanup' (cteCap rv) \<and> snd rvb = cteCap rv) \<or> isZombie (fst rvb) \<and> rva \<and> \<not> False \<and> snd rvb = capability.NullCap \<and> global.capUntypedPtr (fst rvb) = global.capUntypedPtr (cteCap rv) \<and> (isThreadCap (cteCap rv) \<or> isCNodeCap (cteCap rv) \<or> isZombie (cteCap rv)))\<rbrakk> \<Longrightarrow> \<not> capRemovable (fst rvb) slot \<longrightarrow> \<not> exp \<and> capCyclicZombie (fst rvb) slot \<longrightarrow> cte_wp_at' ((\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) \<circ> cteCap_update (\<lambda>y. fst rvb)) slot s
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>\<lambda>rva s. True \<and> cte_wp_at' (\<lambda>_. True) slot s \<and> True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. True \<Longrightarrow> ?P' s_ proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE slot) s_); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>\<lambda>rva s. True \<and> cte_wp_at' (\<lambda>_. True) slot s \<and> True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. s_ \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE slot \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> True \<and> (fst (True, capability.NullCap) \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s)) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. True \<Longrightarrow> ?P' s_ proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>_. True) slot s_ \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s_) proof (prove)
goal:
No subgoals! proof (state)
this:
s_ \<turnstile> \<lbrace>\<lambda>a. True\<rbrace> finaliseSlot' slot exp \<lbrace>\<lambda>a b. fst a \<or> \<not> exp \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot b\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>

goal:
No subgoals!