theory Tcb_R

lemma slotCapLongRunningDelete_corres:
  "cte_map ptr = ptr' \<Longrightarrow>
   corres (=) (cte_at ptr and invs) invs'
           (slot_cap_long_running_delete ptr)
           (slotCapLongRunningDelete ptr')" apply (clarsimp simp: slot_cap_long_running_delete_def
                        slotCapLongRunningDelete_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (auto split: cap_relation_split_asm arch_cap.split_asm
                 intro!: corres_rel_imp [OF isFinalCapability_corres[where ptr=ptr]]
                   simp: liftM_def[symmetric] final_matters'_def
                         long_running_delete_def
                         longRunningDelete_def isCap_simps)[1] apply (wp get_cap_wp getCTE_wp)+ apply clarsimp apply (clarsimp simp: cte_wp_at_ctes_of) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_map ptr = ptr' \<Longrightarrow> corres (=) (cte_wp_at (\<lambda>_. True) ptr and invs) invs' (slot_cap_long_running_delete ptr) (slotCapLongRunningDelete ptr') proof (prove)
goal (1 subgoal):
 1. ptr' = cte_map ptr \<Longrightarrow> corres (=) (cte_wp_at (\<lambda>_. True) ptr and invs) invs' (do cap <- get_cap ptr;
case cap of cap.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- is_final_cap cap;
return (final \<and> long_running_delete cap)
od
od) (do cte <- getCTE (cte_map ptr);
case cteCap cte of capability.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- isFinalCapability cte;
return $ final \<and> longRunningDelete (cteCap cte)
od
od) proof (prove)
goal (3 subgoals):
 1. ptr' = cte_map ptr \<Longrightarrow> corres (=) ?Q4 ?Q'4 (do cap <- get_cap ptr;
case cap of cap.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- is_final_cap cap;
return (final \<and> long_running_delete cap)
od
od) (do cte <- getCTE (cte_map ptr);
case cteCap cte of capability.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- isFinalCapability cte;
return $ final \<and> longRunningDelete (cteCap cte)
od
od)
 2. \<And>s. \<lbrakk>ptr' = cte_map ptr; (cte_wp_at (\<lambda>_. True) ptr and invs) s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>ptr' = cte_map ptr; invs' s\<rbrakk> \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>cap cte. \<lbrakk>ptr' = cte_map ptr; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres (=) (?R8 cap) (?R'8 cte) (case cap of cap.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- is_final_cap cap;
return (final \<and> long_running_delete cap)
od) (case cteCap cte of capability.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- isFinalCapability cte;
return $ final \<and> longRunningDelete (cteCap cte)
od)
 2. ptr' = cte_map ptr \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_cap ptr \<lbrace>?R8\<rbrace>
 3. ptr' = cte_map ptr \<Longrightarrow> \<lbrace>?Q'8\<rbrace> getCTE (cte_map ptr) \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>ptr' = cte_map ptr; (cte_wp_at (\<lambda>_. True) ptr and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q8) s
 5. \<And>s. \<lbrakk>ptr' = cte_map ptr; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. ptr' = cte_map ptr \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_cap ptr \<lbrace>\<lambda>a. invs and cte_wp_at ((=) a) ptr\<rbrace>
 2. ptr' = cte_map ptr \<Longrightarrow> \<lbrace>?Q'8\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) a) (cte_map ptr)\<rbrace>
 3. \<And>s. \<lbrakk>ptr' = cte_map ptr; (cte_wp_at (\<lambda>_. True) ptr and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q8) s
 4. \<And>s. \<lbrakk>ptr' = cte_map ptr; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ptr' = cte_map ptr; (cte_wp_at (\<lambda>_. True) ptr and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) ptr s \<longrightarrow> (invs and cte_wp_at ((=) cap) ptr) s)) s
 2. \<And>s. \<lbrakk>ptr' = cte_map ptr; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map ptr) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (cte_map ptr) s \<and> (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ptr' = cte_map ptr; invs' s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map ptr) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (cte_map ptr) s \<and> (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ptr' = cte_map ptr; invs' s\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s proof (prove)
goal:
No subgoals!