theory Retype_R

lemma createNewCaps_valid_pspace:
  assumes  not_0: "n \<noteq> 0"
  and      cover: "range_cover ptr sz (APIType_capBits ty us) n"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s
  \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + of_nat n * 2^(APIType_capBits ty us) - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace>
  createNewCaps ty ptr n us dev \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" unfolding createNewCaps_def Arch_createNewCaps_def using valid_obj_makeObject_rules apply (clarsimp simp: ARM_H.toAPIType_def
             split del: if_split cong: option.case_cong) apply (cases ty, simp_all split del: if_split) apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split) apply (rule hoare_pre, wp, clarsimp) apply (insert cover) apply (wp createObjects_valid_pspace_untyped' [OF _ not_0 , where ty="Inr ty" and sz = sz]
                     mapM_x_threadSet_valid_pspace mapM_x_wp'
                 | simp add: makeObjectKO_def archObjSize_def APIType_capBits_def
                             objBits_simps pageBits_def pdBits_def ptBits_def not_0
                             createObjects_def curDomain_def
                             pteBits_def pdeBits_def
                 | intro conjI impI
                 | simp add: power_add field_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- let pointerCast = PPtr \<circ> fromPPtr in 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 (injectKOS 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 (injectKOS 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 | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
using this:
valid_obj' KOUserData ?s
valid_obj' (KOTCB makeObject) ?s
valid_obj' (KOEndpoint makeObject) ?s
valid_obj' (KONotification makeObject) ?s
valid_obj' (KOCTE makeObject) ?s
valid_obj' (KOArch (KOPTE makeObject)) ?s
valid_obj' (KOArch (KOPDE makeObject)) ?s
valid_obj' (KOArch (KOASIDPool makeObject)) ?s
valid_obj' KOUserDataDevice ?s

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- let pointerCast = PPtr \<circ> fromPPtr in 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 (injectKOS 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 (injectKOS 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 | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> case case ty of APIObjectType x \<Rightarrow> Just x | _ \<Rightarrow> Nothing of None \<Rightarrow> 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 (injectKOS 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 (injectKOS 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 | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. ty = APIObjectType x1 \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType x1) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace>
 2. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SmallPageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 3. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits LargePageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 4. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 5. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SuperSectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 6. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageTableObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 7. ty = PageDirectoryObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageDirectoryObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>apiobject_type. ty = APIObjectType apiobject_type \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType apiobject_type) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace>
 2. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SmallPageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 3. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits LargePageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 4. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 5. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SuperSectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 6. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageTableObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 7. ty = PageDirectoryObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageDirectoryObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> return (map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1]) \<lbrace>\<lambda>r. valid_pspace'\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 6. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SmallPageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 7. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits LargePageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 8. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 9. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SuperSectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 10. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageTableObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 5. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SmallPageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 6. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits LargePageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 7. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 8. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SuperSectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 9. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageTableObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 10. ty = PageDirectoryObject \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageDirectoryObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>r. valid_pspace'\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 5. \<lbrakk>ty = SmallPageObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SmallPageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 6. \<lbrakk>ty = LargePageObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits LargePageObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 7. \<lbrakk>ty = SectionObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 8. \<lbrakk>ty = SuperSectionObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits SuperSectionObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 9. \<lbrakk>ty = PageTableObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageTableObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace>
 10. \<lbrakk>ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits PageDirectoryObject us - 1} s \<and> ksCurDomain s \<le> maxDomain\<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. valid_pspace'\<rbrace> proof (prove)
goal:
No subgoals!