theory CNodeInv_R

lemma cteDelete_cte_at:
  "\<lbrace>\<top>\<rbrace> cteDelete slot bool \<lbrace>\<lambda>rv. cte_at' slot\<rbrace>" apply (rule_tac Q="\<lambda>s. cte_at' slot s \<or> \<not> cte_at' slot s"
               in hoare_pre(1)) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_disj_lift) apply (rule typ_at_lifts, rule cteDelete_typ_at') apply (simp add: cteDelete_def finaliseSlot_def split_def) apply (rule validE_valid, rule seqE) apply (subst finaliseSlot'_simps_ext) apply (rule seqE) apply simp apply (rule getCTE_sp) apply (rule hoare_pre, rule hoare_FalseE) apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule hoare_FalseE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cteDelete slot bool \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> cteDelete slot bool \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) slot\<rbrace>
 2. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> cteDelete slot bool \<lbrace>?Q1\<rbrace>
 2. \<And>rv s. ?Q1 rv s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 3. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (4 subgoals):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) slot\<rbrace> cteDelete slot bool \<lbrace>?Q4\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> cteDelete slot bool \<lbrace>?Q'4\<rbrace>
 3. \<And>rv s. ?Q4 rv s \<or> ?Q'4 rv s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 4. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> cteDelete slot bool \<lbrace>?Q'4\<rbrace>
 2. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'4 rv s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 3. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> doE p <- finaliseSlot' slot bool;
whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p)))
odE \<lbrace>?Q'4\<rbrace>
 2. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'4 rv s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 3. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (4 subgoals):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> finaliseSlot' slot bool \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 2. \<And>p. \<lbrace>?B13 p\<rbrace> whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p))) \<lbrace>\<lambda>_. ?Q'11\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 3. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 4. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (4 subgoals):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> doE cte <- withoutPreemption $ getCTE slot;
if isNullCap $ cteCap cte then returnOk (True, capability.NullCap) else doE final <- withoutPreemption $ isFinalCapability cte;
(remainder, info) <- withoutPreemption $ global.finaliseCap (cteCap cte) final False;
if capRemovable remainder slot then returnOk (True, info) else if \<not> bool \<and> capCyclicZombie remainder slot then doE withoutPreemption $ updateCap slot remainder;
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap slot remainder;
let (v33, v34) = (remainder, bool) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot bool
odE
odE
odE \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 2. \<And>p. \<lbrace>?B13 p\<rbrace> whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p))) \<lbrace>\<lambda>_. ?Q'11\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 3. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 4. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (5 subgoals):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> withoutPreemption $ getCTE slot \<lbrace>?B19\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 2. \<And>cte. \<lbrace>?B19 cte\<rbrace> if isNullCap $ cteCap cte then returnOk (True, capability.NullCap) else doE final <- withoutPreemption $ isFinalCapability cte;
(remainder, info) <- withoutPreemption $ global.finaliseCap (cteCap cte) final False;
if capRemovable remainder slot then returnOk (True, info) else if \<not> bool \<and> capCyclicZombie remainder slot then doE withoutPreemption $ updateCap slot remainder;
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap slot remainder;
let (v33, v34) = (remainder, bool) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot bool
odE
odE \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 3. \<And>p. \<lbrace>?B13 p\<rbrace> whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p))) \<lbrace>\<lambda>_. ?Q'11\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 4. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 5. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (5 subgoals):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s\<rbrace> getCTE slot \<lbrace>?B19\<rbrace>
 2. \<And>cte. \<lbrace>?B19 cte\<rbrace> if isNullCap $ cteCap cte then returnOk (True, capability.NullCap) else doE final <- withoutPreemption $ isFinalCapability cte;
(remainder, info) <- withoutPreemption $ global.finaliseCap (cteCap cte) final False;
if capRemovable remainder slot then returnOk (True, info) else if \<not> bool \<and> capCyclicZombie remainder slot then doE withoutPreemption $ updateCap slot remainder;
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap slot remainder;
let (v33, v34) = (remainder, bool) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot bool
odE
odE \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 3. \<And>p. \<lbrace>?B13 p\<rbrace> whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p))) \<lbrace>\<lambda>_. ?Q'11\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 4. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 5. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (4 subgoals):
 1. \<And>cte. \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s)\<rbrace> if isNullCap $ cteCap cte then returnOk (True, capability.NullCap) else doE final <- withoutPreemption $ isFinalCapability cte;
(remainder, info) <- withoutPreemption $ global.finaliseCap (cteCap cte) final False;
if capRemovable remainder slot then returnOk (True, info) else if \<not> bool \<and> capCyclicZombie remainder slot then doE withoutPreemption $ updateCap slot remainder;
returnOk (False, capability.NullCap)
odE else doE withoutPreemption $ updateCap slot remainder;
let (v33, v34) = (remainder, bool) in if isZombie v33 \<and> capZombieNumber v33 = 0 then haskell_fail [] else if isZombie v33 \<and> \<not> v34 then let ptr = capZombiePtr v33 in doE haskell_assertE (ptr \<noteq> slot) [];
capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr;
case capAtPtr of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (ptr2 \<noteq> ptr) [] | _ \<Rightarrow> returnOk ();
withoutPreemption $ capSwapForDelete ptr slot
odE else if isZombie v33 \<and> v34 then let z = v33; ptr = capZombiePtr z; n = capZombieNumber z in doE endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1));
doE (success, info) <- finaliseSlot' endSlot False;
whenE (False \<or> success) $ withoutPreemption $ emptySlot endSlot info
odE;
ourCTE <- withoutPreemption $ getCTE slot;
let c2 = cteCap ourCTE in if isNullCap c2 then returnOk () else if isZombie c2 then let ptr2 = capZombiePtr c2 in if ptr = ptr2 \<and> capZombieNumber c2 = n \<and> capZombieType z = capZombieType c2 then withoutPreemption $ do endCTE <- getCTE endSlot;
haskell_assert (isNullCap $ cteCap endCTE) [];
return (capZombieNumber_update (\<lambda>_. n - 1) z) >>= updateCap slot
od else haskell_assertE (ptr2 = slot \<and> ptr \<noteq> slot) [] else haskell_fail []
odE else haskell_fail [];
preemptionPoint;
finaliseSlot' slot bool
odE
odE \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 2. \<And>p. \<lbrace>?B13 p\<rbrace> whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p))) \<lbrace>\<lambda>_. ?Q'11\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 3. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 4. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (4 subgoals):
 1. \<And>cte s. (cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) slot s)) s \<Longrightarrow> False
 2. \<And>p. \<lbrace>?B13 p\<rbrace> whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p))) \<lbrace>\<lambda>_. ?Q'11\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 3. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 4. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrace>?B13 p\<rbrace> whenE (bool \<or> fst p) (liftE (emptySlot slot (snd p))) \<lbrace>\<lambda>_. ?Q'11\<rbrace>, \<lbrace>\<lambda>_. ?Q'11\<rbrace>
 2. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 3. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. cte_wp_at' (\<lambda>_. True) slot s \<or> ?Q'11 s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s
 2. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<or> \<not> cte_wp_at' (\<lambda>_. True) slot s proof (prove)
goal:
No subgoals!