theory CSpace_C

lemma ccorres_return_cte_cteCap [corres]:
  fixes ptr' :: "cstate \<Rightarrow> cte_C ptr"
  assumes r1: "\<And>s s' g. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu g s') \<in> rf_sr"
  and xf_xfu: "\<And>s g. xf (xfu g s) = g s"
  shows "ccorres ccap_relation xf
         (\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr}  hs
         (return (cteCap cte))
         (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s)))
           (Ptr &(ptr' s \<rightarrow>[''cap_C'']))) s))" apply (rule ccorres_return) apply (rule conseqPre) apply vcg apply (clarsimp simp: xf_xfu ccap_relation_def) apply rule apply (erule r1) apply (drule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (simp add: c_valid_cte_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres ccap_relation xf (\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs (return (cteCap cte)) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(ptr' s\<rightarrow>[''cap_C'']))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. ctes_of s ptr = Some cte \<Longrightarrow> \<Gamma>\<turnstile> ({s. ptr_val (ptr' s) = ptr} \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(ptr' s\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr \<and> ccap_relation (cteCap cte) (xf s')} proof (prove)
goal (2 subgoals):
 1. \<And>s. ctes_of s ptr = Some cte \<Longrightarrow> \<Gamma>\<turnstile> (?P'2 s) Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(ptr' s\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr \<and> ccap_relation (cteCap cte) (xf s')}
 2. \<And>s. ctes_of s ptr = Some cte \<Longrightarrow> {s. ptr_val (ptr' s) = ptr} \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> ?P'2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ctes_of s ptr = Some cte \<Longrightarrow> {s. ptr_val (ptr' s) = ptr} \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals sa))) (cap_Ptr &(ptr' sa\<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 &(ptr' sa\<rightarrow>[''cap_C'']))) sa))} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ctes_of s (ptr_val (ptr' x)) = Some cte; ptr = ptr_val (ptr' x); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C'']))) x) \<in> rf_sr \<and> Some (cteCap cte) = map_option cap_to_H (cap_lift (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C''])))) \<and> c_valid_cap (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C'']))) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ctes_of s (ptr_val (ptr' x)) = Some cte; ptr = ptr_val (ptr' x); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C'']))) x) \<in> rf_sr
 2. \<And>s x. \<lbrakk>ctes_of s (ptr_val (ptr' x)) = Some cte; ptr = ptr_val (ptr' x); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> Some (cteCap cte) = map_option cap_to_H (cap_lift (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C''])))) \<and> c_valid_cap (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ctes_of s (ptr_val (ptr' x)) = Some cte; ptr = ptr_val (ptr' x); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> Some (cteCap cte) = map_option cap_to_H (cap_lift (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C''])))) \<and> c_valid_cap (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ctes_of s (ptr_val (ptr' x)) = Some cte; ptr = ptr_val (ptr' x); \<exists>cte'. cslift x (cte_Ptr (ptr_val (ptr' x))) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> Some (cteCap cte) = map_option cap_to_H (cap_lift (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C''])))) \<and> c_valid_cap (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(ptr' x\<rightarrow>[''cap_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cte' y. \<lbrakk>ctes_of s (ptr_val (ptr' x)) = Some (cte_to_H y); ptr = ptr_val (ptr' x); cslift x (ptr' x) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cte = cte_to_H y\<rbrakk> \<Longrightarrow> c_valid_cap (cte_C.cap_C cte') proof (prove)
goal:
No subgoals!