theory Retype_R

lemma createNewCaps_cte_wp_at2:
  "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject
      \<and> n \<noteq> 0
      \<and> range_cover ptr sz (APIType_capBits ty objsz) n
      \<and> pspace_aligned' s \<and> pspace_distinct' s
      \<and> pspace_no_overlap' ptr sz s\<rbrace>
     createNewCaps ty ptr n objsz dev
   \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" including no_pre apply (simp add: createNewCaps_def createObjects_def ARM_H.toAPIType_def
           split del: if_split) apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def
                           split del: if_split cong: if_cong) apply (rename_tac apiobject_type) apply (case_tac apiobject_type; simp split del: if_split) apply (rule hoare_pre, wp, simp add:createObjects_def) apply ((wp createObjects_orig_cte_wp_at2'[where sz = sz]
                     mapM_x_wp' threadSet_cte_wp_at2')+
                   | assumption
                   | clarsimp simp: APIType_capBits_def
                                    projectKOs projectKO_opts_defs
                                    makeObject_tcb tcb_cte_cases_def
                                    pageBits_def archObjSize_def ptBits_def
                                    pdBits_def createObjects_def curDomain_def
                                    Let_def objBits_if_dev
                         split del: if_split
                   | simp add: objBits_simps pteBits_def pdeBits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> n \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createNewCaps ty ptr n objsz dev \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> n \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createNewCaps ty ptr n objsz dev \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits ty objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> case case ty of APIObjectType a \<Rightarrow> Just a | _ \<Rightarrow> Nothing of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr n objsz dev;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral objsz) objsz 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) objsz;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just objsz else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr objsz 0 0) addrs
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. ty = APIObjectType x1 \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType x1) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral objsz) objsz 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) objsz;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just objsz else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr objsz 0 0) addrs
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 2. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SmallPageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSmallPage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 3. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits LargePageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 4)) ` {x. x \<le> word_of_nat n - 1} then Some ARMLargePage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 4))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 4. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 8)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 8))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 5. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SuperSectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 12)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 12))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 6. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits PageTableObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> ((\<lambda>pt. arch_capability.PageTableCap pt None) \<circ> (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))))) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 7. ty = PageDirectoryObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits PageDirectoryObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- do y <- createObjects' ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings (map (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) [0 .e. word_of_nat n - 1]);
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) (map (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) [0 .e. word_of_nat n - 1]))
od;
return (map ((\<lambda>pt. arch_capability.PageDirectoryCap pt None) \<circ> (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>apiobject_type. ty = APIObjectType apiobject_type \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType apiobject_type) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ fromIntegral objsz) objsz 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) objsz;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just objsz else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr objsz 0 0) addrs
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 2. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SmallPageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSmallPage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 3. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits LargePageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 4)) ` {x. x \<le> word_of_nat n - 1} then Some ARMLargePage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 4))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 4. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 8)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 8))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 5. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SuperSectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 12)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 12))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 6. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits PageTableObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> ((\<lambda>pt. arch_capability.PageTableCap pt None) \<circ> (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))))) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 7. ty = PageDirectoryObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits PageDirectoryObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- do y <- createObjects' ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings (map (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) [0 .e. word_of_nat n - 1]);
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) (map (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) [0 .e. word_of_nat n - 1]))
od;
return (map ((\<lambda>pt. arch_capability.PageDirectoryCap pt None) \<circ> (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> return (map (\<lambda>n. capability.UntypedCap dev (ptr + n * 2 ^ objsz) objsz 0) [0 .e. word_of_nat n - 1]) \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz 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>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz 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>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) objsz;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just objsz else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr objsz 0 0) addrs)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 6. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SmallPageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSmallPage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 7. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits LargePageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 4)) ` {x. x \<le> word_of_nat n - 1} then Some ARMLargePage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 4))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 8. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 8)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 8))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 9. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SuperSectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 12)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 12))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 10. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits PageTableObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> ((\<lambda>pt. arch_capability.PageTableCap pt None) \<circ> (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))))) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz 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>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz 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>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<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. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) objsz;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just objsz else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr objsz 0 0) addrs)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 5. ty = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SmallPageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSmallPage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 6. ty = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits LargePageObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 4)) ` {x. x \<le> word_of_nat n - 1} then Some ARMLargePage else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMLargePage None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 4))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 7. ty = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 8)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 8))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 8. ty = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits SuperSectionObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- let Data = if dev then KOUserDataDevice else KOUserData in do y <- createObjects' ptr n Data 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> (\<lambda>x. ptr + (x << objBitsKO Data + 12)) ` {x. x \<le> word_of_nat n - 1} then Some ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map ((\<lambda>n. arch_capability.PageCap dev n VMReadWrite ARMSuperSection None) \<circ> (\<lambda>n. ptr + (n << objBitsKO Data + 12))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 9. ty = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits PageTableObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> ((\<lambda>pt. arch_capability.PageTableCap pt None) \<circ> (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject))))) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>
 10. ty = PageDirectoryObject \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> \<not> P' makeObject \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits PageDirectoryObject objsz) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do archCaps <- do y <- createObjects' ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings (map (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) [0 .e. word_of_nat n - 1]);
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) (map (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))) [0 .e. word_of_nat n - 1]))
od;
return (map ((\<lambda>pt. arch_capability.PageDirectoryCap pt None) \<circ> (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)))) [0 .e. word_of_nat n - 1])
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal:
No subgoals!