theory Detype_R

lemma createObject_pspace_aligned_distinct':
  "\<lbrace>pspace_aligned' and K (is_aligned ptr (APIType_capBits ty us))
   and pspace_distinct' and pspace_no_overlap' ptr (APIType_capBits ty us)
   and K (ty = APIObjectType apiobject_type.CapTableObject \<longrightarrow> us < 28)\<rbrace>
  createObject ty ptr us d
  \<lbrace>\<lambda>xa s. pspace_aligned' s \<and> pspace_distinct' s\<rbrace>" apply (rule hoare_pre) apply (wp placeNewObject_pspace_aligned' unless_wp
      placeNewObject_pspace_distinct'
    | simp add:ARM_H.createObject_def
      Retype_H.createObject_def objBits_simps
      curDomain_def placeNewDataObject_def
          split del: if_split
    | wpc | intro conjI impI)+ apply (auto simp:APIType_capBits_def pdBits_def objBits_simps' pteBits_def pdeBits_def
    pageBits_def word_bits_def archObjSize_def ptBits_def ARM_H.toAPIType_def
    split:ARM_H.object_type.splits apiobject_type.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and K (is_aligned ptr (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ptr (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)\<rbrace> global.createObject ty ptr us d \<lbrace>\<lambda>xa s. pspace_aligned' s \<and> pspace_distinct' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> global.createObject ty ptr us d \<lbrace>\<lambda>xa s. pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
 2. \<And>s. (pspace_aligned' and K (is_aligned ptr (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ptr (APIType_capBits ty us) and K (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28)) s \<Longrightarrow> ?Q s proof (prove)
goal (33 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits SmallPageObject us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits SmallPageObject us) s; toAPIType SmallPageObject = None; ty = SmallPageObject\<rbrakk> \<Longrightarrow> is_aligned ptr pageBits
 2. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = SmallPageObject\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr pageBits s
 3. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = LargePageObject\<rbrakk> \<Longrightarrow> is_aligned ptr (pageBits + 4)
 4. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = LargePageObject\<rbrakk> \<Longrightarrow> pageBits + 4 < word_bits
 5. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = LargePageObject\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (pageBits + 4) s
 6. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = LargePageObject\<rbrakk> \<Longrightarrow> pageBits + 4 < word_bits
 7. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = LargePageObject\<rbrakk> \<Longrightarrow> is_aligned ptr (pageBits + 4)
 8. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = LargePageObject\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (pageBits + 4) s
 9. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = SectionObject\<rbrakk> \<Longrightarrow> is_aligned ptr (pageBits + 8)
 10. \<And>s. \<lbrakk>pspace_aligned' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28); toAPIType ty = None; ty = SectionObject\<rbrakk> \<Longrightarrow> pageBits + 8 < word_bits
A total of 33 subgoals... proof (prove)
goal:
No subgoals!