theory Retype_R

lemma createNewCaps_ko_wp_atQ':
  "\<lbrace>(\<lambda>s. P (ko_wp_at' P' p s)
       \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0
       \<and> pspace_aligned' s \<and> pspace_distinct' s
       \<and> pspace_no_overlap' ptr sz s)
       and K (\<forall>pde_x :: pde. P' (injectKO pde_x)
                   \<longrightarrow> (\<forall>pde_y :: pde. P' (injectKO pde_y)))
       and K (\<forall>d (tcb_x :: tcb). \<not>tcbQueued tcb_x \<and> tcbState tcb_x = Inactive
                   \<longrightarrow> P' (injectKO (tcb_x \<lparr> tcbDomain := d \<rparr>)) = P' (injectKO tcb_x))
       and K (\<forall>v. makeObjectKO d (Inr ty) = Some v
                 \<longrightarrow> P' v \<longrightarrow> P True)\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: createNewCaps_def ARM_H.toAPIType_def
             split del: if_split) apply (cases ty, simp_all add: Arch_createNewCaps_def
                      split del: if_split) apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] apply (rule hoare_pre, wp, simp) apply ((wp mapM_x_threadSet_createNewCaps_futz
                     mapM_x_wp'
                     createObjects_obj_at
                     createObjects_ko_wp_at2 createObjects_makeObject_not_tcbQueued
                     copyGlobalMappings_ko_wp_at[where v="\<forall>pde :: pde. P' (injectKO pde)"]
                   | simp add: makeObjectKO_def objBitsKO_def archObjSize_def APIType_capBits_def
                               objBits_def pageBits_def pdBits_def ptBits_def curDomain_def
                               pteBits_def pdeBits_def
                          split del: if_split
                   | split if_split_asm[where Q=d]
                   | intro conjI impI | fastforce)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (ko_wp_at' P' p s) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and K (\<forall>pde_x. P' (injectKOS pde_x) \<longrightarrow> (\<forall>pde_y. P' (injectKOS pde_y))) and K (\<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (injectKOS (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (injectKOS tcb_x)) and K (\<forall>v. makeObjectKO d (Inr ty) = Some v \<longrightarrow> P' v \<longrightarrow> P True)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. P (ko_wp_at' P' p s) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and K (\<forall>pde_x. P' (injectKOS pde_x) \<longrightarrow> (\<forall>pde_y. P' (injectKOS pde_y))) and K (\<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (injectKOS (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (injectKOS tcb_x)) and K (\<forall>v. makeObjectKO d (Inr ty) = Some v \<longrightarrow> P' v \<longrightarrow> P True)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr ty) = Some v \<longrightarrow> P' v \<longrightarrow> P True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case case ty of APIObjectType a \<Rightarrow> Just a | _ \<Rightarrow> Nothing of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr n us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (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>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s x1. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType x1) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType x1)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (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>rv s. P (ko_wp_at' P' p s)\<rbrace>
 2. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SmallPageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SmallPageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 3. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits LargePageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr LargePageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 4. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 5. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SuperSectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SuperSectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 6. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits PageTableObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr PageTableObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace>
 7. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr PageDirectoryObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType apiobject_type) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType apiobject_type)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType apiobject_type\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (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>rv s. P (ko_wp_at' P' p s)\<rbrace>
 2. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SmallPageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SmallPageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 3. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits LargePageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr LargePageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 4. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 5. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SuperSectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SuperSectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 6. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits PageTableObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr PageTableObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace>
 7. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr PageDirectoryObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> return (map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1]) \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 2. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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 (ko_wp_at' P' p s)\<rbrace>
 3. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.EndpointObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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 (ko_wp_at' P' p s)\<rbrace>
 4. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.NotificationObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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 (ko_wp_at' P' p s)\<rbrace>
 5. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace>
 6. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SmallPageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SmallPageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 7. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits LargePageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr LargePageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 8. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 9. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SuperSectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SuperSectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 10. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits PageTableObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr PageTableObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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 (ko_wp_at' P' p s)\<rbrace>
 2. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.EndpointObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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 (ko_wp_at' P' p s)\<rbrace>
 3. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.NotificationObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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 (ko_wp_at' P' p s)\<rbrace>
 4. \<And>s apiobject_type. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject)) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace>
 5. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SmallPageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SmallPageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 6. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits LargePageObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr LargePageObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 7. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 8. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits SuperSectionObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr SuperSectionObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d 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 d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>
 9. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits PageTableObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr PageTableObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace>
 10. \<And>s. \<lbrakk>P (ko_wp_at' P' p s); range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; (\<exists>pde_x. P' (KOArch (KOPDE pde_x))) \<longrightarrow> (\<forall>pde_y. P' (KOArch (KOPDE pde_y))); \<forall>d tcb_x. \<not> tcbQueued tcb_x \<and> tcbState tcb_x = Structures_H.thread_state.Inactive \<longrightarrow> P' (KOTCB (tcbDomain_update (\<lambda>_. d) tcb_x)) = P' (KOTCB tcb_x); \<forall>v. makeObjectKO d (Inr PageDirectoryObject) = Some v \<longrightarrow> P' v \<longrightarrow> P True; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) 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>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal:
No subgoals!