theory EmptyFail_H

lemma finaliseSlot_spec_empty_fail:
  notes spec_empty_fail_bindE'[rotated, wp_split]
  shows "spec_empty_fail (finaliseSlot x b) s" unfolding finaliseSlot_def proof (induct rule: finalise_spec_empty_fail_induct) case (1 x b s) show ?case apply (subst finaliseSlot'_simps_ext) apply (simp only: split_def Let_def K_bind_def fun_app_def) apply (wp spec_empty_whenE' spec_empty_fail_If | wpc
         | rule 1[unfolded Let_def K_bind_def split_def fun_app_def,
                  simplified], (simp | intro conjI)+
         | rule drop_spec_empty_fail | simp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (finaliseSlot x b) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (finaliseSlot' x b) s 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> spec_empty_fail (finaliseSlot' v False) s'; \<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> spec_empty_fail (finaliseSlot' x b) ste\<rbrakk> \<Longrightarrow> spec_empty_fail (finaliseSlot' x b) s proof (state)
this:
\<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> spec_empty_fail (finaliseSlot' ?v False) ?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); (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> spec_empty_fail (finaliseSlot' x b) ?ste

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> spec_empty_fail (finaliseSlot' v False) s'; \<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> spec_empty_fail (finaliseSlot' x b) ste\<rbrakk> \<Longrightarrow> spec_empty_fail (finaliseSlot' x b) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (finaliseSlot' x b) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (doE cte <- withoutPreemption $ getCTE x;
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 x then returnOk (True, info) else if \<not> b \<and> capCyclicZombie remainder x then doE withoutPreemption $ updateCap x remainder;
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap x remainder;
let (v33, v34) = (remainder, 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 [];
preemptionPoint;
finaliseSlot' x b
odE
odE
odE) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (doE cte <- withoutPreemption (getCTE x);
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) x then returnOk (True, snd p) else if \<not> b \<and> capCyclicZombie (fst p) x then doE y <- withoutPreemption (updateCap x (fst p));
returnOk (False, capability.NullCap)
odE else doE y <- withoutPreemption (updateCap x (fst p));
y <- if isZombie (fst (fst p, b)) \<and> capZombieNumber (fst (fst p, b)) = 0 then haskell_fail [] else if isZombie (fst (fst p, b)) \<and> \<not> snd (fst p, b) then doE y <- haskell_assertE (capZombiePtr (fst (fst p, b)) \<noteq> x) [];
capAtPtr <- withoutPreemption (liftM cteCap (getCTE (capZombiePtr (fst (fst p, b)))));
y <- case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> capZombiePtr (fst (fst p, b))) [] | _ \<Rightarrow> returnOk ();
withoutPreemption (capSwapForDelete (capZombiePtr (fst (fst p, b))) x)
odE else if isZombie (fst (fst p, b)) \<and> snd (fst p, b) then doE endSlot <- withoutPreemption (locateSlotCap (fst (fst p, b)) (fromIntegral (capZombieNumber (fst (fst p, b)) - 1)));
y <- doE p <- finaliseSlot' endSlot False;
whenE (False \<or> fst p) (withoutPreemption (emptySlot endSlot (snd p)))
odE;
ourCTE <- withoutPreemption (getCTE x);
if isNullCap (cteCap ourCTE) then returnOk () else if isZombie (cteCap ourCTE) then if capZombiePtr (fst (fst p, b)) = capZombiePtr (cteCap ourCTE) \<and> capZombieNumber (cteCap ourCTE) = capZombieNumber (fst (fst p, b)) \<and> capZombieType (fst (fst p, b)) = capZombieType (cteCap ourCTE) then withoutPreemption (do endCTE <- getCTE endSlot;
y <- haskell_assert (isNullCap (cteCap endCTE)) [];
return (capZombieNumber_update (\<lambda>_. capZombieNumber (fst (fst p, b)) - 1) (fst (fst p, b))) >>= updateCap x
od) else haskell_assertE (capZombiePtr (cteCap ourCTE) = x \<and> capZombiePtr (fst (fst p, b)) \<noteq> x) [] else haskell_fail []
odE else haskell_fail [];
y <- preemptionPoint;
finaliseSlot' x b
odE
odE
odE) s proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (finaliseSlot' x b) s

goal:
No subgoals!