theory CNodeInv_R

lemma finaliseSlot_invs'':
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_to' slot s)\<rbrace>
     finaliseSlot slot exposed
   \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s)
                 \<and> (\<forall>sl'. snd rv \<noteq> NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))\<rbrace>,
   \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s\<rbrace>" unfolding finaliseSlot_def apply (rule hoare_pre, rule hoare_post_impErr, rule use_spec) apply (rule finaliseSlot_invs'[where P="\<top>" and Pr="\<top>" and p=slot]) apply (simp_all add: no_cte_prop_top) apply wp apply (simp add: finalise_prop_stuff_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot exposed \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple 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))\<rbrace>, \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot' slot exposed \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple 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))\<rbrace>, \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?Q\<rbrace> finaliseSlot' slot exposed \<lbrace>?Q3\<rbrace>, \<lbrace>?E3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> invs' s \<and> sch_act_simple 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))
 3. \<And>e s. ?E3 e s \<Longrightarrow> invs' s \<and> sch_act_simple s
 4. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>s cap final sl. \<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. finalise_prop_stuff (\<lambda>_. True)
 3. \<And>rv s. no_cte_prop (\<lambda>_. True) s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. ((\<lambda>_. True) and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> True \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot 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)) \<Longrightarrow> invs' s \<and> sch_act_simple 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))
 4. \<And>e s. no_cte_prop (\<lambda>_. True) s \<and> invs' s \<and> sch_act_simple s \<Longrightarrow> invs' s \<and> sch_act_simple s
 5. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> no_cte_prop (\<lambda>_. True) s \<and> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. ((\<lambda>_. True) and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> True \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) proof (prove)
goal (3 subgoals):
 1. \<And>cap final sl. \<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. finalise_prop_stuff (\<lambda>_. True)
 3. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal (2 subgoals):
 1. finalise_prop_stuff (\<lambda>_. True)
 2. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal:
No subgoals!