theory CNodeInv_R

lemma cteDelete_sch_act_simple:
  "\<lbrace>invs' and sch_act_simple and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_to' slot s)\<rbrace>
     cteDelete slot exposed \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" apply (simp add: cteDelete_def whenE_def split_def) apply (wp hoare_drop_imps | simp)+ apply (rule_tac hoare_post_impErr [where Q="\<lambda>rv. sch_act_simple"
                                       and E="\<lambda>rv. sch_act_simple"]) apply (rule valid_validE) apply (wp finaliseSlot_sch_act_simple) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> cteDelete slot exposed \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> doE p <- finaliseSlot slot exposed;
if exposed \<or> fst p then liftE (emptySlot slot (snd p)) else returnOk ()
odE \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot slot exposed \<lbrace>\<lambda>p s. (exposed \<longrightarrow> sch_act_simple s) \<and> (fst p \<longrightarrow> sch_act_simple s) \<and> (\<not> exposed \<and> \<not> fst p \<longrightarrow> sch_act_simple s)\<rbrace>, \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>
 2. \<And>s. (invs' and sch_act_simple and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot slot exposed \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>, \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>
 2. \<And>rv s. sch_act_simple s \<Longrightarrow> (exposed \<longrightarrow> sch_act_simple s) \<and> (fst rv \<longrightarrow> sch_act_simple s) \<and> (\<not> exposed \<and> \<not> fst rv \<longrightarrow> sch_act_simple s)
 3. \<And>e s. sch_act_simple s \<Longrightarrow> sch_act_simple s
 4. \<And>s. (invs' and sch_act_simple and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot slot exposed \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>
 2. \<And>rv s. sch_act_simple s \<Longrightarrow> (exposed \<longrightarrow> sch_act_simple s) \<and> (fst rv \<longrightarrow> sch_act_simple s) \<and> (\<not> exposed \<and> \<not> fst rv \<longrightarrow> sch_act_simple s)
 3. \<And>e s. sch_act_simple s \<Longrightarrow> sch_act_simple s
 4. \<And>s. (invs' and sch_act_simple and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. sch_act_simple s \<Longrightarrow> (exposed \<longrightarrow> sch_act_simple s) \<and> (fst rv \<longrightarrow> sch_act_simple s) \<and> (\<not> exposed \<and> \<not> fst rv \<longrightarrow> sch_act_simple s)
 2. \<And>e s. sch_act_simple s \<Longrightarrow> sch_act_simple s
 3. \<And>s. (invs' and sch_act_simple and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) s \<Longrightarrow> invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) proof (prove)
goal:
No subgoals!