theory Retype_R

lemma createObjects_orig_ko_wp_at2':
  "\<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0
      \<and> pspace_aligned' s \<and> pspace_distinct' s
      \<and> P (ko_wp_at' P' p s)
      \<and> (P' val \<longrightarrow> P True)
      \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace>" apply (simp add: createObjects'_def lookupAround2_pspace_no
                    alignError_def unless_def split_def del:fun_upd_apply) apply (rule hoare_grab_asm)+ apply (subst new_cap_addrs_fold') apply (drule range_cover_not_zero_shift[rotated]) apply (rule le_add2) apply (simp add:word_le_sub1 del:fun_upd_apply)+ apply (rule hoare_pre) apply (wp|simp cong: if_cong del: data_map_insert_def fun_upd_apply)+ apply (wpc|wp)+ apply (clarsimp simp:valid_pspace'_def linorder_not_less simp del:fun_upd_apply) apply (subgoal_tac " range_cover ptr sz (objBitsKO val) (unat (of_nat n << gbits))") apply (subst data_map_insert_def[symmetric])+ apply (subst retype_ko_wp_at',simp+)+ apply clarsimp apply (cases "P' val") apply simp apply clarsimp apply (frule(1) subsetD [OF new_cap_addrs_subset]) apply (drule(1) pspace_no_overlap_disjoint') apply (simp add:lookupAround2_None1) apply (intro conjI impI allI) apply (drule_tac x = p in spec) apply (erule impE) apply (erule(1) range_cover_new_cap_addrs_compare[rotated]) apply simp apply (fastforce simp: ko_wp_at'_def) apply (drule_tac x = p in orthD1) apply (clarsimp simp:ptr_add_def p_assoc_help) apply (simp add:dom_def) apply (fastforce simp:ko_wp_at'_def) apply (rule range_cover_rel) apply (simp)+ apply (subst mult.commute) apply (erule range_cover.unat_of_nat_n_shift) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + 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> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + 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> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>_ ya ps y a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << gbits
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + 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> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) ps))
od \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uu_ ya ps y a. 0 < n \<Longrightarrow> ?gbits8 uu_ ya ps y a \<le> objBitsKO val + gbits
 2. \<And>_ ya ps y a. 0 < n \<Longrightarrow> n \<noteq> 0
 3. \<And>uu_ ya ps y a. \<lbrakk>0 < n; word_of_nat n << ?gbits8 uu_ ya ps y a \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << gbits
 4. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + 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> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) ps))
od \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>_ ya ps y a. 0 < n \<Longrightarrow> n \<noteq> 0
 2. \<And>_ ya ps y a. \<lbrakk>0 < n; word_of_nat n << gbits \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << gbits
 3. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + 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> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) ps))
od \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + 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> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) ps))
od \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?Q13\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + 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> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) ps))
od \<lbrace>\<lambda>r s. P (ko_wp_at' P' p s)\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> ?Q13 s proof (prove)
goal (4 subgoals):
 1. \<And>ps. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?B18 () ps\<rbrace> case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr) \<lbrace>\<lambda>ya s. P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) ps\<rparr>))\<rbrace>
 2. \<And>y. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?B17 y\<rbrace> gets ksPSpace \<lbrace>?B18 y\<rbrace>
 3. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?Q13\<rbrace> when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail \<lbrace>?B17\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> ?Q13 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' val \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> (if ptr && mask (objBitsKO val + gbits) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>))) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits))\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits))\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (ko_wp_at' P' p (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits))\<rbrakk> \<Longrightarrow> p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (P' val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (P' val))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (P' val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (P' val))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); P' val\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (P' val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (P' val))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (P' val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (P' val))
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P (P' val)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P (P' val))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P False) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P False)
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P False) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P False)
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> P False) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P False)
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> ((\<forall>y\<le>ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0). ksPSpace s y = None) \<longrightarrow> P False) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> P False)
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<forall>y\<le>ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0). ksPSpace s y = None\<rbrakk> \<Longrightarrow> P False
 2. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> P False
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0) \<longrightarrow> ksPSpace s p = None\<rbrakk> \<Longrightarrow> P False
 2. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> P False
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> p \<le> ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = None\<rbrakk> \<Longrightarrow> P False
 3. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> P False
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = None\<rbrakk> \<Longrightarrow> P False
 3. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> P False
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = None\<rbrakk> \<Longrightarrow> P False
 2. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> P False
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> P False
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (3 subgoals):
 1. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> p \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr; p \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> P False
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr; p \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> P False
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (2 subgoals):
 1. \<And>s a. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_distinct' s; P (ko_wp_at' P' p s); pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0; range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)); p \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val); \<not> P' val; ptr \<le> p \<and> p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr; ksPSpace s p = None\<rbrakk> \<Longrightarrow> P False
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (unat (word_of_nat n << gbits)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (?sbit120 s) (?n120 s)
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> objBitsKO val \<le> ?sbit120 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> unat (word_of_nat n << gbits) = 2 ^ (?sbit120 s - objBitsKO val) * ?n120 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> unat (word_of_nat n << gbits) = 2 ^ gbits * n proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> unat (word_of_nat n << gbits) = n * 2 ^ gbits proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; pspace_aligned' s; pspace_distinct' s; P (ko_wp_at' P' p s); P' val \<longrightarrow> P True; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> gbits \<le> objBitsKO val + gbits proof (prove)
goal:
No subgoals!