theory Retype_R

lemma createNewCaps_vms:
  "\<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and
    K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n) and
    valid_machine_state'\<rbrace>
   createNewCaps ty ptr n us dev
   \<lbrace>\<lambda>archCaps. valid_machine_state'\<rbrace>" apply (clarsimp simp: valid_machine_state'_def pointerInDeviceData_def
                        Arch_createNewCaps_def createNewCaps_def pointerInUserData_def
                        typ_at'_def createObjects_def doMachineOp_return_foo
                  split del: if_split) apply (rule hoare_pre) apply (wpc
         | wp hoare_vcg_const_Ball_lift hoare_vcg_disj_lift
           hoare_vcg_all_lift
           doMachineOp_ko_wp_at' createObjects_orig_ko_wp_at2'[where sz = sz]
           hoare_vcg_all_lift
           doMachineOp_mapM_x_wp dmo_lift' mapM_x_wp' copyGlobalMappings_ko_wp_at threadSet_ko_wp_at2'
         | clarsimp simp: createObjects_def Arch_createNewCaps_def curDomain_def Let_def
                          pteBits_def pdeBits_def
               split del: if_split
         | assumption)+ apply (case_tac ty) apply (auto simp: APIType_capBits_def archObjSize_def objBits_simps pageBits_def ptBits_def
                     pdBits_def ARM_H.toAPIType_def object_type.splits pteBits_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n) and valid_machine_state'\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>archCaps. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n) and (\<lambda>s. \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0)\<rbrace> case toAPIType ty 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>archCaps s. \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> case toAPIType ty 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>archCaps s. \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace>
 2. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n) and (\<lambda>s. \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0))) proof (prove)
goal (7 subgoals):
 1. \<And>s x1. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)))
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)))
 3. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)))
 4. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)))
 5. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)))
 6. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)))
 7. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SmallPageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 4) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 8) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr sz (objBitsKO (if dev then KOUserDataDevice else KOUserData) + 12) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr sz (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s) \<or> ((\<exists>x. ty = APIObjectType x) \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SmallPageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = LargePageObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = SuperSectionObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageTableObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0) \<and> (ty = PageDirectoryObject \<longrightarrow> underlying_memory (ksMachineState s) x = 0))) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOTCB makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOEndpoint makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KONotification makeObject)) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (\<forall>x. range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<or> range_cover ptr sz (objBitsKO (KOCTE makeObject) + us) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) x = 0))) proof (prove)
goal:
No subgoals!