theory Retype_C

lemma createObject_valid_cap':
  "\<lbrace>\<lambda>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and>
         valid_pspace' s \<and>
         is_aligned ptr (APIType_capBits ty us) \<and>
          APIType_capBits ty us < word_bits \<and>
         (ty = APIObjectType apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and>
         (ty = APIObjectType apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits) \<and> ptr \<noteq> 0\<rbrace>
    createObject ty ptr us dev \<lbrace>\<lambda>r s. s \<turnstile>' r\<rbrace>" apply (simp add:createObject_def3) apply (rule hoare_pre) apply wp apply (rule_tac Q = "\<lambda>r s. r \<noteq> [] \<and> Q r s" for Q in hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule hoare_strengthen_post[OF createNewCaps_ret_len]) apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_valid_cap'[where sz = "APIType_capBits ty us"]]) apply assumption apply clarsimp apply (clarsimp simp add:word_bits_conv range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> global.createObject ty ptr us dev \<lbrace>valid_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>valid_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>valid_cap'\<rbrace>
 2. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>m. valid_cap' (hd m)\<rbrace>
 2. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q1\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>r s. r \<noteq> [] \<and> ?Q13 r s\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> valid_cap' (hd rv) s
 3. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>rv s. rv \<noteq> []\<rbrace>
 2. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> valid_cap' (hd rv) s
 4. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> ?P14 s \<and> ?P'14 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. Suc 0 = length rv \<Longrightarrow> rv \<noteq> []
 2. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> valid_cap' (hd rv) s
 4. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> valid_cap' (hd rv) s
 3. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<forall>cap\<in>set rv. valid_cap' cap s \<Longrightarrow> ?Q13 rv s
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> valid_cap' (hd rv) s
 3. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> Suc 0 \<noteq> 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<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 proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (\<forall>cap\<in>set rv. valid_cap' cap s) \<Longrightarrow> valid_cap' (hd rv) s
 2. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> Suc 0 \<noteq> 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<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 proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<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> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> valid_pspace' s \<and> Suc 0 \<noteq> 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<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 proof (prove)
goal:
No subgoals!