theory Retype_R

lemma createObjects'_typ_at:
  "\<lbrace>\<lambda>s. n \<noteq> 0 \<and>
        range_cover ptr sz (objBitsKO val + gbits) n \<and>
        typ_at' T p s \<and>
        pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s\<rbrace>
  createObjects' ptr n val gbits \<lbrace>\<lambda>r s. typ_at' T p s\<rbrace>" apply (rule hoare_grab_asm)+ apply (simp add: createObjects'_def lookupAround2_pspace_no
                    alignError_def unless_def split_def typ_at'_def) apply (subst new_cap_addrs_fold') apply (simp add: unat_1_0 unat_gt_0) apply (rule range_cover_not_zero_shift) apply simp+ apply (rule hoare_pre) apply (wp|simp cong: if_cong del: data_map_insert_def fun_upd_apply)+ apply (wpc|wp)+ apply (subst data_map_insert_def[symmetric]) apply clarsimp 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 (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. n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> typ_at' T p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r. typ_at' T p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at' T p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r. typ_at' T p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<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. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>_ ya ps y a. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << gbits
 2. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<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. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> word_of_nat n << gbits \<noteq> 0
 2. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<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. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> range_cover ?ptr4 ?sz4 ?bits4 n
 3. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> gbits \<le> ?bits4
 4. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<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. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<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. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<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. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (4 subgoals):
 1. \<And>ps. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>?B13 () 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. ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>?B12 y\<rbrace> gets ksPSpace \<lbrace>?B13 y\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail \<lbrace>?B12\<rbrace>
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<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> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<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> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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>x. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' 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))\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' 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))\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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> ko_wp_at' (\<lambda>ko. koTypeOf ko = T) 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' 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))\<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> koTypeOf val = T) \<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> koTypeOf val = T)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' 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)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> koTypeOf val = T) \<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> koTypeOf val = T)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' 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); 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> koTypeOf val = T) \<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> koTypeOf val = T)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T) \<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> koTypeOf val = T)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T) \<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> koTypeOf val = T)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 2. \<And>s a. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 2. \<And>s a. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 3. \<And>s a. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 3. \<And>s a. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 2. \<And>s a. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_distinct' 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); 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> koTypeOf val = T
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (?sbit109 s) (?n109 s)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> objBitsKO val \<le> ?sbit109 s
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> unat (word_of_nat n << gbits) = 2 ^ (?sbit109 s - objBitsKO val) * ?n109 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; 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; ko_wp_at' (\<lambda>ko. koTypeOf ko = T) p s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> gbits \<le> objBitsKO val + gbits proof (prove)
goal:
No subgoals!