theory Retype_R

lemma createNewCaps_pspace_domain_valid[wp]:
  "\<lbrace>pspace_domain_valid and K ({ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}
            \<inter> kernel_data_refs = {}
        \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace>
    createNewCaps ty ptr n us dev
   \<lbrace>\<lambda>rv. pspace_domain_valid\<rbrace>" apply (simp add: createNewCaps_def) apply (rule hoare_pre) apply (wp createObjects_pspace_domain_valid[where sz=sz]
            mapM_x_wp'
        | wpc | simp add: Arch_createNewCaps_def curDomain_def Let_def
                     split del: if_split)+ apply (simp add: ARM_H.toAPIType_def
            split: object_type.splits) apply (auto simp: objBits_simps APIType_capBits_def pageBits_def
                    pteBits_def pdeBits_def
                    archObjSize_def ptBits_def pdBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_domain_valid and K ({ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>rv. pspace_domain_valid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_domain_valid and (\<lambda>y. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr n us 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 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. pspace_domain_valid\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr n us 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 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. pspace_domain_valid\<rbrace>
 2. \<And>s. (pspace_domain_valid and (\<lambda>y. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_domain_valid s \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr sz (objBitsKO (KONotification makeObject)) n) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n)) proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_domain_valid s \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<Longrightarrow> (\<forall>x1. ty = APIObjectType x1 \<longrightarrow> (x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n) \<and> (x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n) \<and> (x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr sz (objBitsKO (KONotification makeObject)) n) \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n)) \<and> (ty = SmallPageObject \<longrightarrow> (dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserDataDevice) n) \<and> (\<not> dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserData) n)) \<and> (ty = LargePageObject \<longrightarrow> (dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserDataDevice + 4) n) \<and> (\<not> dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserData + 4) n)) \<and> (ty = SectionObject \<longrightarrow> (dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserDataDevice + 8) n) \<and> (\<not> dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserData + 8) n)) \<and> (ty = SuperSectionObject \<longrightarrow> (dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserDataDevice + 12) n) \<and> (\<not> dev \<longrightarrow> range_cover ptr sz (objBitsKO KOUserData + 12) n)) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n) proof (prove)
goal:
No subgoals!