theory Detype_C

lemma deleteObjects_ccorres[corres]:
  "ccorres dc xfdc
     (cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap d ptr bits idx) p and
      (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and
      invs' and ct_active' and sch_act_simple and
      K ( 2 \<le> bits \<and> bits < word_bits))
     UNIV hs
     (deleteObjects ptr bits)
     (Seq (global_htd_update (\<lambda>_. typ_region_bytes ptr bits))
          (Basic (\<lambda>s. globals_update
             (ghost'state_'_update (gs_clear_region ptr bits)) s)))" apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard_Seq) apply (rule Corres_UL_C.ccorres_exec_cong
                 [THEN iffD2, OF _ deleteObjects_ccorres'[where idx=idx and p=p and d=d]]) apply (simp add: exec_Basic_Seq_Basic o_def
                    hrs_ghost_update_comm[simplified o_def]) apply clarsimp apply (frule(2) untyped_cap_rf_sr_ptr_bits_domain) by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                        kernel_data_refs_domain_eq_rotate htd_safe_typ_region_bytes
                        untyped_cap_rf_sr_ptr_bits_domain)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and invs' and ct_active' and sch_act_simple and K (2 \<le> bits \<and> bits < word_bits)) UNIV hs (deleteObjects ptr bits) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (typ_region_bytes ptr bits (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (typ_region_bytes ptr bits)));;
\<acute>globals :== ghost'state_'_update (gs_clear_region ptr bits)) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q ?Q' hs (deleteObjects ptr bits) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (typ_region_bytes ptr bits (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (typ_region_bytes ptr bits)));;
\<acute>globals :== ghost'state_'_update (gs_clear_region ptr bits))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and invs' and ct_active' and sch_act_simple and K (2 \<le> bits \<and> bits < word_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q ?C'3 hs (deleteObjects ptr bits) (\<acute>globals :== t_hrs_'_update (hrs_htd_update (typ_region_bytes ptr bits));;
\<acute>globals :== ghost'state_'_update (gs_clear_region ptr bits))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and invs' and ct_active' and sch_act_simple and K (2 \<le> bits \<and> bits < word_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?C'3 \<inter> \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (typ_region_bytes ptr bits (hrs_htd \<acute>t_hrs))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s s'. s \<in> UNIV \<Longrightarrow> \<Gamma>\<turnstile> \<langle>\<acute>globals :== t_hrs_'_update (hrs_htd_update (typ_region_bytes ptr bits));;
\<acute>globals :== ghost'state_'_update (gs_clear_region ptr bits),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>\<acute>globals :== t_hrs_'_update (hrs_htd_update (typ_region_bytes ptr bits)) \<circ> ghost'state_'_update (gs_clear_region ptr bits),Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and invs' and ct_active' and sch_act_simple and K (2 \<le> bits \<and> bits < word_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and invs' and ct_active' and sch_act_simple and K (2 \<le> bits \<and> bits < word_bits)) s \<and> s' \<in> UNIV \<inter> \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (typ_region_bytes ptr bits (hrs_htd \<acute>t_hrs))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and invs' and ct_active' and sch_act_simple and K (2 \<le> bits \<and> bits < word_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and invs' and ct_active' and sch_act_simple and K (2 \<le> bits \<and> bits < word_bits)) s \<and> s' \<in> UNIV \<inter> \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (typ_region_bytes ptr bits (hrs_htd \<acute>t_hrs))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); invs' s; ct_active' s; sch_act_simple s; 2 \<le> bits; bits < word_bits\<rbrakk> \<Longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s'))) \<and> htd_safe domain (typ_region_bytes ptr bits (hrs_htd (t_hrs_' (globals s')))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); invs' s; ct_active' s; sch_act_simple s; 2 \<le> bits; bits < word_bits; {ptr..+2 ^ bits} \<subseteq> domain\<rbrakk> \<Longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s'))) \<and> htd_safe domain (typ_region_bytes ptr bits (hrs_htd (t_hrs_' (globals s'))))