theory CNodeInv_R

lemma finaliseSlot_IRQInactive':
  "s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' a b
  \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<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 "1.hyps") apply (unfold Let_def split_def fst_conv snd_conv
                          case_Zombie_assert_fold haskell_fail_def) apply (wp getCTE_wp' preemptionPoint_invR| simp add: o_def irq_state_independent_HI)+ apply (rule hoare_post_imp [where Q="\<lambda>_. valid_irq_states'"]) apply simp apply wp[1] apply (rule spec_strengthen_postE) apply (rule "1.hyps", (assumption|rule refl)+) apply simp apply (wp hoare_drop_imps hoare_vcg_all_lift | simp add: locateSlot_conv)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' a b \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> finaliseSlot' v False \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> finaliseSlot' ?v False \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> finaliseSlot' v False \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<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>valid_irq_states'\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' x b \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 2. valid_irq_states' 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. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<rbrace>
 2. valid_irq_states' 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. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<rbrace>
 2. valid_irq_states' 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 (?rvd43 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), ?std43 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 (?rve43 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), s''e) \<in> fst (preemptionPoint (?std43 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>?B39 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemptionPoint \<lbrace>\<lambda>rve. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<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>?B37 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>?B39 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a aa. intStateIRQTable (ksInterruptState aa) a \<noteq> irqstate.IRQInactive\<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>?B37 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 9. valid_irq_states' 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 (?rvd43 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), ?std43 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 (?rve43 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e), s''e) \<in> fst (preemptionPoint (?std43 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>?B39 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemptionPoint \<lbrace>\<lambda>rve. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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>?B37 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>?B39 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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>?B37 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 9. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d rve s''e. \<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 rve, s''e) \<in> fst ((doE cte <- liftE (getCTE rvd);
if cteCap cte = capability.NullCap then returnOk (True, capability.NullCap) else doE final <- liftE (isFinalCapability cte);
(remainder, info) <- liftE (global.finaliseCap (cteCap cte) final False);
if capRemovable remainder rvd then returnOk (True, info) else if capCyclicZombie remainder rvd then doE y <- liftE (updateCap rvd remainder);
returnOk (False, capability.NullCap)
odE else doE y <- liftE (updateCap rvd remainder);
y <- if isZombie remainder \<and> capZombieNumber remainder = 0 then fail else if isZombie remainder then let ptr = capZombiePtr remainder in doE y <- assertE (ptr \<noteq> rvd);
capAtPtr <- liftE (liftM cteCap (getCTE ptr));
y <- case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
liftE (capSwapForDelete ptr rvd)
odE else fail;
y <- preemptionPoint;
finaliseSlot' rvd False
odE
odE
odE) s''d); fst rve\<rbrakk> \<Longrightarrow> \<lbrace>?P175 rv s'' rva s''a rvb s''b () s''c rvd s''d rve\<rbrace> emptySlot rvd (snd rve) \<lbrace>\<lambda>rve s. \<forall>cte. cte_wp_at' ((=) cte) sl s \<longrightarrow> (cteCap cte = capability.NullCap \<longrightarrow> valid_irq_states' s) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) rvd s) \<longrightarrow> valid_irq_states' s) \<and> ((capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<longrightarrow> capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<longrightarrow> capZombieType (fst rvb) \<noteq> capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' s))\<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>?B114 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> ?P175 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) sl b \<longrightarrow> (isNullCap (cteCap cte) \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b) \<and> (\<not> isNullCap (cteCap cte) \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) rvd b \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b)) \<and> (\<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' b)) \<and> (\<not> isZombie (cteCap cte) \<longrightarrow> True))))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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>?P111 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B114 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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'113 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. valid_irq_states' s \<and> valid_irq_states' s\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr (fst rvb)) s \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> valid_irq_states' s)) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P111 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'113 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 9. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (10 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d rve s''e rvc s. \<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 rve, s''e) \<in> fst ((doE cte <- liftE (getCTE rvd);
if cteCap cte = capability.NullCap then returnOk (True, capability.NullCap) else doE final <- liftE (isFinalCapability cte);
(remainder, info) <- liftE (global.finaliseCap (cteCap cte) final False);
if capRemovable remainder rvd then returnOk (True, info) else if capCyclicZombie remainder rvd then doE y <- liftE (updateCap rvd remainder);
returnOk (False, capability.NullCap)
odE else doE y <- liftE (updateCap rvd remainder);
y <- if isZombie remainder \<and> capZombieNumber remainder = 0 then fail else if isZombie remainder then let ptr = capZombiePtr remainder in doE y <- assertE (ptr \<noteq> rvd);
capAtPtr <- liftE (liftM cteCap (getCTE ptr));
y <- case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
liftE (capSwapForDelete ptr rvd)
odE else fail;
y <- preemptionPoint;
finaliseSlot' rvd False
odE
odE
odE) s''d); fst rve; valid_irq_states' s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) sl s \<longrightarrow> (cteCap cte = capability.NullCap \<longrightarrow> valid_irq_states' s) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) rvd s) \<longrightarrow> valid_irq_states' s) \<and> ((capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<longrightarrow> capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<longrightarrow> capZombieType (fst rvb) \<noteq> capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' s))
 2. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d rve s''e. \<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 rve, s''e) \<in> fst ((doE cte <- liftE (getCTE rvd);
if cteCap cte = capability.NullCap then returnOk (True, capability.NullCap) else doE final <- liftE (isFinalCapability cte);
(remainder, info) <- liftE (global.finaliseCap (cteCap cte) final False);
if capRemovable remainder rvd then returnOk (True, info) else if capCyclicZombie remainder rvd then doE y <- liftE (updateCap rvd remainder);
returnOk (False, capability.NullCap)
odE else doE y <- liftE (updateCap rvd remainder);
y <- if isZombie remainder \<and> capZombieNumber remainder = 0 then fail else if isZombie remainder then let ptr = capZombiePtr remainder in doE y <- assertE (ptr \<noteq> rvd);
capAtPtr <- liftE (liftM cteCap (getCTE ptr));
y <- case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
liftE (capSwapForDelete ptr rvd)
odE else fail;
y <- preemptionPoint;
finaliseSlot' rvd False
odE
odE
odE) s''d); fst rve\<rbrakk> \<Longrightarrow> \<lbrace>?P175 rv s'' rva s''a rvb s''b () s''c rvd s''d rve\<rbrace> emptySlot rvd (snd rve) \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>
 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); \<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>?B114 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> ?P175 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) sl b \<longrightarrow> (isNullCap (cteCap cte) \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b) \<and> (\<not> isNullCap (cteCap cte) \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) rvd b \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b)) \<and> (\<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' b)) \<and> (\<not> isZombie (cteCap cte) \<longrightarrow> True))))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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); isZombie (fst rvb) \<and> exp\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P111 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B114 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 5. \<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'113 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. valid_irq_states' s \<and> valid_irq_states' s\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 6. \<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> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr (fst rvb)) s \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> valid_irq_states' s)) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P111 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'113 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 7. \<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. \<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 9. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 10. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d rve s''e. \<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 rve, s''e) \<in> fst ((doE cte <- liftE (getCTE rvd);
if cteCap cte = capability.NullCap then returnOk (True, capability.NullCap) else doE final <- liftE (isFinalCapability cte);
(remainder, info) <- liftE (global.finaliseCap (cteCap cte) final False);
if capRemovable remainder rvd then returnOk (True, info) else if capCyclicZombie remainder rvd then doE y <- liftE (updateCap rvd remainder);
returnOk (False, capability.NullCap)
odE else doE y <- liftE (updateCap rvd remainder);
y <- if isZombie remainder \<and> capZombieNumber remainder = 0 then fail else if isZombie remainder then let ptr = capZombiePtr remainder in doE y <- assertE (ptr \<noteq> rvd);
capAtPtr <- liftE (liftM cteCap (getCTE ptr));
y <- case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
liftE (capSwapForDelete ptr rvd)
odE else fail;
y <- preemptionPoint;
finaliseSlot' rvd False
odE
odE
odE) s''d); fst rve\<rbrakk> \<Longrightarrow> \<lbrace>?P175 rv s'' rva s''a rvb s''b () s''c rvd s''d rve\<rbrace> emptySlot rvd (snd rve) \<lbrace>\<lambda>_. valid_irq_states'\<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>?B114 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> ?P175 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) sl b \<longrightarrow> (isNullCap (cteCap cte) \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b) \<and> (\<not> isNullCap (cteCap cte) \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) rvd b \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b)) \<and> (\<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' b)) \<and> (\<not> isZombie (cteCap cte) \<longrightarrow> True))))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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>?P111 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B114 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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'113 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. valid_irq_states' s \<and> valid_irq_states' s\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr (fst rvb)) s \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> valid_irq_states' s)) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P111 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'113 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 9. valid_irq_states' 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>?B114 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> valid_irq_states' b) \<and> (\<not> (False \<or> fst a) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) sl b \<longrightarrow> (isNullCap (cteCap cte) \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b) \<and> (\<not> isNullCap (cteCap cte) \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) rvd b \<longrightarrow> valid_irq_states' b \<and> valid_irq_states' b)) \<and> (\<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' b)) \<and> (\<not> isZombie (cteCap cte) \<longrightarrow> True))))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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>?P111 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B114 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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'113 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. valid_irq_states' s \<and> valid_irq_states' s\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr (fst rvb)) s \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> valid_irq_states' s)) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P111 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'113 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. valid_irq_states' 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. \<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>?B114 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> finaliseSlot' rvd False \<lbrace>?Q'209 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s r. \<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); ?Q'209 rv s'' rva s''a rvb s''b rvc s''c rvd s''d s r\<rbrakk> \<Longrightarrow> (False \<or> fst s \<longrightarrow> valid_irq_states' r) \<and> (\<not> (False \<or> fst s) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) sl r \<longrightarrow> (isNullCap (cteCap cte) \<longrightarrow> valid_irq_states' r \<and> valid_irq_states' r) \<and> (\<not> isNullCap (cteCap cte) \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) rvd r \<longrightarrow> valid_irq_states' r \<and> valid_irq_states' r)) \<and> (\<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' r)) \<and> (\<not> isZombie (cteCap cte) \<longrightarrow> True))))
 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>?P111 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>?B114 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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'113 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. valid_irq_states' s \<and> valid_irq_states' s\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr (fst rvb)) s \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> valid_irq_states' s)) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P111 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'113 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 9. valid_irq_states' 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 s r. \<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); valid_irq_states' r\<rbrakk> \<Longrightarrow> (False \<or> fst s \<longrightarrow> valid_irq_states' r) \<and> (\<not> (False \<or> fst s) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) sl r \<longrightarrow> (isNullCap (cteCap cte) \<longrightarrow> valid_irq_states' r \<and> valid_irq_states' r) \<and> (\<not> isNullCap (cteCap cte) \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) rvd r \<longrightarrow> valid_irq_states' r \<and> valid_irq_states' r)) \<and> (\<not> (capZombiePtr (fst rvb) = capZombiePtr (cteCap cte) \<and> capZombieNumber (cteCap cte) = capZombieNumber (fst rvb) \<and> capZombieType (fst rvb) = capZombieType (cteCap cte)) \<longrightarrow> capZombiePtr (cteCap cte) = sl \<and> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> valid_irq_states' r)) \<and> (\<not> isZombie (cteCap cte) \<longrightarrow> True))))
 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>?P111 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>\<lambda>rvd. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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'113 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. valid_irq_states' s \<and> valid_irq_states' s\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr (fst rvb)) s \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> valid_irq_states' s)) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P111 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'113 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 8. valid_irq_states' 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>?P111 rv s'' rva s''a rvb s''b rvc\<rbrace> withoutPreemption $ locateSlotCap (fst rvb) (fromIntegral (capZombieNumber (fst rvb) - 1)) \<lbrace>\<lambda>rvd. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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'113 rv s'' rva s''a rvb s''b rvc\<rbrace> fail \<lbrace>\<lambda>rvd s. valid_irq_states' s \<and> valid_irq_states' s\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> capZombiePtr (fst rvb) \<noteq> sl \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (capZombiePtr (fst rvb)) s \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> capZombiePtr (fst rvb)) \<longrightarrow> valid_irq_states' s)) \<and> (\<not> (isZombie (fst rvb) \<and> \<not> exp) \<longrightarrow> (isZombie (fst rvb) \<and> exp \<longrightarrow> ?P111 rv s'' rva s''a rvb s''b rvc s) \<and> (\<not> (isZombie (fst rvb) \<and> exp) \<longrightarrow> ?P'113 rv s'' rva s''a rvb s''b rvc s)))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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> valid_irq_states' s) \<and> (\<not> capRemovable (fst rvb) sl \<longrightarrow> (\<not> exp \<and> capCyclicZombie (fst rvb) sl \<longrightarrow> valid_irq_states' s) \<and> (\<not> (\<not> exp \<and> capCyclicZombie (fst rvb) sl) \<longrightarrow> ?P'28 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<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 b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> withoutPreemption $ getCTE sl \<lbrace>\<lambda>rv s. ((isNullCap $ cteCap rv) \<longrightarrow> valid_irq_states' s) \<and> (\<not> (isNullCap $ cteCap rv) \<longrightarrow> ?P'12 rv s)\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>
 7. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' sl exp \<lbrace>\<lambda>a. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>a b. intStateIRQTable (ksInterruptState b) a \<noteq> irqstate.IRQInactive\<rbrace>

goal:
No subgoals!