theory CSpaceAcc_C

lemma getSlotCap_h_val_ccorres [corres]:
  fixes p :: "cstate \<Rightarrow> cte_C ptr"
  assumes gl: "\<And>v s. globals (xfu v s) = globals s" \<comment> \<open>for state rel. preservation\<close>
  and     fg: "\<And>v s. xf (xfu (\<lambda>_. v) s) = v"
  shows "ccorres ccap_relation xf \<top> {s. p s = Ptr a} hs
         (getSlotCap a) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (Ptr &(p s\<rightarrow>[''cap_C'']) :: cap_C ptr)) s))" unfolding getSlotCap_def apply (rule ccorres_add_UNIV_Int) apply (cinitlift p) \<comment> \<open>EVIL!\<close> apply simp apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) apply (rule_tac R = "\<lambda>s. ctes_of s a = Some cte" in ccorres_return  [where R' = UNIV]) apply vcg apply (clarsimp simp: gl fg cte_wp_at_ctes_of) apply (erule (1) rf_sr_ctes_of_cliftE) apply (clarsimp simp add: typ_heap_simps ccap_relation_def cte_to_H_def cl_valid_cte_def c_valid_cap_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres ccap_relation xf (\<lambda>_. True) {s. p s = cte_Ptr a} hs (getSlotCap a) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(p s\<rightarrow>[''cap_C'']))) s)) proof (prove)
goal (1 subgoal):
 1. ccorres ccap_relation xf (\<lambda>_. True) {s. p s = cte_Ptr a} hs (do cte <- getCTE a;
return $ cteCap cte
od) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(p s\<rightarrow>[''cap_C'']))) s)) proof (prove)
goal (1 subgoal):
 1. ccorres ccap_relation xf (\<lambda>_. True) (UNIV \<inter> {s. p s = cte_Ptr a}) hs (do cte <- getCTE a;
return $ cteCap cte
od) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(p s\<rightarrow>[''cap_C'']))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>rv. rv = cte_Ptr a \<Longrightarrow> ccorres ccap_relation xf (\<lambda>_. True) UNIV hs (do cte <- getCTE a;
return $ cteCap cte
od) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(rv\<rightarrow>[''cap_C'']))) s)) proof (prove)
goal (1 subgoal):
 1. ccorres ccap_relation xf (\<lambda>_. True) UNIV hs (do cte <- getCTE a;
return (cteCap cte)
od) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C'']))) s)) proof (prove)
goal (2 subgoals):
 1. ccorres ccap_relation xf ?Q20 ?Q'20 hs (do cte <- getCTE a;
return (cteCap cte)
od) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C'']))) s))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q20 s \<and> s' \<in> ?Q'20 proof (prove)
goal (2 subgoals):
 1. \<And>cte. ccorres ccap_relation xf (?P23 cte) (?P'23 cte) hs (return (cteCap cte)) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C'']))) s))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s a = Some cte \<longrightarrow> ?P23 cte s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr a) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> ?P'23 (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>cte s. ctes_of s a = Some cte \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr \<and> ccap_relation (cteCap cte) (xf s')}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s a = Some cte \<longrightarrow> ctes_of s a = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr a) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>cte s. ctes_of s a = Some cte \<Longrightarrow> UNIV \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals sa))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C'']))) sa) \<in> rf_sr \<and> ccap_relation (cteCap cte) (xf (xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals sa))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C'']))) sa))}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s a = Some cte \<longrightarrow> ctes_of s a = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr a) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>cte s x. \<lbrakk>ctes_of s a = Some cte; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C''])))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s a = Some cte \<longrightarrow> ctes_of s a = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr a) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>cte s x cte' ctel'. \<lbrakk>(s, x) \<in> rf_sr; ctes_of s a = Some (cte_to_H ctel'); cslift x (cte_Ptr a) = Some cte'; cte_lift cte' = Some ctel'; cte = cte_to_H ctel'; cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(cte_Ptr a\<rightarrow>[''cap_C''])))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s a = Some cte \<longrightarrow> ctes_of s a = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr a) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s a = Some cte \<longrightarrow> ctes_of s a = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr a) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal:
No subgoals!