theory Retype_R

lemma cwo_ret:
  assumes  cover:"range_cover ptr sz v n"
  assumes not_0:"n\<noteq> 0"
  shows result: "\<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace>
           createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs
          \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits).
                 typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace>" proof - note create_objs_device = hoare_post_imp [OF _ hoare_conj [OF createObjects_ret
     createObjects_ko_at[where val = UserDataDevice,simplified]]] note create_objs_normal = hoare_post_imp [OF _ hoare_conj [OF createObjects_ret
     createObjects_ko_at[where val = UserData,simplified]]] show ?thesis apply (cases dev) apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (rule create_objs_device) apply (clarsimp simp add: pageBits_def) apply (drule bspec, simp, drule spec, drule(1) mp) apply (simp add: typ_at'_def obj_at'_real_def objBits_simps pageBits_def shiftl_t2n field_simps) apply (erule ko_wp_at'_weakenE) apply (clarsimp simp add: projectKO_opts_defs split: kernel_object.splits) apply (rule le_less_trans[OF _ power_strict_increasing]) apply (rule range_cover.range_cover_n_le(1)[OF cover]) apply (simp add: word_bits_def pageBits_def not_0)+ apply (rule range_cover_rel[OF cover]) apply (simp add: objBitsKO_def pageBits_def not_0)+ using not_0 apply simp_all apply (clarsimp simp add: projectKO_def return_def
      projectKO_opts_defs split: kernel_object.splits) apply (rule hoare_gen_asm[unfolded K_def]) apply (rule hoare_pre) apply (rule create_objs_normal) apply (clarsimp simp add: pageBits_def) apply (drule bspec, simp, drule spec, drule(1) mp) apply (simp add: typ_at'_def obj_at'_real_def objBits_simps pageBits_def shiftl_t2n field_simps) apply (erule ko_wp_at'_weakenE) apply (clarsimp simp add: projectKO_opts_defs split: kernel_object.splits) apply (rule le_less_trans[OF _ power_strict_increasing]) apply (rule range_cover.range_cover_n_le(1)[OF cover]) apply (simp add: word_bits_def pageBits_def not_0)+ apply (rule range_cover_rel[OF cover]) apply (simp add: objBitsKO_def pageBits_def not_0)+ using not_0 apply simp_all apply (clarsimp simp add: projectKO_def return_def
      projectKO_opts_defs split: kernel_object.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (state)
this:
\<lbrakk>\<And>rv s. ((\<lambda>r s. r = map (\<lambda>p. ptr_add ?ptr2 (p * 2 ^ objBitsKO ?ko2 * 2 ^ ?gbits2)) [0..<?n2]) and (\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ ?gbits2. obj_at' (\<lambda>k. True) (x + (offs << objBitsKO ?ko2)) s)) rv s \<Longrightarrow> ?R rv s; ?n2 < 2 ^ word_bits; ?n2 \<noteq> 0; range_cover ?ptr2 ?sz2 (objBitsKO ?ko2 + ?gbits2) ?n2; 0 < ?n2; projectKO_opt ?ko2 = Some UserDataDevice\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ?ptr2 ?sz2 s \<and> valid_pspace' s)\<rbrace> createObjects ?ptr2 ?n2 ?ko2 ?gbits2 \<lbrace>?R\<rbrace>

goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (state)
this:
\<lbrakk>\<And>rv s. ((\<lambda>r s. r = map (\<lambda>p. ptr_add ?ptr2 (p * 2 ^ objBitsKO ?ko2 * 2 ^ ?gbits2)) [0..<?n2]) and (\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ ?gbits2. obj_at' (\<lambda>k. True) (x + (offs << objBitsKO ?ko2)) s)) rv s \<Longrightarrow> ?R rv s; ?n2 < 2 ^ word_bits; ?n2 \<noteq> 0; range_cover ?ptr2 ?sz2 (objBitsKO ?ko2 + ?gbits2) ?n2; 0 < ?n2; projectKO_opt ?ko2 = Some UserData\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ?ptr2 ?sz2 s \<and> valid_pspace' s)\<rbrace> createObjects ?ptr2 ?n2 ?ko2 ?gbits2 \<lbrace>?R\<rbrace>

goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace>
 2. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace'\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace>
 2. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> \<lbrace>?Q3\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace>
 2. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv s. \<lbrakk>dev; v = 12 + bs; ((\<lambda>r s. r = map (\<lambda>p. ptr_add ptr (p * 2 ^ objBitsKO (if dev then KOUserDataDevice else KOUserData) * 2 ^ bs)) [0..<n]) and (\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ bs. obj_at' (\<lambda>k. True) (x + (offs << objBitsKO (if dev then KOUserDataDevice else KOUserData))) s)) rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 7. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 8. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s x p. \<lbrakk>dev; v = 12 + bs; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ bs. obj_at' (\<lambda>k. True) (ptr_add ptr (x * 2 ^ objBitsKO KOUserDataDevice * 2 ^ bs) + (offs << objBitsKO KOUserDataDevice)) s; x < n; p < 2 ^ bs\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (ptr_add ptr (x * 2 ^ objBitsKO KOUserDataDevice * 2 ^ bs) + p * 0x1000) s
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 7. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 8. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s x p. \<lbrakk>dev; v = 12 + bs; x < n; p < 2 ^ bs; obj_at' (\<lambda>k. True) (ptr_add ptr (x * 2 ^ objBitsKO KOUserDataDevice * 2 ^ bs) + (p << objBitsKO KOUserDataDevice)) s\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (ptr_add ptr (x * 2 ^ objBitsKO KOUserDataDevice * 2 ^ bs) + p * 0x1000) s
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 7. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 8. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s x p. \<lbrakk>dev; v = bs + 12; x < n; p < 2 ^ bs; ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (p * 0x1000 + ptr_add ptr (x * (2 ^ bs * 4096))) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p * 0x1000 + ptr_add ptr (x * (2 ^ bs * 4096))) s
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 7. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 8. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s x p ko. \<lbrakk>dev; v = bs + 12; x < n; p < 2 ^ bs; \<exists>obj. projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> koTypeOf ko = UserDataDeviceT
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 7. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 8. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 6. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 7. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<le> 2 ^ ?n75
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> ?n75 < word_bits
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 1 < 2
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 6. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 7. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 8. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 9. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> LENGTH(32) - v < word_bits
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO (if dev then KOUserDataDevice else KOUserData) + bs) n
 5. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 7. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 8. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz8 (objBitsKO KOUserDataDevice + bs) n
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 4. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz8 s \<and> valid_pspace' s)) s
 5. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> objBitsKO KOUserDataDevice + bs \<le> v
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> n = 2 ^ (v - (objBitsKO KOUserDataDevice + bs)) * n
 3. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 4. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 5. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s)) s
 6. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 3. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s)) s
 4. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
using this:
n \<noteq> 0

goal (4 subgoals):
 1. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 2. \<lbrakk>dev; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt (if dev then KOUserDataDevice else KOUserData) = Some UserDataDevice
 3. \<And>s. \<lbrakk>dev; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s)) s
 4. \<not> dev \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dev; v = 12 + bs; 0 < n\<rbrakk> \<Longrightarrow> projectKO_opt KOUserDataDevice = Some UserDataDevice
 2. \<lbrakk>\<not> dev; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and (\<lambda>y. v = 12 + bs)\<rbrace> createObjects ptr n KOUserData bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' UserDataT (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> dev; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and (\<lambda>y. v = 12 + bs)\<rbrace> createObjects ptr n KOUserData bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' UserDataT (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' ptr sz and valid_pspace'\<rbrace> createObjects ptr n KOUserData bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' UserDataT (x + p * 2 ^ pageBits) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> \<lbrace>?Q108\<rbrace> createObjects ptr n KOUserData bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' UserDataT (x + p * 2 ^ pageBits) s\<rbrace>
 2. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ?Q108 s proof (prove)
goal (7 subgoals):
 1. \<And>rv s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; ((\<lambda>r s. r = map (\<lambda>p. ptr_add ptr (p * 2 ^ objBitsKO KOUserData * 2 ^ bs)) [0..<n]) and (\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ bs. obj_at' (\<lambda>k. True) (x + (offs << objBitsKO KOUserData)) s)) rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' UserDataT (x + p * 2 ^ pageBits) s
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 7. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (7 subgoals):
 1. \<And>s x p. \<lbrakk>\<not> dev; v = 12 + bs; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ bs. obj_at' (\<lambda>k. True) (ptr_add ptr (x * 2 ^ objBitsKO KOUserData * 2 ^ bs) + (offs << objBitsKO KOUserData)) s; x < n; p < 2 ^ bs\<rbrakk> \<Longrightarrow> typ_at' UserDataT (ptr_add ptr (x * 2 ^ objBitsKO KOUserData * 2 ^ bs) + p * 0x1000) s
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 7. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (7 subgoals):
 1. \<And>s x p. \<lbrakk>\<not> dev; v = 12 + bs; x < n; p < 2 ^ bs; obj_at' (\<lambda>k. True) (ptr_add ptr (x * 2 ^ objBitsKO KOUserData * 2 ^ bs) + (p << objBitsKO KOUserData)) s\<rbrakk> \<Longrightarrow> typ_at' UserDataT (ptr_add ptr (x * 2 ^ objBitsKO KOUserData * 2 ^ bs) + p * 0x1000) s
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 7. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (7 subgoals):
 1. \<And>s x p. \<lbrakk>\<not> dev; v = bs + 12; x < n; p < 2 ^ bs; ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (p * 0x1000 + ptr_add ptr (x * (2 ^ bs * 4096))) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p * 0x1000 + ptr_add ptr (x * (2 ^ bs * 4096))) s
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 7. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (7 subgoals):
 1. \<And>s x p ko. \<lbrakk>\<not> dev; v = bs + 12; x < n; p < 2 ^ bs; \<exists>obj. projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> koTypeOf ko = UserDataT
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 7. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 6. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (8 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<le> 2 ^ ?n180
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> ?n180 < word_bits
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 1 < 2
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 6. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 7. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 8. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> LENGTH(32) - v < word_bits
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 5. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 6. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 7. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> range_cover ptr ?sz113 (objBitsKO KOUserData + bs) n
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 4. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr ?sz113 s \<and> valid_pspace' s)) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> objBitsKO KOUserData + bs \<le> v
 2. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> n = 2 ^ (v - (objBitsKO KOUserData + bs)) * n
 3. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> 0 < n
 4. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 5. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s)) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 2. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s)) s proof (prove)
using this:
n \<noteq> 0

goal (2 subgoals):
 1. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData
 2. \<And>s. \<lbrakk>\<not> dev; 0 < n; v = 12 + bs; (pspace_no_overlap' ptr sz and valid_pspace') s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> dev; v = 12 + bs; 0 < n\<rbrakk> \<Longrightarrow> projectKO_opt KOUserData = Some UserData proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pspace_no_overlap' ptr sz and valid_pspace' and K (v = 12 + bs)\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) bs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>p<2 ^ (v - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s\<rbrace>

goal:
No subgoals!