theory Untyped_DR

lemma detype_dcorres:
  "S = {ptr..ptr + 2 ^ sz - 1}
 \<Longrightarrow> dcorres dc \<top> (\<lambda>s. invs s \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) cref s) \<and> valid_etcbs s)
        (modify (Untyped_D.detype S))
        (modify (Retype_A.detype S))" apply (rule corres_modify) apply (clarsimp simp: transform_def Untyped_D.detype_def
                        transform_cdt_def
             split del: if_split
              simp del: untyped_range.simps) apply (simp add: Untyped_D.detype_def transform_def
                   transform_current_thread_def Retype_A.detype_def transform_asid_table_def
                   detype_ext_def wrap_ext_det_ext_ext_def) apply (rule ext) apply (clarsimp simp: map_option_case restrict_map_def transform_objects_def
                        map_add_def cte_wp_at_caps_of_state
                 split: option.split) apply (drule valid_global_refsD2) apply clarsimp apply (clarsimp simp: global_refs_def transform_object_def detype_ext_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S = {ptr..ptr + 2 ^ sz - 1} \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) cref s) \<and> valid_etcbs s) (modify (Untyped_D.detype S)) (modify (Retype_A.detype S)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; True; invs s' \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) cref s') \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (Untyped_D.detype S s, Retype_A.detype S s') \<in> {ss'. transform (snd ss') = fst ss'} proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; invs s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) (a, b) s'\<rbrakk> \<Longrightarrow> transform_objects (Retype_A.detype {ptr..ptr + 2 ^ sz - 1} s') = (\<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then Some cdl_object.Untyped else cdl_objects \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s', cdl_cdt = map_lift_over transform_cslot_ptr (cdt s'), cdl_current_thread = transform_current_thread s', cdl_irq_node = interrupt_irq_node s', cdl_asid_table = transform_asid_table s', cdl_current_domain = cur_domain s'\<rparr> x) \<and> transform_current_thread (Retype_A.detype {ptr..ptr + 2 ^ sz - 1} s') = transform_current_thread s' \<and> transform_asid_table (Retype_A.detype {ptr..ptr + 2 ^ sz - 1} s') = transform_asid_table s' \<and> cur_domain (Retype_A.detype {ptr..ptr + 2 ^ sz - 1} s') = cur_domain s' proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; invs s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) (a, b) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap (\<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then None else kheap s' x) (trans_state (\<lambda>_. exst s'\<lparr>ekheap_internal := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then None else ekheap s' x\<rparr>) s')) = (\<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then Some cdl_object.Untyped else cdl_objects \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s', cdl_cdt = map_lift_over transform_cslot_ptr (cdt s'), cdl_current_thread = transform_current_thread s', cdl_irq_node = interrupt_irq_node s', cdl_asid_table = transform_asid_table s', cdl_current_domain = cur_domain s'\<rparr> x) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b x. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; invs s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) (a, b) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap (\<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then None else kheap s' x) (trans_state (\<lambda>_. exst s'\<lparr>ekheap_internal := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then None else ekheap s' x\<rparr>) s')) x = (if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then Some cdl_object.Untyped else cdl_objects \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s', cdl_cdt = map_lift_over transform_cslot_ptr (cdt s'), cdl_current_thread = transform_current_thread s', cdl_irq_node = interrupt_irq_node s', cdl_asid_table = transform_asid_table s', cdl_current_domain = cur_domain s'\<rparr> x) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b x. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; invs s'; valid_etcbs s'; caps_of_state s' (a, b) = Some (cap.UntypedCap dev ptr sz idx)\<rbrakk> \<Longrightarrow> (ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 \<longrightarrow> x = idle_thread s' \<longrightarrow> ptr \<le> idle_thread s' \<longrightarrow> \<not> idle_thread s' \<le> ptr + 2 ^ sz - 1) \<and> ((ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ sz - 1) \<longrightarrow> x = idle_thread s' \<longrightarrow> ptr \<le> idle_thread s' \<longrightarrow> \<not> idle_thread s' \<le> ptr + 2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b x. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> valid_global_refs s'
 2. \<And>s' a b x. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; invs s'; valid_etcbs s'; global_refs s' \<inter> cap_range (cap.UntypedCap dev ptr sz idx) = {}\<rbrakk> \<Longrightarrow> (ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 \<longrightarrow> x = idle_thread s' \<longrightarrow> ptr \<le> idle_thread s' \<longrightarrow> \<not> idle_thread s' \<le> ptr + 2 ^ sz - 1) \<and> ((ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ sz - 1) \<longrightarrow> x = idle_thread s' \<longrightarrow> ptr \<le> idle_thread s' \<longrightarrow> \<not> idle_thread s' \<le> ptr + 2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b x. \<lbrakk>S = {ptr..ptr + 2 ^ sz - 1}; invs s'; valid_etcbs s'; global_refs s' \<inter> cap_range (cap.UntypedCap dev ptr sz idx) = {}\<rbrakk> \<Longrightarrow> (ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 \<longrightarrow> x = idle_thread s' \<longrightarrow> ptr \<le> idle_thread s' \<longrightarrow> \<not> idle_thread s' \<le> ptr + 2 ^ sz - 1) \<and> ((ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ sz - 1) \<longrightarrow> x = idle_thread s' \<longrightarrow> ptr \<le> idle_thread s' \<longrightarrow> \<not> idle_thread s' \<le> ptr + 2 ^ sz - 1) proof (prove)
goal:
No subgoals!