theory ArchUntyped_AI

lemma retype_ret_valid_caps_aobj[Untyped_AI_assms]:
  "\<And>ptr sz (s::'state_ext::state_ext state) x6 us n.
  \<lbrakk>pspace_no_overlap_range_cover ptr sz s \<and> x6 \<noteq> ASIDPoolObj \<and>
  range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0\<rbrakk>
            \<Longrightarrow> \<forall>y\<in>{0..<n}. s
                   \<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n])
                              (kheap s)\<rparr> \<turnstile> ArchObjectCap (ARM_A.arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" apply (rename_tac aobject_type us n) apply (case_tac aobject_type) by (clarsimp simp: valid_cap_def default_object_def cap_aligned_def
                     cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
                     dom_def arch_default_cap_def ptr_add_def
      | intro conjI obj_at_foldr_intro
        imageI valid_vm_rights_def
      | rule is_aligned_add_multI[OF _ le_refl]
      | fastforce simp:range_cover_def obj_bits_api_def
        default_arch_object_def valid_vm_rights_def  word_bits_def a_type_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz s x6 us n. pspace_no_overlap (up_aligned_area ptr sz) s \<and> x6 \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0 \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev) proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz s aobject_type us n. pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0 \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev) proof (prove)
goal (7 subgoals):
 1. \<And>ptr sz s aobject_type us n. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0; aobject_type = SmallPageObj\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev)
 2. \<And>ptr sz s aobject_type us n. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0; aobject_type = LargePageObj\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev)
 3. \<And>ptr sz s aobject_type us n. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0; aobject_type = SectionObj\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev)
 4. \<And>ptr sz s aobject_type us n. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0; aobject_type = SuperSectionObj\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev)
 5. \<And>ptr sz s aobject_type us n. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0; aobject_type = PageTableObj\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev)
 6. \<And>ptr sz s aobject_type us n. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0; aobject_type = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev)
 7. \<And>ptr sz s aobject_type us n. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> aobject_type \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n \<and> ptr \<noteq> 0; aobject_type = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject aobject_type) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject aobject_type) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap aobject_type (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject aobject_type) us)) us dev)