theory CNodeInv_R

lemma finaliseSlot_cte_wp_at:
  "\<lbrakk> \<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_to' slot s
         \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>
     finaliseSlot slot False
   \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or>
                         (\<exists>zb n cp. cteCap cte = Zombie p zb n \<and>
                              P cp \<and> capZombiePtr cp \<noteq> p)) p s\<rbrace>,-" unfolding finaliseSlot_def apply (rule hoare_pre, unfold validE_R_def) apply (rule hoare_post_impErr, rule use_spec) apply (rule finaliseSlot_invs'[where P=P and Pr=\<top> and p=p]) apply (simp_all add: no_cte_prop_top finalise_prop_stuff_def) apply wp apply (clarsimp simp: cte_wp_at_ctes_of) apply fastforce apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> finaliseSlot slot False \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> capZombiePtr cp \<noteq> p)) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> finaliseSlot' slot False \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> capZombiePtr cp \<noteq> p)) p\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'\<rbrace> finaliseSlot' slot False \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> capZombiePtr cp \<noteq> p)) p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>?P'\<rbrace> finaliseSlot' slot False \<lbrace>?Q3\<rbrace>, \<lbrace>?E3\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; ?Q3 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> capZombiePtr cp \<noteq> p)) p s
 3. \<And>e s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; ?E3 e s\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>s cap final sl. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>no_cte_prop (\<lambda>_. True) and invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap final False \<lbrace>\<lambda>rv. no_cte_prop (\<lambda>_. True)\<rbrace>
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> finalise_prop_stuff (\<lambda>_. True)
 3. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; no_cte_prop (\<lambda>_. True) s \<and> invs' s \<and> sch_act_simple s \<and> (False \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s) \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> capZombiePtr cp \<noteq> p)) p s
 4. \<And>e s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; no_cte_prop (\<lambda>_. True) s \<and> invs' s \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> True
 5. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> no_cte_prop (\<lambda>_. True) s \<and> invs' s \<and> sch_act_simple s \<and> (False \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (False \<or> p = slot \<or> cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie p zb n \<and> P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s) proof (prove)
goal (3 subgoals):
 1. \<And>cap final sl. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<lbrace>invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap final False \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s
 3. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> capZombiePtr cp \<noteq> p)) p s
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s proof (prove)
goal (2 subgoals):
 1. \<And>a b s cte. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s; sch_act_simple s; a \<longrightarrow> (\<exists>cte. ctes_of s slot = Some cte \<and> removeable' slot s (cteCap cte)); b \<noteq> capability.NullCap \<longrightarrow> (\<forall>sl'. sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some b); ctes_of s p = Some cte; P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p)); (\<forall>zb n. cteCap cte \<noteq> capability.Zombie p zb n) \<or> (\<forall>cp. P cp \<longrightarrow> capZombiePtr cp = p)\<rbrakk> \<Longrightarrow> P (cteCap cte)
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> isZombie cap; p \<noteq> slot; invs' s \<and> sch_act_simple s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) slot s \<and> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte) \<or> (\<exists>zb n. cteCap cte = capability.Zombie p zb n) \<and> (\<exists>cp. P cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> p))) p s proof (prove)
goal:
No subgoals!