theory CSpace_R

lemma ensureEmptySlot_corres:
  "q = cte_map p \<Longrightarrow>
   corres (ser \<oplus> dc) (invs and cte_at p) invs'
                     (ensure_empty p) (ensureEmptySlot q)" apply (clarsimp simp add: ensure_empty_def ensureEmptySlot_def unlessE_whenE liftE_bindE) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_trivial) apply (case_tac cap, auto simp add: whenE_def returnOk_def)[1] apply wp+ apply (clarsimp simp: invs_valid_objs invs_psp_aligned) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. q = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (invs and cte_wp_at (\<lambda>_. True) p) invs' (ensure_empty p) (ensureEmptySlot q) proof (prove)
goal (1 subgoal):
 1. q = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (invs and cte_wp_at (\<lambda>_. True) p) invs' (do cap <- get_cap p;
whenE (cap \<noteq> cap.NullCap) (throwError ExceptionTypes_A.syscall_error.DeleteFirst)
od) (do cte <- getCTE (cte_map p);
whenE (cteCap cte \<noteq> capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst)
od) proof (prove)
goal (3 subgoals):
 1. q = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) ?Q1 ?Q'1 (do cap <- get_cap p;
whenE (cap \<noteq> cap.NullCap) (throwError ExceptionTypes_A.syscall_error.DeleteFirst)
od) (do cte <- getCTE (cte_map p);
whenE (cteCap cte \<noteq> capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst)
od)
 2. \<And>s. \<lbrakk>q = cte_map p; (invs and cte_wp_at (\<lambda>_. True) p) s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>q = cte_map p; invs' s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (5 subgoals):
 1. \<And>cap cte. \<lbrakk>q = cte_map p; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?R5 cap) (?R'5 cte) (whenE (cap \<noteq> cap.NullCap) (throwError ExceptionTypes_A.syscall_error.DeleteFirst)) (whenE (cteCap cte \<noteq> capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst))
 2. q = cte_map p \<Longrightarrow> \<lbrace>?Q5\<rbrace> get_cap p \<lbrace>?R5\<rbrace>
 3. q = cte_map p \<Longrightarrow> \<lbrace>?Q'5\<rbrace> getCTE (cte_map p) \<lbrace>?R'5\<rbrace>
 4. \<And>s. \<lbrakk>q = cte_map p; (invs and cte_wp_at (\<lambda>_. True) p) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) p and ?Q5) s
 5. \<And>s. \<lbrakk>q = cte_map p; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>cap cte. \<lbrakk>q = cte_map p; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (cap \<noteq> cap.NullCap) (throwError ExceptionTypes_A.syscall_error.DeleteFirst)) (whenE (cteCap cte \<noteq> capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst))
 2. q = cte_map p \<Longrightarrow> \<lbrace>?Q5\<rbrace> get_cap p \<lbrace>\<lambda>cap _. True\<rbrace>
 3. q = cte_map p \<Longrightarrow> \<lbrace>?Q'5\<rbrace> getCTE (cte_map p) \<lbrace>\<lambda>cte _. True\<rbrace>
 4. \<And>s. \<lbrakk>q = cte_map p; (invs and cte_wp_at (\<lambda>_. True) p) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) p and ?Q5) s
 5. \<And>s. \<lbrakk>q = cte_map p; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'5) s proof (prove)
goal (4 subgoals):
 1. q = cte_map p \<Longrightarrow> \<lbrace>?Q5\<rbrace> get_cap p \<lbrace>\<lambda>cap _. True\<rbrace>
 2. q = cte_map p \<Longrightarrow> \<lbrace>?Q'5\<rbrace> getCTE (cte_map p) \<lbrace>\<lambda>cte _. True\<rbrace>
 3. \<And>s. \<lbrakk>q = cte_map p; (invs and cte_wp_at (\<lambda>_. True) p) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) p and ?Q5) s
 4. \<And>s. \<lbrakk>q = cte_map p; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'5) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>q = cte_map p; (invs and cte_wp_at (\<lambda>_. True) p) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) p and (\<lambda>_. True)) s
 2. \<And>s. \<lbrakk>q = cte_map p; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>q = cte_map p; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!