theory Refine

lemma typ_at_ADeviceDataI:
  "\<lbrakk> typ_at (AArch (ADeviceData sz)) p s; pspace_relation (kheap s) (ksPSpace s');
     pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits) \<rbrakk>
        \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s'" apply (clarsimp simp add: obj_at_def a_type_def ) apply (simp split: Structures_A.kernel_object.split_asm
                     arch_kernel_obj.split_asm split: if_split_asm) apply (drule(1) pspace_relation_absD) apply (clarsimp) apply (drule_tac x = "p + n * 2 ^ pageBits" in spec) apply (drule_tac x = "\<lambda>_ obj. obj = KOUserDataDevice" in spec) apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def
                        projectKOs) apply (rule exI [where x = KOUserDataDevice]) apply (drule mp) apply (rule exI [where x = n]) apply simp apply (clarsimp simp: pspace_aligned'_def) apply (drule (1) bspec [OF _ domI]) apply (clarsimp simp: objBits_simps) apply (fastforce  dest!: pspace_distinctD'  simp: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch (ADeviceData sz)) p s; pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); kheap s p = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x41 x42. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); kheap s p = Some (ArchObj (DataPage True sz)); ko = ArchObj (DataPage True sz); x5 = DataPage True sz; x41; x42 = sz\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x41 x42. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); ko = ArchObj (DataPage True sz); x5 = DataPage True sz; x41; x42 = sz; \<forall>(x', P)\<in>obj_relation_cuts (ArchObj (DataPage True sz)) p. \<exists>z. ksPSpace s' x' = Some z \<and> P (ArchObj (DataPage True sz)) z\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; \<forall>a b. (\<exists>n. a = p + n * 2 ^ pageBits \<and> b = (\<lambda>_ obj. obj = KOUserDataDevice) \<and> n < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> (\<exists>z. ksPSpace s' a = Some z \<and> b (ArchObj (DataPage True sz)) z)\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; \<forall>b. (\<exists>na. p + n * 2 ^ pageBits = p + na * 2 ^ pageBits \<and> b = (\<lambda>_ obj. obj = KOUserDataDevice) \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> (\<exists>z. ksPSpace s' (p + n * 2 ^ pageBits) = Some z \<and> b (ArchObj (DataPage True sz)) z)\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; (\<exists>na. p + n * 2 ^ pageBits = p + na * 2 ^ pageBits \<and> (\<lambda>_ obj. obj = KOUserDataDevice) = (\<lambda>_ obj. obj = KOUserDataDevice) \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> (\<exists>z. ksPSpace s' (p + n * 2 ^ pageBits) = Some z \<and> z = KOUserDataDevice)\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; (\<exists>na. n * 2 ^ pageBits = na * 2 ^ pageBits \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s' (p + n * 2 ^ pageBits) = Some ko \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO ko) \<and> koTypeOf ko = UserDataDeviceT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO ko) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; (\<exists>na. n * 2 ^ pageBits = na * 2 ^ pageBits \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) \<and> koTypeOf KOUserDataDevice = UserDataDeviceT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) s' proof (prove)
goal (2 subgoals):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41\<rbrakk> \<Longrightarrow> \<exists>na. n * 2 ^ pageBits = na * 2 ^ pageBits \<and> na < 2 ^ (pageBitsForSize sz - pageBits)
 2. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) \<and> koTypeOf KOUserDataDevice = UserDataDeviceT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) s' proof (prove)
goal (2 subgoals):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits = n * 2 ^ pageBits \<and> n < 2 ^ (pageBitsForSize sz - pageBits)
 2. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) \<and> koTypeOf KOUserDataDevice = UserDataDeviceT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) \<and> koTypeOf KOUserDataDevice = UserDataDeviceT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); \<forall>x\<in>dom (ksPSpace s'). is_aligned x (objBitsKO (the (ksPSpace s' x))); pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice; is_aligned (p + n * 2 ^ pageBits) (objBitsKO (the (ksPSpace s' (p + n * 2 ^ pageBits))))\<rbrakk> \<Longrightarrow> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserDataDevice) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserDataDevice; is_aligned (p + n * 2 ^ pageBits) pageBits\<rbrakk> \<Longrightarrow> ps_clear (p + n * 2 ^ pageBits) pageBits s' proof (prove)
goal:
No subgoals!