theory Retype_C

lemma createNewCaps_valid_cap_hd:
    "\<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 ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits) \<and>
       ptr \<noteq> 0 \<rbrace>
    createNewCaps ty ptr n us dev
  \<lbrace>\<lambda>r s. s \<turnstile>' hd r\<rbrace>" apply (cases "n = 0") apply simp apply (rule hoare_chain) apply (rule hoare_vcg_conj_lift) apply (rule createNewCaps_ret_len) apply (rule createNewCaps_valid_cap'[where sz=sz]) apply (clarsimp simp: range_cover_n_wb) 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 dev \<lbrace>\<lambda>r. valid_cap' (hd r)\<rbrace> proof (prove)
goal (2 subgoals):
 1. n = 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 dev \<lbrace>\<lambda>r. valid_cap' (hd r)\<rbrace>
 2. n \<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 dev \<lbrace>\<lambda>r. valid_cap' (hd r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. n \<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 dev \<lbrace>\<lambda>r. valid_cap' (hd r)\<rbrace> proof (prove)
goal (3 subgoals):
 1. n \<noteq> 0 \<Longrightarrow> \<lbrace>?P1\<rbrace> createNewCaps ty ptr n us dev \<lbrace>?Q1\<rbrace>
 2. \<And>s. \<lbrakk>n \<noteq> 0; 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\<rbrakk> \<Longrightarrow> ?P1 s
 3. \<And>rv s. \<lbrakk>n \<noteq> 0; ?Q1 rv s\<rbrakk> \<Longrightarrow> valid_cap' (hd rv) s proof (prove)
goal (4 subgoals):
 1. n \<noteq> 0 \<Longrightarrow> \<lbrace>?P5\<rbrace> createNewCaps ty ptr n us dev \<lbrace>?Q5\<rbrace>
 2. n \<noteq> 0 \<Longrightarrow> \<lbrace>?P'5\<rbrace> createNewCaps ty ptr n us dev \<lbrace>?Q'5\<rbrace>
 3. \<And>s. \<lbrakk>n \<noteq> 0; 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\<rbrakk> \<Longrightarrow> ?P5 s \<and> ?P'5 s
 4. \<And>rv s. \<lbrakk>n \<noteq> 0; ?Q5 rv s \<and> ?Q'5 rv s\<rbrakk> \<Longrightarrow> valid_cap' (hd rv) s proof (prove)
goal (3 subgoals):
 1. n \<noteq> 0 \<Longrightarrow> \<lbrace>?P'5\<rbrace> createNewCaps ty ptr n us dev \<lbrace>?Q'5\<rbrace>
 2. \<And>s. \<lbrakk>n \<noteq> 0; 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\<rbrakk> \<Longrightarrow> K (n < 2 ^ word_bits \<and> n \<noteq> 0) s \<and> ?P'5 s
 3. \<And>rv s. \<lbrakk>n \<noteq> 0; n = length rv \<and> ?Q'5 rv s\<rbrakk> \<Longrightarrow> valid_cap' (hd rv) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>n \<noteq> 0; 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\<rbrakk> \<Longrightarrow> K (n < 2 ^ word_bits \<and> n \<noteq> 0) s \<and> 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
 2. \<And>rv s. \<lbrakk>n \<noteq> 0; n = length rv \<and> (\<forall>cap\<in>set rv. valid_cap' cap s)\<rbrakk> \<Longrightarrow> valid_cap' (hd rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>n \<noteq> 0; n = length rv \<and> (\<forall>cap\<in>set rv. valid_cap' cap s)\<rbrakk> \<Longrightarrow> valid_cap' (hd rv) s proof (prove)
goal:
No subgoals!