theory Retype_C

lemma mdb_node_get_mdbNext_heap_ccorres:
  "ccorres (=) ret__unsigned_' \<top> UNIV hs
  (liftM (mdbNext \<circ> cteMDBNode) (getCTE parent))
  (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext(h_val
                           (hrs_mem \<acute>t_hrs)
                           (Ptr &((Ptr parent :: cte_C ptr) \<rightarrow>[''cteMDBNode_C'']))))" apply (simp add: ccorres_liftM_simp) apply (rule ccorres_add_return2) apply (rule ccorres_guard_imp2) apply (rule ccorres_getCTE) apply (rule_tac  P = "\<lambda>s. ctes_of s parent = Some x" in ccorres_from_vcg [where P' = UNIV]) apply (rule allI, rule conseqPre) apply vcg apply (clarsimp simp: return_def) apply (drule cmap_relation_cte) apply (erule (1) cmap_relationE1) apply (simp add: typ_heap_simps) apply (drule ccte_relation_cmdbnode_relation) apply (erule mdbNext_CL_mdb_node_lift_eq_mdbNext [symmetric]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (=) ret__unsigned_' (\<lambda>_. True) UNIV hs (liftM (mdbNext \<circ> cteMDBNode) (getCTE parent)) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) proof (prove)
goal (1 subgoal):
 1. ccorres ((=) \<circ> (mdbNext \<circ> cteMDBNode)) ret__unsigned_' (\<lambda>_. True) UNIV hs (getCTE parent) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) proof (prove)
goal (1 subgoal):
 1. ccorres ((=) \<circ> (mdbNext \<circ> cteMDBNode)) ret__unsigned_' (\<lambda>_. True) UNIV hs (getCTE parent >>= return) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) proof (prove)
goal (2 subgoals):
 1. ccorres ((=) \<circ> (mdbNext \<circ> cteMDBNode)) ret__unsigned_' ?Q2 ?Q'2 hs (getCTE parent >>= return) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q2 s \<and> s' \<in> ?Q'2 proof (prove)
goal (2 subgoals):
 1. \<And>x. ccorres ((=) \<circ> (mdbNext \<circ> cteMDBNode)) ret__unsigned_' (?P5 x) (?P'5 x) hs (return x) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ?P5 cte s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> ?P'5 (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ctes_of \<sigma> parent = Some x \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ((=) \<circ> (mdbNext \<circ> cteMDBNode)) rv (ret__unsigned_' s)}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>x \<sigma>. \<Gamma>\<turnstile> (?P'12 x \<sigma>) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ((=) \<circ> (mdbNext \<circ> cteMDBNode)) rv (ret__unsigned_' s)}
 2. \<And>x \<sigma>. {s. ctes_of \<sigma> parent = Some x \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'12 x \<sigma>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma>. {s. ctes_of \<sigma> parent = Some x \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<forall>t. ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))\<rparr>) \<in> rf_sr \<and> mdbNext (cteMDBNode rv) = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))))}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma> xa t. \<lbrakk>ctes_of \<sigma> parent = Some x; (\<sigma>, xa) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals xa))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode x) = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals xa))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma> xa t. \<lbrakk>ctes_of \<sigma> parent = Some x; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals xa))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); cmap_relation (ctes_of \<sigma>) (cslift xa) cte_Ptr ccte_relation\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode x) = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals xa))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma> xa t y'. \<lbrakk>ctes_of \<sigma> parent = Some x; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals xa))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); ctes_of \<sigma> parent = Some x; ccte_relation x y'; cslift xa (cte_Ptr parent) = Some y'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode x) = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals xa))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma> xa t y'. \<lbrakk>ret__unsigned_' t = mdbNext_CL (mdb_node_lift (cteMDBNode_C y')); ctes_of \<sigma> parent = Some x; ccte_relation x y'; cslift xa (cte_Ptr parent) = Some y'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode x) = mdbNext_CL (mdb_node_lift (cteMDBNode_C y'))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma> xa t y'. \<lbrakk>ret__unsigned_' t = mdbNext_CL (mdb_node_lift (cteMDBNode_C y')); ctes_of \<sigma> parent = Some x; cslift xa (cte_Ptr parent) = Some y'; cmdbnode_relation (cteMDBNode x) (cteMDBNode_C y')\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode x) = mdbNext_CL (mdb_node_lift (cteMDBNode_C y'))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = 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 parent = Some cte \<longrightarrow> ctes_of s parent = Some cte) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr parent) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV} proof (prove)
goal:
No subgoals!