theory Untyped_DR

lemma retype_transform_obj_ref_available:
  "\<lbrakk>pspace_no_overlap_range_cover ptr sz s'; s = transform s'; valid_pspace s'; valid_idle s';
    range_cover ptr sz (obj_bits_api ty us) n;
    y \<in> set (retype_addrs ptr ty n us)\<rbrakk>
  \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq>
    (cdl_objects s) -` {Some Types_D.Untyped}" apply (clarsimp simp:retype_transform_obj_ref_def | rule conjI)+ apply (rule transform_none_to_untyped, simp) apply (rule ccontr, clarsimp) apply (drule(1) retype_addrs_range_subset[where p = y]) apply (drule(1) pspace_no_overlap_obj_range) apply (simp only: field_simps) apply (drule(1) disjoint_subset2) apply (clarsimp simp:obj_bits_api_def) apply (drule p_in_obj_range) apply clarsimp+ apply auto[1] apply (drule(2) pspace_no_overlap_into_Int_none) apply (clarsimp simp: transform_def restrict_map_def map_add_def transform_objects_def
                 split: if_splits option.splits) apply (fastforce simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects s -` {Some cdl_object.Untyped} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1\<rbrakk> \<Longrightarrow> cdl_objects (transform s') x = Some cdl_object.Untyped
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1\<rbrakk> \<Longrightarrow> kheap s' x = None
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x ya. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; kheap s' x = Some ya\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x ya. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; kheap s' x = Some ya; {y..y + 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; kheap s' x = Some ya; {y..y + 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; obj_range x ya \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; kheap s' x = Some ya; {y..y + 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; obj_range x ya \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; kheap s' x = Some ya; obj_range x ya \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range x ya \<inter> {y..y + 2 ^ obj_bits_api apiobject_type.Untyped us - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz us n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; kheap s' x = Some ya; obj_range x ya \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range x ya \<inter> {y..y + 2 ^ us - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (4 subgoals):
 1. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz us n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; obj_range x ya \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range x ya \<inter> {y..y + 2 ^ us - 1} = {}\<rbrakk> \<Longrightarrow> pspace_aligned s'
 2. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz us n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; obj_range x ya \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range x ya \<inter> {y..y + 2 ^ us - 1} = {}\<rbrakk> \<Longrightarrow> valid_objs s'
 3. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz us n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; obj_range x ya \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range x ya \<inter> {y..y + 2 ^ us - 1} = {}; x \<in> obj_range x ya\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (2 subgoals):
 1. \<And>x ya. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz us n; ty = apiobject_type.Untyped; y \<le> x; x \<le> y + 2 ^ us - 1; obj_range x ya \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range x ya \<inter> {y..y + 2 ^ us - 1} = {}; x \<in> obj_range x ya\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us); set (retype_addrs ptr ty n us) \<inter> dom (kheap s') = {}\<rbrakk> \<Longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> cdl_objects (transform s') y = Some cdl_object.Untyped proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = \<lparr>cdl_arch = ARM11, cdl_objects = \<lambda>x. case if x \<noteq> idle_thread s' then kheap s' x else None of None \<Rightarrow> if x \<noteq> idle_thread s' then Some cdl_object.Untyped else None | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state s') x (if x \<noteq> idle_thread s' then ekheap s' x else None)) xa, cdl_cdt = transform_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>; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \<in> set (retype_addrs ptr ty n us); set (retype_addrs ptr ty n us) \<inter> dom (kheap s') = {}\<rbrakk> \<Longrightarrow> (kheap s' y = None \<longrightarrow> y = idle_thread s' \<longrightarrow> ty = apiobject_type.Untyped) \<and> (\<forall>x2. kheap s' y = Some x2 \<longrightarrow> (y \<noteq> idle_thread s' \<longrightarrow> ty \<noteq> apiobject_type.Untyped \<longrightarrow> transform_object (machine_state s') y (ekheap s' y) x2 = cdl_object.Untyped) \<and> (y = idle_thread s' \<longrightarrow> ty = apiobject_type.Untyped)) proof (prove)
goal:
No subgoals!