theory Untyped_R

lemma createNewCaps_valid_cap':
  "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and>
        valid_pspace' s \<and> n \<noteq> 0 \<and>
        range_cover ptr sz (APIType_capBits ty us) n \<and>
        (ty = APIObjectType ArchTypes_H.CapTableObject \<longrightarrow> 0 < us) \<and>
        (ty = APIObjectType apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits) \<and>
       ptr \<noteq> 0 \<rbrace>
    createNewCaps ty ptr n us d
  \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. s \<turnstile>' cap\<rbrace>" apply (rule hoare_assume_pre) apply clarsimp apply (erule createNewCaps_valid_cap) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> n \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits) \<and> ptr \<noteq> 0\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> n \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits) \<and> ptr \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> n \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits) \<and> ptr \<noteq> 0\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; valid_pspace' s; 0 < n; range_cover ptr sz (APIType_capBits ty us) n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; valid_pspace' s; 0 < n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; valid_pspace' s; 0 < n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> 0 < us
 3. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; valid_pspace' s; 0 < n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; ptr \<noteq> 0; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
 4. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; valid_pspace' s; 0 < n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal:
No subgoals!