theory Retype_R

lemma createNewCaps_valid_cap:
  fixes ptr :: word32
  assumes cover: "range_cover ptr sz (APIType_capBits ty us) n "
  assumes not_0: "n \<noteq> 0"
  assumes ct: "ty = APIObjectType ArchTypes_H.CapTableObject \<Longrightarrow> 0 < us"
              "ty = APIObjectType apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits"
  assumes ptr: " ptr \<noteq> 0"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace>
           createNewCaps ty ptr n us dev
         \<lbrace>\<lambda>r s. (\<forall>cap \<in> set r. s \<turnstile>' cap)\<rbrace>" proof - note blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex note if_split_def[split del] = if_splits show ?thesis proof(cases "Types_H.toAPIType ty") case None thus ?thesis using not_0 apply (clarsimp simp: createNewCaps_def Arch_createNewCaps_def) using cover apply (simp add: range_cover_def) using cover apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def
                     split: ARM_H.object_type.splits)

       \<comment> \<open>SmallPageObject\<close> apply wp apply (simp add: valid_cap'_def capAligned_def n_less_word_bits
                         ball_conj_distrib) apply (wp createObjects_aligned2 createObjects_nonzero[OF not_0 ,simplified]
                 cwo_ret[OF _ not_0]
         | simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+ apply (simp add:pageBits_def ptr word_bits_def)
      \<comment> \<open>LargePageObject\<close> apply wp apply (simp add: valid_cap'_def capAligned_def n_less_word_bits
                        ball_conj_distrib) apply (wp createObjects_aligned2 createObjects_nonzero[OF not_0 ,simplified]
                 cwo_ret[OF _ not_0]
         | simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+ apply (simp add:pageBits_def ptr word_bits_def)

     \<comment> \<open>SectionObject\<close> apply wp apply (simp add: valid_cap'_def capAligned_def n_less_word_bits
                       ball_conj_distrib) apply (wp createObjects_aligned2 createObjects_nonzero[OF not_0 ,simplified]
                cwo_ret[OF _ not_0]
       | simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+ apply (simp add:pageBits_def ptr word_bits_def)

    \<comment> \<open>SuperSectionObject\<close> apply wp apply (simp add: valid_cap'_def capAligned_def n_less_word_bits
                      ball_conj_distrib) apply (wp createObjects_aligned2 createObjects_nonzero[OF not_0 ,simplified]
               cwo_ret[OF _ not_0]
       | simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+ apply (simp add:pageBits_def ptr word_bits_def)

   \<comment> \<open>PageTableObject\<close> apply wp apply (simp add: valid_cap'_def capAligned_def n_less_word_bits) apply (simp only: imp_conv_disj page_table_at'_def
                       typ_at_to_obj_at_arches) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule createObjects_aligned [OF _ range_cover.range_cover_n_less(1)
           [where 'a=32, unfolded word_bits_len_of, OF cover] not_0]) apply (simp add:objBits_simps archObjSize_def ptBits_def pageBits_def
                       pdeBits_def pteBits_def)+ apply (simp add:range_cover_def word_bits_def) apply (rule createObjects_obj_at[where 'a =pte, OF _  not_0]) apply (simp add:objBits_simps archObjSize_def ptBits_def pageBits_def
                        pdeBits_def pteBits_def)+ apply (simp add: projectKOs projectKO_opt_pte) apply simp apply (clarsimp simp: objBits_simps archObjSize_def ptBits_def pageBits_def
                          pdeBits_def pteBits_def) apply clarsimp
  \<comment> \<open>PageDirectoryObject\<close> apply (wp hoare_vcg_const_Ball_lift) apply (wp mapM_x_wp' ) apply (simp add: valid_cap'_def capAligned_def n_less_word_bits) apply (simp only: imp_conv_disj page_directory_at'_def
                     typ_at_to_obj_at_arches) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule createObjects_aligned [OF _ range_cover.range_cover_n_less(1)
          [where 'a=32, unfolded word_bits_len_of, OF cover] not_0]) apply (simp add:objBits_simps archObjSize_def ptBits_def pageBits_def pdBits_def
                       pdeBits_def pteBits_def)+ apply (simp add:range_cover_def word_bits_def) apply (rule createObjects_obj_at [where 'a=pde, OF _  not_0]) apply (simp add:objBits_simps archObjSize_def ptBits_def pageBits_def pdBits_def
                      pdeBits_def pteBits_def) apply (simp add: projectKOs projectKO_opt_pde) apply simp apply (clarsimp simp: objBits_simps archObjSize_def pdBits_def pageBits_def
                         pdeBits_def pteBits_def) apply clarsimp done next case (Some a) thus ?thesis proof(cases a) case Untyped with Some cover ct show ?thesis apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) apply (simp_all add: ARM_H.toAPIType_def fromIntegral_def
                             toInteger_nat fromInteger_nat APIType_capBits_def
                      split: ARM_H.object_type.splits) apply wp apply (intro ballI) apply (clarsimp simp: image_def upto_enum_red' valid_cap'_def capAligned_def
                       split: capability.splits) apply (drule word_leq_minus_one_le[rotated]) apply (rule range_cover_not_zero[OF not_0 cover]) apply (intro conjI) apply (rule is_aligned_add_multI[OF _ le_refl refl]) apply (fastforce simp:range_cover_def word_bits_def)+ apply (clarsimp simp:valid_untyped'_def ko_wp_at'_def obj_range'_def) apply (drule(1) pspace_no_overlapD'[rotated]) apply (frule(1) range_cover_cell_subset) apply (erule disjE) apply (drule psubset_imp_subset) apply (drule(1) disjoint_subset2[rotated]) apply (drule(1) disjoint_subset) apply (drule(1) range_cover_subset_not_empty) apply clarsimp+ apply blast apply (drule(1) range_cover_no_0[OF ptr _ unat_less_helper]) apply simp done next case TCBObject with Some cover ct show ?thesis including no_pre apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) apply (simp_all add: ARM_H.toAPIType_def
                             fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def curDomain_def
                      split: ARM_H.object_type.splits) apply (wp mapM_x_wp' hoare_vcg_const_Ball_lift)+ apply (rule hoare_post_imp) prefer 2 apply (rule createObjects_obj_at [where 'a = "tcb",OF _ not_0]) using cover apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
                         split: ARM_H.object_type.splits) apply (simp add: projectKOs) apply (clarsimp simp: valid_cap'_def objBits_simps) apply (fastforce intro: capAligned_tcbI) done next case EndpointObject with Some cover ct show ?thesis including no_pre apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) apply (simp_all add: ARM_H.toAPIType_def
                             fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def
                      split: ARM_H.object_type.splits) apply wp apply (rule hoare_post_imp) prefer 2 apply (rule createObjects_obj_at [where 'a=endpoint, OF _ not_0]) using cover apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
                         split: ARM_H.object_type.splits) apply (simp add: projectKOs) apply (clarsimp simp: valid_cap'_def objBits_simps) apply (fastforce intro: capAligned_epI) done next case NotificationObject with Some cover ct show ?thesis including no_pre apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) apply (simp_all add: ARM_H.toAPIType_def
                             fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def
                      split: ARM_H.object_type.splits) apply wp apply (rule hoare_post_imp) prefer 2 apply (rule createObjects_obj_at [where 'a="notification", OF _ not_0]) using cover apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
                         split: ARM_H.object_type.splits) apply (simp add: projectKOs) apply (clarsimp simp: valid_cap'_def objBits_simps) apply (fastforce intro: capAligned_ntfnI) done next case CapTableObject with Some cover ct show ?thesis apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def) apply (simp_all add: ARM_H.toAPIType_def
                             fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def
                      split: ARM_H.object_type.splits) apply wp apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
                        split: ARM_H.object_type.split object_type.splits) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule createObjects_aligned [OF _ _ not_0 ]) apply ((clarsimp simp:objBits_simps range_cover_def range_cover.range_cover_n_less[where 'a=32, unfolded word_bits_len_of, OF cover])+)[3] apply (simp add: word_bits_def) apply (rule hoare_vcg_conj_lift) apply (rule createObjects_ret [OF range_cover.range_cover_n_less(1)[where 'a=32, unfolded word_bits_len_of, OF cover] not_0]) apply (rule createObjects_obj_at [where 'a=cte, OF _ not_0]) apply (simp add: objBits_simps APIType_capBits_def) apply (simp add: projectKOs) apply simp apply (clarsimp simp: valid_cap'_def capAligned_def objBits_simps
                        dest!: less_two_pow_divD) apply (thin_tac "\<forall>x\<in>S. is_aligned (p x) n" for S p n) apply (intro conjI) apply ((simp add:range_cover_def word_bits_def)+)[2] apply (clarsimp simp: power_sub) apply (drule bspec, simp) apply (drule_tac x = "addr && mask us" in spec) apply (drule mp) apply simp apply (rule and_mask_less') apply (simp add: range_cover_def word_bits_def) apply (clarsimp simp add: shiftl_t2n) apply simp done qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
untyped_range (cap.UntypedCap ?dev ?p ?n ?f) = {?p..?p + (1 << ?n) - 1}
untyped_range cap.NullCap = {}
untyped_range (cap.EndpointCap ?r ?badge ?rights) = {}
untyped_range (cap.NotificationCap ?r ?badge ?rights) = {}
untyped_range (cap.CNodeCap ?r ?bits ?guard) = {}
untyped_range (cap.ThreadCap ?r) = {}
untyped_range cap.DomainCap = {}
untyped_range (cap.ReplyCap ?r ?master ?rights) = {}
untyped_range cap.IRQControlCap = {}
untyped_range (cap.IRQHandlerCap ?irq) = {}
untyped_range (cap.Zombie ?r ?b ?n) = {}
untyped_range (cap.ArchObjectCap ?cap) = {}
usable_untyped_range (cap.UntypedCap ?uu ?p ?n ?f) = (if ?f < 2 ^ ?n then {?p + word_of_nat ?f..?p + 2 ^ ?n - 1} else {})
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))
?P (if ?Q then ?x else ?y) = (\<not> (?Q \<and> \<not> ?P ?x \<or> \<not> ?Q \<and> \<not> ?P ?y))

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (2 subgoals):
 1. toAPIType ty = None \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<And>a. toAPIType ty = Some a \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
toAPIType ty = None

goal (2 subgoals):
 1. toAPIType ty = None \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<And>a. toAPIType ty = Some a \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
toAPIType ty = None

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
toAPIType ty = None
n \<noteq> 0

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = None; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- case ty of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
range_cover ptr sz (APIType_capBits ty us) n

goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = None; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- case ty of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = None; 0 < n; is_aligned ptr (APIType_capBits ty us) \<and> sz < 32 \<and> APIType_capBits ty us \<le> sz \<and> n + unat (ptr && mask sz >> APIType_capBits ty us) \<le> 2 ^ (sz - APIType_capBits ty us)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- case ty of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
range_cover ptr sz (APIType_capBits ty us) n

goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = None; 0 < n; is_aligned ptr (APIType_capBits ty us) \<and> sz < 32 \<and> APIType_capBits ty us \<le> sz \<and> n + unat (ptr && mask sz >> APIType_capBits ty us) \<le> 2 ^ (sz - APIType_capBits ty us)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- case ty of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if dev then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap dev (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKO makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 12 n; ty = SmallPageObject; is_aligned ptr 12; sz < 32; 12 \<le> sz; n + unat (ptr && mask sz >> 12) \<le> 2 ^ (sz - 12)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 6. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 12 n; ty = SmallPageObject; is_aligned ptr 12; sz < 32; 12 \<le> sz; n + unat (ptr && mask sz >> 12) \<le> 2 ^ (sz - 12)\<rbrakk> \<Longrightarrow> \<lbrace>?Q71\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 0 \<lbrace>\<lambda>addrs s. \<forall>cap\<in>set (map capability.ArchObjectCap (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSmallPage None) addrs)). valid_cap' cap (s\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages s addr\<rparr>)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 12 n; ty = SmallPageObject; is_aligned ptr 12; sz < 32; 12 \<le> sz; n + unat (ptr && mask sz >> 12) \<le> 2 ^ (sz - 12); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q71 s
 3. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 6. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 7. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 12 n; ty = SmallPageObject; is_aligned ptr 12; sz < 32; 12 \<le> sz; n + unat (ptr && mask sz >> 12) \<le> 2 ^ (sz - 12)\<rbrakk> \<Longrightarrow> \<lbrace>?Q71\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 0 \<lbrace>\<lambda>addrs s. (\<forall>cap\<in>set addrs. is_aligned cap 12) \<and> (\<forall>x\<in>set addrs. x \<noteq> 0) \<and> (\<forall>x\<in>set addrs. \<forall>p<2 ^ (12 - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 12 n; ty = SmallPageObject; is_aligned ptr 12; sz < 32; 12 \<le> sz; n + unat (ptr && mask sz >> 12) \<le> 2 ^ (sz - 12); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q71 s
 3. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 6. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 7. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 12 n; ty = SmallPageObject; is_aligned ptr 12; sz < 32; 12 \<le> sz; n + unat (ptr && mask sz >> 12) \<le> 2 ^ (sz - 12); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> 12 < word_bits
 2. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 6. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16)\<rbrakk> \<Longrightarrow> \<lbrace>?Q107\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 4 \<lbrace>\<lambda>addrs s. \<forall>cap\<in>set (map capability.ArchObjectCap (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) addrs)). valid_cap' cap (s\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages s addr\<rparr>)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q107 s
 3. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 6. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16)\<rbrakk> \<Longrightarrow> \<lbrace>?Q107\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 4 \<lbrace>\<lambda>addrs s. (\<forall>cap\<in>set addrs. is_aligned cap 16) \<and> (\<forall>x\<in>set addrs. x \<noteq> 0) \<and> (\<forall>x\<in>set addrs. \<forall>p<2 ^ (16 - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q107 s
 3. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 6. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 16 n; ty = LargePageObject; is_aligned ptr 16; sz < 32; 16 \<le> sz; n + unat (ptr && mask sz >> 16) \<le> 2 ^ (sz - 16); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> 16 < word_bits
 2. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>?Q143\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8 \<lbrace>\<lambda>addrs s. \<forall>cap\<in>set (map capability.ArchObjectCap (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) addrs)). valid_cap' cap (s\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages s addr\<rparr>)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q143 s
 3. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20)\<rbrakk> \<Longrightarrow> \<lbrace>?Q143\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 8 \<lbrace>\<lambda>addrs s. (\<forall>cap\<in>set addrs. is_aligned cap 20) \<and> (\<forall>x\<in>set addrs. x \<noteq> 0) \<and> (\<forall>x\<in>set addrs. \<forall>p<2 ^ (20 - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q143 s
 3. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 20 n; ty = SectionObject; is_aligned ptr 20; sz < 32; 20 \<le> sz; n + unat (ptr && mask sz >> 20) \<le> 2 ^ (sz - 20); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> 20 < word_bits
 2. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>?Q179\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12 \<lbrace>\<lambda>addrs s. \<forall>cap\<in>set (map capability.ArchObjectCap (map (\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) addrs)). valid_cap' cap (s\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages s addr\<rparr>)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q179 s
 3. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24)\<rbrakk> \<Longrightarrow> \<lbrace>?Q179\<rbrace> createObjects ptr n (if dev then KOUserDataDevice else KOUserData) 12 \<lbrace>\<lambda>addrs s. (\<forall>cap\<in>set addrs. is_aligned cap 24) \<and> (\<forall>x\<in>set addrs. x \<noteq> 0) \<and> (\<forall>x\<in>set addrs. \<forall>p<2 ^ (24 - pageBits). typ_at' (if dev then UserDataDeviceT else UserDataT) (x + p * 2 ^ pageBits) s)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q179 s
 3. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 24 n; ty = SuperSectionObject; is_aligned ptr 24; sz < 32; 24 \<le> sz; n + unat (ptr && mask sz >> 24) \<le> 2 ^ (sz - 24); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> 24 < word_bits
 2. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?Q215\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>\<lambda>addrs a. \<forall>cap\<in>set (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs). valid_cap' cap a\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q215 s
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?Q215\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>\<lambda>addrs a. \<forall>cap\<in>set addrs. is_aligned cap 10 \<and> page_table_at' cap a\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q215 s
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?Q215\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>\<lambda>addrs a. \<forall>cap\<in>set addrs. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) a)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q215 s
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?Q215\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>?Q228\<rbrace>
 2. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); ?Q228 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q215 s
 4. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?P231\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>?Q231\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?P'231\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>?Q'231\<rbrace>
 3. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); ?Q231 rv s \<and> ?Q'231 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?P231 s \<and> ?P'231 s
 5. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))
 2. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject) < word_bits
 3. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?P'231\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>?Q'231\<rbrace>
 4. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))) \<and> ?Q'231 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 5. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'231 s
 6. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> 10 < word_bits
 2. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?P'231\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>?Q'231\<rbrace>
 3. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))) \<and> ?Q'231 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'231 s
 5. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<lbrace>?P'231\<rbrace> createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject) \<lbrace>?Q'231\<rbrace>
 2. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))) \<and> ?Q'231 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'231 s
 4. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> range_cover ptr ?sz239 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n
 2. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOArch (KOPTE makeObject)) = Some val
 3. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (ptBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPTE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr ?sz239 s \<and> valid_pspace' s
 5. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10)\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOArch (KOPTE makeObject)) = Some val
 2. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (ptBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPTE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s
 4. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (ptBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPTE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y. \<not> y < 2 ^ 8 \<or> obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (ptBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPTE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. is_aligned cap 10 \<and> is_aligned cap ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (cap + (y << 2)) s)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 10 n; ty = PageTableObject; is_aligned ptr 10; sz < 32; 10 \<le> sz; n + unat (ptr && mask sz >> 10) \<le> 2 ^ (sz - 10); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s
 2. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>addrs cap. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); cap \<in> set (map capability.ArchObjectCap (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs))\<rbrakk> \<Longrightarrow> \<lbrace>?P249 addrs cap\<rbrace> mapM_x copyGlobalMappings addrs \<lbrace>\<lambda>y. valid_cap' cap\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?Q243\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>\<lambda>addrs s. \<forall>x\<in>set (map capability.ArchObjectCap (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)). ?P249 addrs x s\<rbrace>
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q243 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?Q243\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>\<lambda>addrs s. \<forall>x\<in>set (map capability.ArchObjectCap (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)). valid_cap' x s\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q243 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?Q243\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>\<lambda>addrs s. \<forall>x\<in>set addrs. is_aligned x 14 \<and> page_directory_at' x s\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q243 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?Q243\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>\<lambda>addrs s. \<forall>x\<in>set addrs. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)\<rbrace>
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q243 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?Q243\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>?Q257\<rbrace>
 2. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); ?Q257 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q243 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?P260\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>?Q260\<rbrace>
 2. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?P'260\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>?Q'260\<rbrace>
 3. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); ?Q260 rv s \<and> ?Q'260 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?P260 s \<and> ?P'260 s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))
 2. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject) < word_bits
 3. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?P'260\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>?Q'260\<rbrace>
 4. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) \<and> ?Q'260 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 5. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'260 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> 14 < word_bits
 2. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?P'260\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>?Q'260\<rbrace>
 3. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) \<and> ?Q'260 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'260 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<lbrace>?P'260\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>?Q'260\<rbrace>
 2. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) \<and> ?Q'260 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'260 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> range_cover ptr ?sz268 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n
 2. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOArch (KOPDE makeObject)) = Some val
 3. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (pdBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 4. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr ?sz268 s \<and> valid_pspace' s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14)\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOArch (KOPDE makeObject)) = Some val
 2. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (pdBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 3. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (pdBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y. \<not> y < 2 ^ 12 \<or> obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ (pdBits - objBits makeObject). obj_at' (\<lambda>x. True) (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x 14 \<and> is_aligned x pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (x + (y << 2)) s)
 2. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < n; range_cover ptr sz 14 n; ty = PageDirectoryObject; is_aligned ptr 14; sz < 32; 14 \<le> sz; n + unat (ptr && mask sz >> 14) \<le> 2 ^ (sz - 14); pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal (1 subgoal):
 1. \<And>a. toAPIType ty = Some a \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a. toAPIType ty = Some a \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
toAPIType ty = Some a

goal (1 subgoal):
 1. \<And>a. toAPIType ty = Some a \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
toAPIType ty = Some a

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (5 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
a = ArchTypes_H.apiobject_type.Untyped

goal (5 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 5. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (chain)
picking this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.Untyped proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.Untyped

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped; range_cover ptr sz (APIType_capBits ty us) n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> return (map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1]) \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz us n; minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; x1 = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> return (map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1]) \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 s. \<lbrakk>range_cover ptr sz us n; minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; x1 = ArchTypes_H.apiobject_type.Untyped; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1]). valid_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<And>x1 s cap. \<lbrakk>range_cover ptr sz us n; minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; x1 = ArchTypes_H.apiobject_type.Untyped; pspace_no_overlap' ptr sz s \<and> valid_pspace' s; cap \<in> set (map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1])\<rbrakk> \<Longrightarrow> valid_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x \<le> word_of_nat n - 1\<rbrakk> \<Longrightarrow> is_aligned (ptr + x * 2 ^ us) us \<and> us < word_bits \<and> valid_untyped' dev (ptr + x * 2 ^ us) us 0 s \<and> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> is_aligned (ptr + x * 2 ^ us) us \<and> us < word_bits \<and> valid_untyped' dev (ptr + x * 2 ^ us) us 0 s \<and> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> is_aligned (ptr + x * 2 ^ us) us \<and> us < word_bits \<and> valid_untyped' dev (ptr + x * 2 ^ us) us 0 s \<and> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> is_aligned (ptr + x * 2 ^ us) us
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> us < word_bits
 3. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> valid_untyped' dev (ptr + x * 2 ^ us) us 0 s
 4. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> is_aligned ptr us
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> us < word_bits
 3. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> valid_untyped' dev (ptr + x * 2 ^ us) us 0 s
 4. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> valid_untyped' dev (ptr + x * 2 ^ us) us 0 s
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subset> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<or> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}; ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subset> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<or> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subset> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<or> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subset> {ptr'..ptr' + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr'..ptr' + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr'..ptr' + 2 ^ objBitsKO ko - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x ptr' ko. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; valid_pspace' s; x < word_of_nat n; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>range_cover ptr sz us n; a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>a = ArchTypes_H.apiobject_type.Untyped; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; minUntypedSizeBits \<le> us; us \<le> maxUntypedSizeBits; pspace_no_overlap' ptr sz s; valid_pspace' s; x < word_of_nat n; ptr + word_of_nat (unat x) * 2 ^ us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal (4 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (4 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
a = ArchTypes_H.apiobject_type.TCBObject

goal (4 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 4. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (chain)
picking this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.TCBObject proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.TCBObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.TCBObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.TCBObject; range_cover ptr sz (APIType_capBits ty us) n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- gets ksCurDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KOTCB makeObject) 0 \<lbrace>\<lambda>addrs s. \<forall>x\<in>set (map capability.ThreadCap addrs). valid_cap' x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject; ?Q41 x1 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map capability.ThreadCap rv). valid_cap' x s
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KOTCB makeObject) 0 \<lbrace>?Q41 x1\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KOTCB makeObject) 0 \<lbrace>?Q41 x1\<rbrace>
 2. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject; ?Q41 x1 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map capability.ThreadCap rv). valid_cap' x s proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO (KOTCB makeObject) + 0) n
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOTCB makeObject) = Some val
 3. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. tcb_at' (x + (offs << objBitsKO (KOTCB makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map capability.ThreadCap rv). valid_cap' x s proof (prove)
using this:
range_cover ptr sz (APIType_capBits ty us) n

goal (3 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO (KOTCB makeObject) + 0) n
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOTCB makeObject) = Some val
 3. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. tcb_at' (x + (offs << objBitsKO (KOTCB makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map capability.ThreadCap rv). valid_cap' x s proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOTCB makeObject) = Some val
 2. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. tcb_at' (x + (offs << objBitsKO (KOTCB makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map capability.ThreadCap rv). valid_cap' x s proof (prove)
goal (1 subgoal):
 1. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. tcb_at' (x + (offs << objBitsKO (KOTCB makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map capability.ThreadCap rv). valid_cap' x s proof (prove)
goal (1 subgoal):
 1. \<And>rv s x. \<lbrakk>range_cover ptr sz tcbBlockSizeBits n; a = ArchTypes_H.apiobject_type.TCBObject; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; \<forall>x\<in>set rv. tcb_at' x s; x \<in> set rv\<rbrakk> \<Longrightarrow> capAligned (capability.ThreadCap x) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal (3 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (3 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
a = ArchTypes_H.apiobject_type.EndpointObject

goal (3 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 3. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (chain)
picking this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.EndpointObject proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.EndpointObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.EndpointObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.EndpointObject; range_cover ptr sz (APIType_capBits ty us) n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KOEndpoint makeObject) 0 \<lbrace>\<lambda>addrs a. \<forall>cap\<in>set (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs). valid_cap' cap a\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject; ?Q34 x1 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) rv). valid_cap' cap s
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KOEndpoint makeObject) 0 \<lbrace>?Q34 x1\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KOEndpoint makeObject) 0 \<lbrace>?Q34 x1\<rbrace>
 2. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject; ?Q34 x1 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) rv). valid_cap' cap s proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO (KOEndpoint makeObject) + 0) n
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOEndpoint makeObject) = Some val
 3. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ep_at' (x + (offs << objBitsKO (KOEndpoint makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) rv). valid_cap' cap s proof (prove)
using this:
range_cover ptr sz (APIType_capBits ty us) n

goal (3 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO (KOEndpoint makeObject) + 0) n
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOEndpoint makeObject) = Some val
 3. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ep_at' (x + (offs << objBitsKO (KOEndpoint makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) rv). valid_cap' cap s proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOEndpoint makeObject) = Some val
 2. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ep_at' (x + (offs << objBitsKO (KOEndpoint makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) rv). valid_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; x1 = ArchTypes_H.apiobject_type.EndpointObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ep_at' (x + (offs << objBitsKO (KOEndpoint makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) rv). valid_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<And>rv s cap. \<lbrakk>range_cover ptr sz epSizeBits n; a = ArchTypes_H.apiobject_type.EndpointObject; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; \<forall>x\<in>set rv. ep_at' x s; cap \<in> set rv\<rbrakk> \<Longrightarrow> capAligned (capability.EndpointCap cap 0 True True True True) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal (2 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (2 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
a = ArchTypes_H.apiobject_type.NotificationObject

goal (2 subgoals):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>
 2. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (chain)
picking this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.NotificationObject proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.NotificationObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.NotificationObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.NotificationObject; range_cover ptr sz (APIType_capBits ty us) n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KONotification makeObject) 0 \<lbrace>\<lambda>addrs a. \<forall>cap\<in>set (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs). valid_cap' cap a\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject; ?Q34 x1 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.NotificationCap addr 0 True True) rv). valid_cap' cap s
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KONotification makeObject) 0 \<lbrace>?Q34 x1\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n (KONotification makeObject) 0 \<lbrace>?Q34 x1\<rbrace>
 2. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject; ?Q34 x1 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.NotificationCap addr 0 True True) rv). valid_cap' cap s proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO (KONotification makeObject) + 0) n
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KONotification makeObject) = Some val
 3. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ntfn_at' (x + (offs << objBitsKO (KONotification makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.NotificationCap addr 0 True True) rv). valid_cap' cap s proof (prove)
using this:
range_cover ptr sz (APIType_capBits ty us) n

goal (3 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO (KONotification makeObject) + 0) n
 2. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KONotification makeObject) = Some val
 3. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ntfn_at' (x + (offs << objBitsKO (KONotification makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.NotificationCap addr 0 True True) rv). valid_cap' cap s proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KONotification makeObject) = Some val
 2. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ntfn_at' (x + (offs << objBitsKO (KONotification makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.NotificationCap addr 0 True True) rv). valid_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<And>x1 rv s. \<lbrakk>range_cover ptr sz (objBits makeObject) n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; x1 = ArchTypes_H.apiobject_type.NotificationObject; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ntfn_at' (x + (offs << objBitsKO (KONotification makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set (map (\<lambda>addr. capability.NotificationCap addr 0 True True) rv). valid_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<And>rv s cap. \<lbrakk>range_cover ptr sz ntfnSizeBits n; a = ArchTypes_H.apiobject_type.NotificationObject; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; \<forall>x\<in>set rv. ntfn_at' x s; cap \<in> set rv\<rbrakk> \<Longrightarrow> capAligned (capability.NotificationCap cap 0 True True) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (state)
this:
a = ArchTypes_H.apiobject_type.CapTableObject

goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some a; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (chain)
picking this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.CapTableObject proof (prove)
using this:
toAPIType ty = Some a
range_cover ptr sz (APIType_capBits ty us) n
ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us
ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits
a = ArchTypes_H.apiobject_type.CapTableObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.CapTableObject; range_cover ptr sz (APIType_capBits ty us) n; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> 0 < us; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 x1\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>\<lambda>addrs s. \<forall>cap\<in>set (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs). valid_cap' cap (s\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes s addr\<rparr>)\<rbrace>
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q32 x1 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>\<lambda>addrs s. \<forall>cap\<in>set addrs. valid_cap' (capability.CNodeCap cap us 0 0) s\<rbrace>
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q32 x1 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q45\<rbrace>
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; ?Q45 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 3. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q32 x1 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P50 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q48\<rbrace>
 2. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q'48\<rbrace>
 3. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; ?Q48 rv s \<and> ?Q'48 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 4. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?P50 x1 s \<and> ?P'49 x1 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOCTE makeObject) + us)
 2. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> objBitsKO (KOCTE makeObject) + us < word_bits
 4. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q'48\<rbrace>
 5. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> ?Q'48 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 6. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'49 x1 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; is_aligned ptr (cteSizeBits + us); sz < 32; cteSizeBits + us \<le> sz; n + unat (ptr && mask sz >> cteSizeBits + us) \<le> 2 ^ (sz - (cteSizeBits + us))\<rbrakk> \<Longrightarrow> cteSizeBits + us < word_bits
 2. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q'48\<rbrace>
 3. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> ?Q'48 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 4. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'49 x1 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q'48\<rbrace>
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> ?Q'48 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 3. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P'49 x1 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P66 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q64\<rbrace>
 2. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'65 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q'64\<rbrace>
 3. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> ?Q64 rv s \<and> ?Q'64 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 4. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> ?P66 x1 s \<and> ?P'65 x1 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'65 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> createObjects ptr n (KOCTE makeObject) us \<lbrace>?Q'64\<rbrace>
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ objBitsKO (KOCTE makeObject) * 2 ^ us)) [0..<n] \<and> ?Q'64 rv s\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 3. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> ?P'65 x1 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> range_cover ptr (?sz74 ArchTypes_H.apiobject_type.CapTableObject) (objBitsKO (KOCTE makeObject) + us) n
 2. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOCTE makeObject) = Some val
 3. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ objBitsKO (KOCTE makeObject) * 2 ^ us)) [0..<n] \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ us. real_cte_at' (x + (offs << objBitsKO (KOCTE makeObject))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 4. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr (?sz74 x1) s \<and> valid_pspace' s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<exists>val. projectKO_opt (KOCTE makeObject) = Some val
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ objBitsKO (KOCTE makeObject) * 2 ^ us)) [0..<n] \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ us. real_cte_at' (x + (offs << objBitsKO (KOCTE makeObject))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 3. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>set rv. is_aligned x (objBitsKO (KOCTE makeObject) + us)) \<and> rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ objBitsKO (KOCTE makeObject) * 2 ^ us)) [0..<n] \<and> (\<forall>x\<in>set rv. \<forall>offs<2 ^ us. real_cte_at' (x + (offs << objBitsKO (KOCTE makeObject))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>set rv. valid_cap' (capability.CNodeCap cap us 0 0) s
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (\<forall>x\<in>{0..<n}. is_aligned (ptr_add ptr (x * 2 ^ objBitsKO (KOCTE makeObject) * 2 ^ us)) (objBitsKO (KOCTE makeObject) + us)) \<and> (\<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ objBitsKO (KOCTE makeObject) * 2 ^ us) + (offs << objBitsKO (KOCTE makeObject))) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>{0..<n}. valid_cap' (capability.CNodeCap (ptr_add ptr (cap * 2 ^ objBitsKO (KOCTE makeObject) * 2 ^ us)) us 0 0) s
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>x\<in>{0..<n}. is_aligned (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us)) (cteSizeBits + us); \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> cteSizeBits + us < word_bits \<and> us \<le> word_bits \<and> (\<forall>addr. real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s)
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> cteSizeBits + us < word_bits \<and> us \<le> word_bits \<and> (\<forall>addr. real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s)
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (4 subgoals):
 1. \<And>s cap. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> cteSizeBits + us < word_bits
 2. \<And>s cap. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> us \<le> word_bits
 3. \<And>s cap. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> \<forall>addr. real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 4. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> \<forall>addr. real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>x\<in>{0..<n}. \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (x * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; \<forall>offs<2 ^ us. real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + (offs << cteSizeBits)) s\<rbrakk> \<Longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; addr && mask us < 2 ^ us \<longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + (addr && mask us << cteSizeBits)) s\<rbrakk> \<Longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (3 subgoals):
 1. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}\<rbrakk> \<Longrightarrow> addr && mask us < 2 ^ us
 2. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + (addr && mask us << cteSizeBits)) s\<rbrakk> \<Longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 3. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (3 subgoals):
 1. \<And>cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}\<rbrakk> \<Longrightarrow> addr && mask us < 2 ^ us
 2. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + (addr && mask us << cteSizeBits)) s\<rbrakk> \<Longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 3. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (3 subgoals):
 1. \<And>cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}\<rbrakk> \<Longrightarrow> us < LENGTH(32)
 2. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + (addr && mask us << cteSizeBits)) s\<rbrakk> \<Longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 3. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (2 subgoals):
 1. \<And>s cap addr. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; cap \<in> {0..<n}; real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + (addr && mask us << cteSizeBits)) s\<rbrakk> \<Longrightarrow> real_cte_at' (ptr_add ptr (cap * 2 ^ cteSizeBits * 2 ^ us) + 2 ^ cteSizeBits * (addr && mask us)) s
 2. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal (1 subgoal):
 1. \<And>x1 s. \<lbrakk>range_cover ptr sz (objBits makeObject + us) n; 0 < us; a = ArchTypes_H.apiobject_type.CapTableObject; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> True \<and> True \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. valid_cap' cap s\<rbrace>

goal:
No subgoals!