theory CNodeInv_R

lemma finaliseSlot'_preservation:
  assumes wp:
    "\<And>cap final. \<lbrace>P\<rbrace> finaliseCap cap final False \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl opt. \<lbrace>P\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl1 sl2. \<lbrace>P\<rbrace> capSwapForDelete sl1 sl2 \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl cap. \<lbrace>P\<rbrace> updateCap sl cap \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s"
  assumes irq: "irq_state_independent_H P"
  shows
    "st \<turnstile> \<lbrace>P\<rbrace> finaliseSlot' slot exposed \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>" proof (induct rule: finalise_spec_induct) case (1 sl exp s) show ?case apply (rule hoare_pre_spec_validE) apply (subst finaliseSlot'_simps_ext) apply (simp only: split_def) apply wp apply (simp, wp wp) apply (wp "1.hyps") apply (unfold Let_def split_def fst_conv snd_conv
                        case_Zombie_assert_fold haskell_fail_def) apply (wp wp preemptionPoint_inv| simp add: o_def irq)+ apply (wp hoare_drop_imps) apply (wp wp | simp)+ apply (wp hoare_drop_imps | simp(no_asm))+ apply (wp wp)[1] apply (simp(no_asm)) apply (rule "1.hyps", (assumption | rule refl)+) apply (wp wp hoare_drop_imps isFinalCapability_inv
                    | simp add: locateSlot_conv)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st \<turnstile> \<lbrace>P\<rbrace> finaliseSlot' slot exposed \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<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>P\<rbrace> finaliseSlot' v False \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<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>P\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst ?rvb) sl); (Inr ?rvc, ?stc) \<in> fst ((withoutPreemption $ updateCap sl (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>P\<rbrace> finaliseSlot' ?v False \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst ?rvb) sl); (Inr ?rvc, ?stc) \<in> fst ((withoutPreemption $ updateCap sl (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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail []) ?stc); (Inr ?rve, ?ste) \<in> fst (preemptionPoint ?std)\<rbrakk> \<Longrightarrow> ?ste \<turnstile> \<lbrace>P\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<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>P\<rbrace> finaliseSlot' v False \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<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>P\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. P s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE cte <- withoutPreemption $ getCTE sl;
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 sl then returnOk (True, info) else if \<not> exp \<and> capCyclicZombie remainder sl then doE withoutPreemption $ updateCap sl remainder;
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap sl 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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' sl exp
odE
odE
odE \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. P s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE cte <- withoutPreemption $ getCTE sl;
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) sl then returnOk (True, snd p) else if \<not> exp \<and> capCyclicZombie (fst p) sl then doE withoutPreemption $ updateCap sl (fst p);
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap sl (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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' sl exp
odE
odE
odE \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. P s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> exp \<and> capCyclicZombie (fst rvb) sl\<rbrakk> \<Longrightarrow> \<lbrace>?P26 rv s'' rva s''a rvb\<rbrace> withoutPreemption (updateCap sl (fst rvb)) \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> doE withoutPreemption $ updateCap sl (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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' sl exp
odE \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> ?P26 rv s'' rva s''a rvb s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. P s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> doE withoutPreemption $ updateCap sl (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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' sl exp
odE \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. P s \<Longrightarrow> ?P' s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail []) s''c); (Inr rve, s''e) \<in> fst (preemptionPoint s''d)\<rbrakk> \<Longrightarrow> (Inr (?rvd46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), ?std46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e) \<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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail []) s''c)
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail []) s''c); (Inr rve, s''e) \<in> fst (preemptionPoint s''d)\<rbrakk> \<Longrightarrow> (Inr (?rve46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), s''e) \<in> fst (preemptionPoint (?std46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e))
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail []) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B42 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemptionPoint \<lbrace>\<lambda>rve. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B40 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> sl) [];
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 sl
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 sl;
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 sl
od else haskell_assertE (ptr2 = sl \<and> ptr \<noteq> sl) [] else haskell_fail []
odE else haskell_fail [] \<lbrace>?B42 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>?B40 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 9. P s \<Longrightarrow> ?P' s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); (Inr rvd, s''d) \<in> fst ((if isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 then fail else if isZombie (fst rvb) \<and> \<not> exp then doE haskell_assertE (capZombiePtr (fst rvb) \<noteq> sl) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr (fst rvb));
assertE (isZombie capAtPtr \<longrightarrow> capZombiePtr capAtPtr \<noteq> capZombiePtr (fst rvb));
withoutPreemption $ capSwapForDelete (capZombiePtr (fst rvb)) sl
odE else if isZombie (fst rvb) \<and> exp then doE endSlot <- withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE sl;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst rvb) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst rvb) - 1) (fst rvb)) >>= updateCap sl
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] else fail
odE else fail) s''c); (Inr rve, s''e) \<in> fst (preemptionPoint s''d)\<rbrakk> \<Longrightarrow> (Inr (?rvd46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), ?std46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e) \<in> fst ((if isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 then fail else if isZombie (fst rvb) \<and> \<not> exp then doE haskell_assertE (capZombiePtr (fst rvb) \<noteq> sl) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr (fst rvb));
assertE (isZombie capAtPtr \<longrightarrow> capZombiePtr capAtPtr \<noteq> capZombiePtr (fst rvb));
withoutPreemption $ capSwapForDelete (capZombiePtr (fst rvb)) sl
odE else if isZombie (fst rvb) \<and> exp then doE endSlot <- withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE sl;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst rvb) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst rvb) - 1) (fst rvb)) >>= updateCap sl
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] else fail
odE else fail) s''c)
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); (Inr rvd, s''d) \<in> fst ((if isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 then fail else if isZombie (fst rvb) \<and> \<not> exp then doE haskell_assertE (capZombiePtr (fst rvb) \<noteq> sl) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr (fst rvb));
assertE (isZombie capAtPtr \<longrightarrow> capZombiePtr capAtPtr \<noteq> capZombiePtr (fst rvb));
withoutPreemption $ capSwapForDelete (capZombiePtr (fst rvb)) sl
odE else if isZombie (fst rvb) \<and> exp then doE endSlot <- withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE sl;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst rvb) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst rvb) - 1) (fst rvb)) >>= updateCap sl
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] else fail
odE else fail) s''c); (Inr rve, s''e) \<in> fst (preemptionPoint s''d)\<rbrakk> \<Longrightarrow> (Inr (?rve46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), s''e) \<in> fst (preemptionPoint (?std46 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e))
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); (Inr rvd, s''d) \<in> fst ((if isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 then fail else if isZombie (fst rvb) \<and> \<not> exp then doE haskell_assertE (capZombiePtr (fst rvb) \<noteq> sl) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr (fst rvb));
assertE (isZombie capAtPtr \<longrightarrow> capZombiePtr capAtPtr \<noteq> capZombiePtr (fst rvb));
withoutPreemption $ capSwapForDelete (capZombiePtr (fst rvb)) sl
odE else if isZombie (fst rvb) \<and> exp then doE endSlot <- withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE sl;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst rvb) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst rvb) - 1) (fst rvb)) >>= updateCap sl
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] else fail
odE else fail) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B42 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemptionPoint \<lbrace>\<lambda>rve. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B40 rv s'' rva s''a rvb s''b rvc\<rbrace> if isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 then fail else if isZombie (fst rvb) \<and> \<not> exp then doE haskell_assertE (capZombiePtr (fst rvb) \<noteq> sl) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE (capZombiePtr (fst rvb));
assertE (isZombie capAtPtr \<longrightarrow> capZombiePtr capAtPtr \<noteq> capZombiePtr (fst rvb));
withoutPreemption $ capSwapForDelete (capZombiePtr (fst rvb)) sl
odE else if isZombie (fst rvb) \<and> exp then doE endSlot <- withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE sl;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst rvb) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst rvb) - 1) (fst rvb)) >>= updateCap sl
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] else fail
odE else fail \<lbrace>?B42 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>?B40 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 9. P s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c s''d. \<lbrakk>(rv, s'') \<in> fst (getCTE sl 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) sl; \<not> capCyclicZombie (fst rvb) sl; ((), s''c) \<in> fst (updateCap sl (fst rvb) s''b); 0 < capZombieNumber (fst rvb); isZombie (fst rvb) \<and> \<not> exp; (Inr (), s''d) \<in> fst (assertE (capZombiePtr (fst rvb) \<noteq> sl) s''c)\<rbrakk> \<Longrightarrow> \<lbrace>?B89 rv s'' rva s''a rvb s''b () s''c ()\<rbrace> getCTE (capZombiePtr (fst rvb)) \<lbrace>\<lambda>x a. (isZombie (cteCap x) \<longrightarrow> capZombiePtr (cteCap x) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> P a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); isZombie (fst rvb) \<and> \<not> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P86 rv s'' rva s''a rvb s''b rvc\<rbrace> haskell_assertE (capZombiePtr (fst rvb) \<noteq> sl) [] \<lbrace>?B89 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'88 rv s'' rva s''a rvb s''b rvc\<rbrace> if isZombie (fst rvb) \<and> exp then doE endSlot <- withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE sl;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst rvb) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst rvb) - 1) (fst rvb)) >>= updateCap sl
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] else fail
odE else fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>\<lambda>rvc s. (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 \<longrightarrow> True) \<and> (\<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0) \<longrightarrow> (isZombie (fst rvb) \<and> \<not> exp \<longrightarrow> ?P86 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> ?P'88 rv s'' rva s''a rvb s''b rvc s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 8. P s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); isZombie (fst rvb) \<and> \<not> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P86 rv s'' rva s''a rvb s''b rvc\<rbrace> haskell_assertE (capZombiePtr (fst rvb) \<noteq> sl) [] \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'88 rv s'' rva s''a rvb s''b rvc\<rbrace> if isZombie (fst rvb) \<and> exp then doE endSlot <- withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1));
doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot endSlot (snd p)
odE;
ourCTE <- withoutPreemption $ getCTE sl;
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst rvb) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap ourCTE) then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst rvb) - 1) (fst rvb)) >>= updateCap sl
od else haskell_assertE (capZombiePtr (cteCap ourCTE) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] else fail
odE else fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>\<lambda>rvc s. (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 \<longrightarrow> True) \<and> (\<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0) \<longrightarrow> (isZombie (fst rvb) \<and> \<not> exp \<longrightarrow> ?P86 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> ?P'88 rv s'' rva s''a rvb s''b rvc s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. P s \<Longrightarrow> ?P' s proof (prove)
goal (12 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d s''e rvf s''f. \<lbrakk>(rv, s'') \<in> fst (getCTE sl 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) sl; ((), s''c) \<in> fst (updateCap sl (fst rvb) s''b); 0 < capZombieNumber (fst rvb); isZombie (fst rvb) \<and> exp; (rvd, s''d) \<in> fst (locateSlotCap (fst rvb) (word_of_nat (capZombieNumber (fst rvb)) - 1) s''c); (Inr (), s''e) \<in> fst ((doE p <- finaliseSlot' rvd False;
whenE (fst p) (liftE (emptySlot rvd (snd p)))
odE) s''d); (rvf, s''f) \<in> fst (getCTE sl s''e); cteCap rvf \<noteq> capability.NullCap; isZombie (cteCap rvf); capZombiePtr (fst rvb) = capZombiePtr (cteCap rvf) \<and> capZombieNumber (cteCap rvf) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap rvf)\<rbrakk> \<Longrightarrow> \<lbrace>?P150 rv s'' rva s''a rvb s''b () s''c rvd s''d () s''e rvf\<rbrace> getCTE rvd \<lbrace>\<lambda>endCTE s. cteCap endCTE = capability.NullCap \<longrightarrow> P s\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s''f. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c); (Inr rve, s''e) \<in> fst ((doE p <- finaliseSlot' rvd False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rvd (snd p)
odE) s''d); (Inr rvf, s''f) \<in> fst ((withoutPreemption $ getCTE sl) s''e); \<not> isNullCap (cteCap rvf); isZombie (cteCap rvf); \<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap rvf) \<and> capZombieNumber (cteCap rvf) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap rvf))\<rbrakk> \<Longrightarrow> s''f \<turnstile> \<lbrace>?P'152 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf\<rbrace> haskell_assertE (capZombiePtr (cteCap rvf) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl) [] \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s''f. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c); (Inr rve, s''e) \<in> fst ((doE p <- finaliseSlot' rvd False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rvd (snd p)
odE) s''d); (Inr rvf, s''f) \<in> fst ((withoutPreemption $ getCTE sl) s''e); \<not> isNullCap (cteCap rvf); \<not> isZombie (cteCap rvf)\<rbrakk> \<Longrightarrow> s''f \<turnstile> \<lbrace>?P'147 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf\<rbrace> fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c); (Inr rve, s''e) \<in> fst ((doE p <- finaliseSlot' rvd False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rvd (snd p)
odE) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B133 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rvf s. (isNullCap (cteCap rvf) \<longrightarrow> P s \<and> P s) \<and> (\<not> isNullCap (cteCap rvf) \<longrightarrow> (isZombie (cteCap rvf) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap rvf) \<and> capZombieNumber (cteCap rvf) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap rvf) \<longrightarrow> ?P150 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s) \<and> (\<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap rvf) \<and> capZombieNumber (cteCap rvf) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap rvf)) \<longrightarrow> ?P'152 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s)) \<and> (\<not> isZombie (cteCap rvf) \<longrightarrow> ?P'147 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B132 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> doE p <- finaliseSlot' rvd False;
whenE (False \<or> fst p) $ withoutPreemption $ emptySlot rvd (snd p)
odE \<lbrace>?B133 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P129 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B132 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); \<not> (isZombie (fst rvb) \<and> exp)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'131 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 8. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>\<lambda>rvc s. (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 \<longrightarrow> True) \<and> (\<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0) \<longrightarrow> (isZombie (fst rvb) \<and> \<not> exp \<longrightarrow> P s \<and> P s) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P129 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'131 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 9. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 10. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
A total of 12 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c); (Inr rve, s''e) \<in> fst (finaliseSlot' rvd False s''d); False \<or> fst rve\<rbrakk> \<Longrightarrow> \<lbrace>?P220 rv s'' rva s''a rvb s''b () s''c rvd s''d rve\<rbrace> emptySlot rvd (snd rve) \<lbrace>\<lambda>a. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B132 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> finaliseSlot' rvd False \<lbrace>\<lambda>a b. (False \<or> fst a \<longrightarrow> ?P220 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> P b \<and> P b \<and> P b)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P129 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B132 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); \<not> (isZombie (fst rvb) \<and> exp)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'131 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>\<lambda>rvc s. (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 \<longrightarrow> True) \<and> (\<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0) \<longrightarrow> (isZombie (fst rvb) \<and> \<not> exp \<longrightarrow> P s \<and> P s) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P129 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'131 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 9. P s \<Longrightarrow> ?P' s proof (prove)
goal (8 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 sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B132 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> finaliseSlot' rvd False \<lbrace>\<lambda>a b. (False \<or> fst a \<longrightarrow> P b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> P b \<and> P b \<and> P b)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P129 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B132 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); \<not> (isZombie (fst rvb) \<and> exp)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'131 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>\<lambda>rvc s. (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 \<longrightarrow> True) \<and> (\<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0) \<longrightarrow> (isZombie (fst rvb) \<and> \<not> exp \<longrightarrow> P s \<and> P s) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P129 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'131 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 8. P s \<Longrightarrow> ?P' s proof (prove)
goal (8 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 sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp; (Inr rvd, s''d) \<in> fst ((withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1))) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B132 rv s'' rva s''a rvb s''b () s''c rvd\<rbrace> finaliseSlot' rvd False \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P129 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B132 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); \<not> (isZombie (fst rvb) \<and> exp)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'131 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>\<lambda>rvc s. (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 \<longrightarrow> True) \<and> (\<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0) \<longrightarrow> (isZombie (fst rvb) \<and> \<not> exp \<longrightarrow> P s \<and> P s) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P129 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'131 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 8. P s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); isZombie (fst rvb) \<and> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P129 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl); (Inr rvc, s''c) \<in> fst ((withoutPreemption $ updateCap sl (fst rvb)) s''b); \<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0); \<not> (isZombie (fst rvb) \<and> \<not> exp); \<not> (isZombie (fst rvb) \<and> exp)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'131 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) 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) sl; \<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'28 rv s'' rva s''a rvb\<rbrace> withoutPreemption $ updateCap sl (fst rvb) \<lbrace>\<lambda>rvc s. (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0 \<longrightarrow> True) \<and> (\<not> (isZombie (fst rvb) \<and> capZombieNumber (fst rvb) = 0) \<longrightarrow> (isZombie (fst rvb) \<and> \<not> exp \<longrightarrow> P s \<and> P s) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P129 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'131 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv); (Inr rva, s''a) \<in> fst ((withoutPreemption $ isFinalCapability rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B15 rv s'' rva\<rbrace> withoutPreemption $ global.finaliseCap (cteCap rv) rva False \<lbrace>\<lambda>rvb s. (capRemovable (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> P s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((withoutPreemption $ getCTE sl) s); \<not> (isNullCap $ cteCap rv)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'12 rv\<rbrace> withoutPreemption $ isFinalCapability rv \<lbrace>?B15 rv s''\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> P s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>
 7. P s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>P\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. P\<rbrace>, \<lbrace>\<lambda>a. P\<rbrace>

goal:
No subgoals!