theory CSpace_C

lemma ccorres_move_ptr_safe_Seq:
  "ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;d) \<Longrightarrow>
  ccorres_underlying rf_sr \<Gamma> r xf arrel axf
  (A and cte_wp_at' (\<lambda>_. True) (ptr_val dest) and K (dest = cte_Ptr (ptr_val dest)))
  (C' \<inter> \<lbrace>True\<rbrace>) hs a
  (Guard MemorySafety \<lbrace>ptr_safe (dest) (hrs_htd \<acute>t_hrs) \<rbrace> c;;d)" apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard_Seq) apply simp apply (clarsimp simp:cte_wp_at_ctes_of) apply (drule(1) rf_sr_ctes_of_clift) apply clarsimp apply (erule cslift_ptr_safe) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d) \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (A and cte_wp_at' (\<lambda>_. True) (ptr_val dest) and K (dest = cte_Ptr (ptr_val dest))) (C' \<inter> \<lbrace>True\<rbrace>) hs a (Guard MemorySafety \<lbrace>ptr_safe dest (hrs_htd \<acute>t_hrs)\<rbrace> c;;
d) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d) \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (Guard MemorySafety \<lbrace>ptr_safe dest (hrs_htd \<acute>t_hrs)\<rbrace> c;;
d)
 2. \<And>s s'. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d); (s, s') \<in> rf_sr; (A and cte_wp_at' (\<lambda>_. True) (ptr_val dest) and K (dest = cte_Ptr (ptr_val dest))) s; s' \<in> C' \<inter> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d) \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?Q ?C'3 hs a (c;;
d)
 2. \<And>s s'. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d); (s, s') \<in> rf_sr; (A and cte_wp_at' (\<lambda>_. True) (ptr_val dest) and K (dest = cte_Ptr (ptr_val dest))) s; s' \<in> C' \<inter> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?C'3 \<inter> \<lbrace>ptr_safe dest (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d); (s, s') \<in> rf_sr; (A and cte_wp_at' (\<lambda>_. True) (ptr_val dest) and K (dest = cte_Ptr (ptr_val dest))) s; s' \<in> C' \<inter> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> A s \<and> s' \<in> C' \<inter> \<lbrace>ptr_safe dest (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d); (s, s') \<in> rf_sr; s' \<in> C'; A s; ctes_of s (ptr_val dest) = Some cte\<rbrakk> \<Longrightarrow> ptr_safe dest (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d); s' \<in> C'; A s; ctes_of s (ptr_val dest) = Some cte; \<exists>cte'. cslift s' (cte_Ptr (ptr_val dest)) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> ptr_safe dest (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte' y. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;
d); s' \<in> C'; A s; ctes_of s (ptr_val dest) = Some (cte_to_H y); cslift s' dest = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ptr_safe dest (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal:
No subgoals!