theory Retype_R

lemma createObjects_ko_at_strg:
  fixes ptr :: word32
  assumes    cover: "range_cover ptr sz ((objBitsKO ko) + gbits) n"
  assumes    not_0: "n\<noteq> 0"
  assumes       pi: "projectKO_opt ko  = Some val"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
             createObjects ptr n ko gbits
         \<lbrace>\<lambda>r s. \<forall>x \<in> set r. \<forall>offs < 2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace>" proof - have shiftr_not_zero:" 1 \<le> ((of_nat n)::word32) << gbits" using range_cover_not_zero_shift[OF not_0 cover,where gbits = gbits] apply - apply (simp add:word_le_sub1) done note unat_of_nat_shiftl = range_cover.unat_of_nat_n_shift[OF cover,where gbits = gbits,simplified] note word_of_nat_eq_0_iff[simp del] have in_new:"\<And>idx offs. \<lbrakk>idx \<le> of_nat n - 1;offs<2 ^ gbits\<rbrakk>
    \<Longrightarrow> ptr + (idx << objBitsKO ko + gbits) + (offs << objBitsKO ko)
        \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko)" apply (insert range_cover_not_zero[OF not_0 cover] not_0) apply (clarsimp simp:new_cap_addrs_def image_def) apply (rule_tac x ="unat (2 ^ gbits * idx + offs)" in bexI) apply (subst add.commute) apply (simp add:shiftl_shiftl[symmetric]) apply (simp add:shiftl_t2n distrib_left[symmetric]) apply simp apply (rule unat_less_helper) apply (rule less_le_trans) apply (erule word_plus_strict_mono_right) apply (subst distrib_left[where c = "1 :: 32 word",symmetric,simplified]) apply (subst mult.commute[where a = "2^gbits"])+ apply (insert cover) apply (rule word_mult_le_iff[THEN iffD2]) apply (simp add:p2_gt_0) apply (clarsimp simp:range_cover_def word_bits_def) apply (drule range_cover_rel[where sbit' = "objBitsKO ko "]) apply simp apply simp apply (rule less_le_trans) apply (rule range_cover.range_cover_le_n_less) apply simp apply (subst unat_power_lower) using cover apply (clarsimp simp:range_cover_def) apply (simp add:field_simps) apply (rule unat_le_helper) apply (erule order_trans[OF _ word_sub_1_le]) apply (simp add:range_cover_not_zero[OF not_0 cover]) apply (simp add:word_bits_def) apply (drule range_cover_rel[where sbit' = "objBitsKO ko "]) apply simp apply simp apply (erule less_le_trans[OF range_cover.range_cover_le_n_less(1)]) apply (subst unat_power_lower) using cover apply (clarsimp simp:range_cover_def) apply (simp add:field_simps) apply (rule unat_le_helper[OF inc_le]) apply (simp add:word_leq_minus_one_le) apply (simp add:word_bits_def) apply (rule no_plus_overflow_neg) apply (rule less_le_trans[where y = "of_nat n"]) apply unat_arith using range_cover.range_cover_n_less[OF cover] apply (simp add:word_bits_def) apply (subst distrib_left[where c = "1 :: 32 word",symmetric,simplified]) apply (subst mult.commute) apply simp apply (rule word_mult_le_iff[THEN iffD2]) apply (simp add:p2_gt_0) apply (simp add:range_cover_def word_bits_def) apply (drule range_cover_rel[where sbit' = "objBitsKO ko "]) apply simp apply simp apply (rule less_le_trans) apply (rule range_cover.range_cover_le_n_less) apply simp apply (subst unat_power_lower) using cover apply (clarsimp simp:range_cover_def) apply (simp add:field_simps) apply (rule unat_le_helper) apply unat_arith apply (simp add:word_bits_def) apply (drule range_cover_rel[where sbit' = "objBitsKO ko "]) apply simp apply simp apply (rule less_le_trans) apply (erule range_cover.range_cover_le_n_less) apply (simp add:range_cover.unat_of_nat_n[OF cover]) apply (simp add: unat_le_helper) apply (simp add:word_bits_def) apply unat_arith done show ?thesis apply (simp add: split_def createObjects_def lookupAround2_pspace_no
                   alignError_def unless_def createObjects'_def) apply (rule hoare_pre) apply (wp|simp add:data_map_insert_def[symmetric]
     cong: if_cong del: fun_upd_apply data_map_insert_def)+ apply (wpc|wp|clarsimp simp del:fun_upd_apply)+ apply (subst new_cap_addrs_fold'[OF shiftr_not_zero])+ apply (subst data_map_insert_def[symmetric])+ apply (subst retype_obj_at_disj') apply (simp add:valid_pspace'_def unat_of_nat_shiftl)+ apply (rule range_cover_rel[OF cover]) apply simp+ apply (subst retype_obj_at_disj') apply (simp add:valid_pspace'_def unat_of_nat_shiftl)+ apply (rule range_cover_rel[OF cover]) apply simp+ using range_cover.unat_of_nat_n_shift[OF cover,where gbits = gbits,simplified] pi apply (simp add: in_new) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. 1 \<le> word_of_nat n << gbits proof (prove)
using this:
gbits \<le> objBitsKO ko + gbits \<Longrightarrow> word_of_nat n << gbits \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> word_of_nat n << gbits proof (prove)
goal (1 subgoal):
 1. (gbits \<le> objBitsKO ko + gbits \<Longrightarrow> word_of_nat n << gbits \<noteq> 0) \<Longrightarrow> 1 \<le> word_of_nat n << gbits proof (prove)
goal:
No subgoals! proof (state)
this:
1 \<le> word_of_nat n << gbits

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (state)
this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (state)
this:
(word_of_nat ?n = 0) = (2 ^ LENGTH(?'a) dvd ?n)

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits\<rbrakk> \<Longrightarrow> ptr + (idx << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko) proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (idx << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko) proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<n * 2 ^ gbits}. (idx << objBitsKO ko + gbits) + (offs << objBitsKO ko) = word_of_nat x << objBitsKO ko proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> (idx << objBitsKO ko + gbits) + (offs << objBitsKO ko) = word_of_nat (unat (2 ^ gbits * idx + offs)) << objBitsKO ko
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (2 ^ gbits * idx + offs) \<in> {0..<n * 2 ^ gbits} proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> (idx << gbits + objBitsKO ko) + (offs << objBitsKO ko) = word_of_nat (unat (2 ^ gbits * idx + offs)) << objBitsKO ko
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (2 ^ gbits * idx + offs) \<in> {0..<n * 2 ^ gbits} proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> (idx << gbits << objBitsKO ko) + (offs << objBitsKO ko) = 2 ^ gbits * idx + offs << objBitsKO ko
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (2 ^ gbits * idx + offs) \<in> {0..<n * 2 ^ gbits} proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (2 ^ gbits * idx + offs) \<in> {0..<n * 2 ^ gbits} proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (2 ^ gbits * idx + offs) < n * 2 ^ gbits proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + offs < word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + offs < ?y18 idx offs
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?y18 idx offs \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx \<le> 2 ^ gbits * idx + 2 ^ gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx \<le> 2 ^ gbits * (idx + 1)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> idx * 2 ^ gbits \<le> (idx + 1) * 2 ^ gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx * 2 ^ gbits \<le> (idx + 1) * 2 ^ gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 0 < 2 ^ gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> gbits < 32
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (6 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko + gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m40 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m40 idx offs)\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 6. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m40 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m40 idx offs)\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) < ?y45 idx offs
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> ?y45 idx offs \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (6 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> range_cover (?ptr48 idx offs) (?sz48 idx offs) (?sbit48 idx offs) (?n48 idx offs)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) \<le> ?n48 idx offs
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(?'a48) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 6. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat idx * unat (2 ^ gbits) \<le> 2 ^ gbits * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (6 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> gbits < LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat idx * 2 ^ gbits \<le> 2 ^ gbits * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 6. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
using this:
range_cover ptr sz (objBitsKO ko + gbits) n

goal (6 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> gbits < LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat idx * 2 ^ gbits \<le> 2 ^ gbits * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 6. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat idx * 2 ^ gbits \<le> 2 ^ gbits * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)\<rbrakk> \<Longrightarrow> unat idx \<le> n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)\<rbrakk> \<Longrightarrow> idx \<le> word_of_nat n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx. \<lbrakk>word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko + gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m61 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m61 idx offs)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m61 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m61 idx offs)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) \<le> 2 ^ gbits * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> gbits < LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (idx + 1) * 2 ^ gbits \<le> 2 ^ gbits * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
using this:
range_cover ptr sz (objBitsKO ko + gbits) n

goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> gbits < LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (idx + 1) * 2 ^ gbits \<le> 2 ^ gbits * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (idx + 1) * 2 ^ gbits \<le> 2 ^ gbits * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (idx + 1) \<le> n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (4 subgoals):
 1. \<And>idx. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> idx < word_of_nat n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx \<le> idx + 1
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx < - 1
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx < word_of_nat n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> word_of_nat n \<le> - 1
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> word_of_nat n \<le> - 1
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
using this:
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - (objBitsKO ko + gbits))

goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> word_of_nat n \<le> - 1
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * idx + 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 2 ^ gbits * (idx + 1) \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> (idx + 1) * 2 ^ gbits \<le> word_of_nat (n * 2 ^ gbits) proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> (idx + 1) * 2 ^ gbits \<le> word_of_nat n * 2 ^ gbits proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> 0 < 2 ^ gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> gbits < 32
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko + gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m160 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m160 idx offs)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m160 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m160 idx offs)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) < ?y165 idx offs
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> ?y165 idx offs \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> range_cover (?ptr168 idx offs) (?sz168 idx offs) (?sbit168 idx offs) (?n168 idx offs)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) \<le> ?n168 idx offs
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(?'a168) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * unat (2 ^ gbits) \<le> 2 ^ gbits * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> gbits < LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * 2 ^ gbits \<le> 2 ^ gbits * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
using this:
range_cover ptr sz (objBitsKO ko + gbits) n

goal (5 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> gbits < LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * 2 ^ gbits \<le> 2 ^ gbits * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 5. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (idx + 1) * 2 ^ gbits \<le> 2 ^ gbits * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)\<rbrakk> \<Longrightarrow> unat (idx + 1) \<le> n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (4 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko + gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m543 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m543 idx offs)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 4. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> ?m543 idx offs = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (?m543 idx offs)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) < ?y548 idx offs
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> ?y548 idx offs \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (word_of_nat n) * unat (2 ^ gbits) \<le> 2 ^ gbits * n
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (3 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n\<rbrakk> \<Longrightarrow> unat (2 ^ gbits) \<le> 2 ^ gbits
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 3. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (2 subgoals):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko) (2 ^ gbits * n)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(32) \<le> 2 ^ LENGTH(32)
 2. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal (1 subgoal):
 1. \<And>idx offs. \<lbrakk>idx \<le> word_of_nat n - 1; offs < 2 ^ gbits; word_of_nat n \<noteq> 0; 0 < n; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> idx + 1 \<le> word_of_nat n proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?idx \<le> word_of_nat n - 1; ?offs < 2 ^ gbits\<rbrakk> \<Longrightarrow> ptr + (?idx << objBitsKO ko + gbits) + (?offs << objBitsKO ko) \<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko)

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> do y <- do y <- when (ptr && mask (objBitsKO ko + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od;
return (map (\<lambda>n. ptr + (n << objBitsKO ko + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do y <- do y <- when (ptr && mask (objBitsKO ko + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od;
return (map (\<lambda>n. ptr + (n << objBitsKO ko + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace>
 2. \<And>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>ps. \<lbrace>?B11 () ps\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>ya s. \<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << gbits) - 1]) ps\<rparr>)\<rbrace>
 2. \<And>y. \<lbrace>?B10 y\<rbrace> gets ksPSpace \<lbrace>?B11 y\<rbrace>
 3. \<lbrace>?Q4\<rbrace> when (ptr && mask (objBitsKO ko + gbits) \<noteq> 0) fail \<lbrace>?B10\<rbrace>
 4. \<And>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr a. a(addr \<mapsto> ko)) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr a. a(addr \<mapsto> ko)) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr a. a(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr a. a(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) proof (prove)
goal (5 subgoals):
 1. \<And>s offs x. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>s offs x. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> pspace_distinct' s
 3. \<And>s offs x. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz70 s) s
 4. \<And>s offs x. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr (?sz70 s) (objBitsKO ko) (unat (word_of_nat n << gbits))
 5. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> (\<exists>koa. projectKO_opt ko = Some koa \<and> koa = val))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)
 2. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> (\<exists>koa. projectKO_opt ko = Some koa \<and> koa = val))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko + gbits
 2. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> n * 2 ^ gbits = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 3. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> (\<exists>koa. projectKO_opt ko = Some koa \<and> koa = val))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) (ksPSpace s)\<rparr>))) proof (prove)
goal (5 subgoals):
 1. \<And>s offs x a. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>s offs x a. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> pspace_distinct' s
 3. \<And>s offs x a. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz74 s) s
 4. \<And>s offs x a. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr (?sz74 s) (objBitsKO ko) (unat (word_of_nat n << gbits))
 5. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> (\<exists>koa. projectKO_opt ko = Some koa \<and> koa = val))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO ko) (n * 2 ^ gbits)
 2. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> (\<exists>koa. projectKO_opt ko = Some koa \<and> koa = val))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko + gbits
 2. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> n * 2 ^ gbits = 2 ^ (objBitsKO ko + gbits - objBitsKO ko) * n
 3. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> (\<exists>koa. projectKO_opt ko = Some koa \<and> koa = val))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) proof (prove)
using this:
unat (word_of_nat n << gbits) = n * 2 ^ gbits
projectKO_opt ko = Some val

goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; ptr && mask (objBitsKO ko + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n - 1. \<forall>offs<2 ^ gbits. ko_at' val (ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko)) s \<or> ptr + (x << objBitsKO ko + gbits) + (offs << objBitsKO ko) \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr ko) \<and> projectKO_opt ko = Some val)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace>

goal:
No subgoals!