theory Untyped_R

lemma createNewCaps_valid_pspace_extras:
  "\<lbrace>(\<lambda>s.    n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n
          \<and> pspace_no_overlap' ptr sz s
          \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s
          \<and> caps_overlap_reserved' {ptr .. ptr + of_nat n * 2 ^ APIType_capBits ty us - 1} s
          \<and> ksCurDomain s \<le> maxDomain
   )\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
  "\<lbrace>(\<lambda>s.    n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n
          \<and> pspace_no_overlap' ptr sz s
          \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s
          \<and> caps_overlap_reserved' {ptr .. ptr + of_nat n * 2 ^ APIType_capBits ty us - 1} s
          \<and> ksCurDomain s \<le> maxDomain
   )\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>"
  "\<lbrace>(\<lambda>s.    n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n
          \<and> pspace_no_overlap' ptr sz s
          \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s
          \<and> caps_overlap_reserved' {ptr .. ptr + of_nat n * 2 ^ APIType_capBits ty us - 1} s
          \<and> ksCurDomain s \<le> maxDomain
   )\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>"
  "\<lbrace>(\<lambda>s.    n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n
          \<and> pspace_no_overlap' ptr sz s
          \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s
          \<and> caps_overlap_reserved' {ptr .. ptr + of_nat n * 2 ^ APIType_capBits ty us - 1} s
          \<and> ksCurDomain s \<le> maxDomain
   )\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (rule hoare_grab_asm)+ apply (rule hoare_pre,rule hoare_strengthen_post[OF createNewCaps_valid_pspace]) apply (simp add:valid_pspace'_def)+ apply (rule hoare_grab_asm)+ apply (rule hoare_pre,rule hoare_strengthen_post[OF createNewCaps_valid_pspace]) apply (simp add:valid_pspace'_def)+ apply (rule hoare_grab_asm)+ apply (rule hoare_pre,rule hoare_strengthen_post[OF createNewCaps_valid_pspace]) apply (simp add:valid_pspace'_def)+ apply (rule hoare_grab_asm)+ apply (rule hoare_pre,rule hoare_strengthen_post[OF createNewCaps_valid_pspace]) apply (simp add:valid_pspace'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> &&& \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>) &&& \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> &&& \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<noteq> 0; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
 2. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 3. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 4. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrakk>n \<noteq> 0; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<lbrakk>n \<noteq> 0; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> range_cover ptr ?sz10 (APIType_capBits ty us) n
 3. \<And>rv s. \<lbrakk>n \<noteq> 0; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; valid_pspace' s\<rbrakk> \<Longrightarrow> pspace_aligned' s
 4. \<And>s. \<lbrakk>n \<noteq> 0; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz10 s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr ?sz10 s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain
 5. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 6. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 7. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. 0 < n \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 2. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 3. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 2. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 3. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> range_cover ptr ?sz24 (APIType_capBits ty us) n
 3. \<And>rv s. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; valid_pspace' s\<rbrakk> \<Longrightarrow> pspace_distinct' s
 4. \<And>s. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz24 s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr ?sz24 s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain
 5. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 6. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. 0 < n \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 2. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 2. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> range_cover ptr ?sz38 (APIType_capBits ty us) n
 3. \<And>rv s. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; valid_pspace' s\<rbrakk> \<Longrightarrow> valid_mdb' s
 4. \<And>s. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz38 s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr ?sz38 s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain
 5. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < n \<and> ptr \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> range_cover ptr ?sz52 (APIType_capBits ty us) n
 3. \<And>rv s. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; valid_pspace' s\<rbrakk> \<Longrightarrow> valid_objs' s
 4. \<And>s. \<lbrakk>0 < n; ptr \<noteq> 0; range_cover ptr sz (APIType_capBits ty us) n; pspace_no_overlap' ptr sz s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz52 s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr ?sz52 s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain proof (prove)
goal:
No subgoals!