theory CSpace_C

lemma ccorres_move_ptr_safe:
  "ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a c \<Longrightarrow>
  ccorres_underlying rf_sr \<Gamma> r xf arrel axf
  (A and K (dest = cte_Ptr (ptr_val dest)) and cte_wp_at' (\<lambda>_. True) (ptr_val dest))
  (C' \<inter> \<lbrace>True\<rbrace>) hs a (Guard MemorySafety \<lbrace>ptr_safe (dest) (hrs_htd \<acute>t_hrs) \<rbrace> c)" apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard) apply simp apply (clarsimp simp:cte_wp_at_ctes_of) apply (drule(1) rf_sr_ctes_of_clift) apply (case_tac dest) apply (clarsimp simp:ptr_coerce_def) 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 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (A and K (dest = cte_Ptr (ptr_val dest)) and cte_wp_at' (\<lambda>_. True) (ptr_val dest)) (C' \<inter> \<lbrace>True\<rbrace>) hs a (Guard MemorySafety \<lbrace>ptr_safe dest (hrs_htd \<acute>t_hrs)\<rbrace> c) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a c \<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)
 2. \<And>s s'. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a c; (s, s') \<in> rf_sr; (A and K (dest = cte_Ptr (ptr_val dest)) and cte_wp_at' (\<lambda>_. True) (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 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?Q ?C'3 hs a c
 2. \<And>s s'. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a c; (s, s') \<in> rf_sr; (A and K (dest = cte_Ptr (ptr_val dest)) and cte_wp_at' (\<lambda>_. True) (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; (s, s') \<in> rf_sr; (A and K (dest = cte_Ptr (ptr_val dest)) and cte_wp_at' (\<lambda>_. True) (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; (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; 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 x. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a c; 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'; dest = cte_Ptr x\<rbrakk> \<Longrightarrow> ptr_safe dest (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x cte' y. \<lbrakk>ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a c; s' \<in> C'; A s; ctes_of s x = Some (cte_to_H y); dest = cte_Ptr x; cslift s' (cte_Ptr x) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ptr_safe (cte_Ptr x) (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal:
No subgoals!