theory CSpace_C

lemma ccorres_return_cte_mdbnode [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 cmdbnode_relation xf
         (\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr}  hs
         (return (cteMDBNode cte))
         (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s)))
           (Ptr &(ptr' s \<rightarrow>[''cteMDBNode_C'']))) s))" apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp add: return_def xf_xfu) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (erule r1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres cmdbnode_relation xf (\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs (return (cteMDBNode cte)) (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(ptr' s\<rightarrow>[''cteMDBNode_C'']))) s)) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ctes_of \<sigma> ptr = Some cte \<and> s \<in> {s. ptr_val (ptr' s) = ptr} \<and> (\<sigma>, s) \<in> rf_sr} Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(ptr' s\<rightarrow>[''cteMDBNode_C'']))) s) {s. \<exists>(rv, \<sigma>')\<in>fst (return (cteMDBNode cte) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> cmdbnode_relation rv (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. ctes_of \<sigma> ptr = Some cte \<and> s \<in> {s. ptr_val (ptr' s) = ptr} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (cteMDBNode cte) \<sigma>). (\<sigma>', xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(ptr' s\<rightarrow>[''cteMDBNode_C'']))) s) \<in> rf_sr \<and> cmdbnode_relation rv (xf (xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(ptr' s\<rightarrow>[''cteMDBNode_C'']))) s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte; (\<sigma>, x) \<in> rf_sr; ptr = ptr_val (ptr' x)\<rbrakk> \<Longrightarrow> (\<sigma>, xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) x) \<in> rf_sr \<and> cmdbnode_relation (cteMDBNode cte) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte; (\<sigma>, x) \<in> rf_sr; 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> (\<sigma>, xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) x) \<in> rf_sr \<and> cmdbnode_relation (cteMDBNode cte) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte' y. \<lbrakk>ctes_of \<sigma> (ptr_val (ptr' x)) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; 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> (\<sigma>, xfu (\<lambda>_. cteMDBNode_C cte') x) \<in> rf_sr proof (prove)
goal:
No subgoals!