theory CSpace_C

lemma ccorres_return_cte_mdbnode_safer:
  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. \<exists> cte'. ctes_of s ptr = Some cte' \<and> cteMDBNode cte = cteMDBNode 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) apply rule apply (erule r1) apply (simp add: xf_xfu) apply (drule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres cmdbnode_relation xf (\<lambda>s. \<exists>cte'. ctes_of s ptr = Some cte' \<and> cteMDBNode cte = cteMDBNode 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. (\<exists>cte'. ctes_of \<sigma> ptr = Some cte' \<and> cteMDBNode cte = cteMDBNode 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. (\<exists>cte'. ctes_of \<sigma> ptr = Some cte' \<and> cteMDBNode cte = cteMDBNode 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 cte'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ptr = ptr_val (ptr' x); ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte'; cteMDBNode cte = cteMDBNode 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') (xf (xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) x)) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ptr = ptr_val (ptr' x); ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte'; cteMDBNode cte = cteMDBNode 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
 2. \<And>\<sigma> x cte'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ptr = ptr_val (ptr' x); ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte'; cteMDBNode cte = cteMDBNode cte'\<rbrakk> \<Longrightarrow> cmdbnode_relation (cteMDBNode cte') (xf (xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) x)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ptr = ptr_val (ptr' x); ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte'; cteMDBNode cte = cteMDBNode cte'\<rbrakk> \<Longrightarrow> cmdbnode_relation (cteMDBNode cte') (xf (xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) x)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ptr = ptr_val (ptr' x); ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte'; cteMDBNode cte = cteMDBNode cte'\<rbrakk> \<Longrightarrow> 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'. \<lbrakk>ptr = ptr_val (ptr' x); ctes_of \<sigma> (ptr_val (ptr' x)) = Some cte'; cteMDBNode cte = cteMDBNode cte'; \<exists>cte'a. cslift x (cte_Ptr (ptr_val (ptr' x))) = Some cte'a \<and> cte_lift cte'a \<noteq> None \<and> cte' = cte_to_H (the (cte_lift cte'a)) \<and> c_valid_cte cte'a\<rbrakk> \<Longrightarrow> cmdbnode_relation (cteMDBNode cte') (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(ptr' x\<rightarrow>[''cteMDBNode_C'']))) proof (prove)
goal:
No subgoals!