theory Retype_R

lemma createNewCaps_pde_mappings'[wp]:
  "\<lbrace>\<lambda>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0
            \<and> valid_arch_state' s
            \<and> pspace_aligned' s \<and> pspace_distinct' s
            \<and> pspace_no_overlap' ptr sz s\<rbrace>
       createNewCaps ty ptr n us d
   \<lbrace>\<lambda>_. valid_pde_mappings'\<rbrace>" apply (simp add: createNewCaps_def Arch_createNewCaps_def Let_def
              split del: if_split cong: option.case_cong
                                        object_type.case_cong) apply (rule hoare_pre) apply (wp mapM_x_copyGlobalMappings_pde_mappings' | wpc
         | simp split del: if_split)+ apply (rule_tac P="range_cover ptr sz (APIType_capBits ty us) n \<and> n\<noteq> 0" in hoare_gen_asm) apply (rule hoare_strengthen_post) apply (rule createObjects_aligned, simp+) apply (simp add: objBits_simps pdBits_def pageBits_def archObjSize_def APIType_capBits_def
                         range_cover_def pdeBits_def) apply (rule range_cover.range_cover_n_less[where 'a=32, folded word_bits_def],fastforce+) apply (simp add: objBits_simps pdBits_def pageBits_def archObjSize_def APIType_capBits_def range_cover_def word_bits_def
                      pteBits_def pdeBits_def)+ apply (wp mapM_x_wp[OF _ subset_refl] | wpc | simp add: curDomain_def)+ apply (clarsimp simp: projectKOs) apply (simp add: objBits_simps pdBits_def pageBits_def archObjSize_def APIType_capBits_def) apply (case_tac ty; simp) apply (rename_tac apiobject_type) apply (case_tac apiobject_type) apply (auto simp: ARM_H.toAPIType_def objBits_simps ptBits_def pageBits_def pteBits_def pdeBits_def
                    makeObject_pde valid_arch_state'_def pdBits_def page_directory_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>_. valid_pde_mappings'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- case ty of APIObjectType apiObject \<Rightarrow> fail | SmallPageObject \<Rightarrow> 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 | LargePageObject \<Rightarrow> 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 | SectionObject \<Rightarrow> 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 | SuperSectionObject \<Rightarrow> 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 | PageTableObject \<Rightarrow> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (\<lambda>pt. arch_capability.PageTableCap pt None) addrs)
od | PageDirectoryObject \<Rightarrow> 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 | 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>_. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q12\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- case ty of APIObjectType apiObject \<Rightarrow> fail | SmallPageObject \<Rightarrow> 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 | LargePageObject \<Rightarrow> 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 | SectionObject \<Rightarrow> 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 | SuperSectionObject \<Rightarrow> 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 | PageTableObject \<Rightarrow> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (\<lambda>pt. arch_capability.PageTableCap pt None) addrs)
od | PageDirectoryObject \<Rightarrow> 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 | 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>_. valid_pde_mappings'\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?Q12 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'109\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. is_aligned x pdBits\<rbrace>
 2. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> case x2 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>_. valid_pde_mappings'\<rbrace>
 3. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ty = APIObjectType x \<longrightarrow> True) \<and> (ty = SmallPageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz64 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 0) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz73 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 4) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz82 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 8) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz91 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 12) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> (valid_pde_mappings' s \<and> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ?P'109 s)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R24 x s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'112\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. is_aligned x pdBits\<rbrace>
 2. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> case x2 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>_. valid_pde_mappings'\<rbrace>
 3. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ty = APIObjectType x \<longrightarrow> True) \<and> (ty = SmallPageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz64 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 0) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz73 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 4) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz82 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 8) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz91 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 12) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> (valid_pde_mappings' s \<and> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (?P'112 and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)) s)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R24 x s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'112\<rbrace> createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject) \<lbrace>?Q113\<rbrace>
 2. \<And>rv s. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; ?Q113 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x pdBits
 3. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> case x2 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>_. valid_pde_mappings'\<rbrace>
 4. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ty = APIObjectType x \<longrightarrow> True) \<and> (ty = SmallPageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz64 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 0) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz73 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 4) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz82 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 8) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz91 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 12) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> (valid_pde_mappings' s \<and> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (?P'112 and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)) s)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R24 x s) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits PageDirectoryObject us) n \<and> 0 < n\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))
 2. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 3. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 4. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject) < word_bits
 5. \<And>rv s. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; \<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x pdBits
 6. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> case x2 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>_. valid_pde_mappings'\<rbrace>
 7. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ty = APIObjectType x \<longrightarrow> True) \<and> (ty = SmallPageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz64 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 0) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz73 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 4) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz82 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 8) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz91 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 12) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> (valid_pde_mappings' s \<and> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ((\<lambda>_. True) and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)) s)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R24 x s) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 2. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject) < word_bits
 4. \<And>rv s. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; \<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x pdBits
 5. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> case x2 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>_. valid_pde_mappings'\<rbrace>
 6. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ty = APIObjectType x \<longrightarrow> True) \<and> (ty = SmallPageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz64 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 0) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz73 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 4) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz82 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 8) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz91 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 12) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> (valid_pde_mappings' s \<and> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ((\<lambda>_. True) and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)) s)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R24 x s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0\<rbrakk> \<Longrightarrow> objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject) < word_bits
 2. \<And>rv s. \<lbrakk>toAPIType PageDirectoryObject = None; ty = PageDirectoryObject; range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0; \<forall>x\<in>set rv. is_aligned x (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x pdBits
 3. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> case x2 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>_. valid_pde_mappings'\<rbrace>
 4. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ty = APIObjectType x \<longrightarrow> True) \<and> (ty = SmallPageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz64 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 0) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz73 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 4) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz82 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 8) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz91 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 12) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> (valid_pde_mappings' s \<and> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ((\<lambda>_. True) and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)) s)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R24 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> case x2 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>_. valid_pde_mappings'\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (\<forall>x. ty = APIObjectType x \<longrightarrow> True) \<and> (ty = SmallPageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz64 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 0) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz73 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 4) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz82 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 8) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz91 (objBitsKO (if d then KOUserDataDevice else KOUserData) + 12) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt (if d then KOUserDataDevice else KOUserData) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> valid_pde_mappings' s \<and> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> (valid_pde_mappings' s \<and> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ((\<lambda>_. True) and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)) s)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R24 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pde_mappings' s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> (d \<longrightarrow> (toAPIType ty = None \<longrightarrow> (ty = SmallPageObject \<longrightarrow> range_cover ptr ?sz64 (objBitsKO KOUserDataDevice) n \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt KOUserDataDevice = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr ?sz73 (objBitsKO KOUserDataDevice + 4) n \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt KOUserDataDevice = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr ?sz82 (objBitsKO KOUserDataDevice + 8) n \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt KOUserDataDevice = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr ?sz91 (objBitsKO KOUserDataDevice + 12) n \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt KOUserDataDevice = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> range_cover ptr sz (APIType_capBits PageDirectoryObject us) n)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) (objBitsKO (KOTCB makeObject)) n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s \<and> (\<forall>pde. projectKO_opt (KOTCB makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) (objBitsKO (KOEndpoint makeObject)) n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s \<and> (\<forall>pde. projectKO_opt (KOEndpoint makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) (objBitsKO (KONotification makeObject)) n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s \<and> (\<forall>pde. projectKO_opt (KONotification makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (objBitsKO (KOCTE makeObject) + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s \<and> (\<forall>pde. projectKO_opt (KOCTE makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)))) \<and> (\<not> d \<longrightarrow> (toAPIType ty = None \<longrightarrow> (ty = SmallPageObject \<longrightarrow> range_cover ptr ?sz64 (objBitsKO KOUserData) n \<and> pspace_no_overlap' ptr ?sz64 s \<and> (\<forall>pde. projectKO_opt KOUserData = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr ?sz73 (objBitsKO KOUserData + 4) n \<and> pspace_no_overlap' ptr ?sz73 s \<and> (\<forall>pde. projectKO_opt KOUserData = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr ?sz82 (objBitsKO KOUserData + 8) n \<and> pspace_no_overlap' ptr ?sz82 s \<and> (\<forall>pde. projectKO_opt KOUserData = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr ?sz91 (objBitsKO KOUserData + 12) n \<and> pspace_no_overlap' ptr ?sz91 s \<and> (\<forall>pde. projectKO_opt KOUserData = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz96 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPTE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz108 s \<and> (\<forall>pde. projectKO_opt (KOArch (KOPDE makeObject)) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> range_cover ptr sz (APIType_capBits PageDirectoryObject us) n)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) (objBitsKO (KOTCB makeObject)) n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s \<and> (\<forall>pde. projectKO_opt (KOTCB makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) (objBitsKO (KOEndpoint makeObject)) n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s \<and> (\<forall>pde. projectKO_opt (KOEndpoint makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) (objBitsKO (KONotification makeObject)) n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s \<and> (\<forall>pde. projectKO_opt (KONotification makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (objBitsKO (KOCTE makeObject) + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s \<and> (\<forall>pde. projectKO_opt (KOCTE makeObject) = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE))))
flex-flex pairs:
?sz201 (ds_id ArchTypes_H.apiobject_type.CapTableObject) \<equiv>\<^sup>? ?sz199 (ds_id ArchTypes_H.apiobject_type.CapTableObject) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> (d \<longrightarrow> (toAPIType ty = None \<longrightarrow> (ty = SmallPageObject \<longrightarrow> range_cover ptr ?sz64 (objBitsKO KOUserDataDevice) n \<and> pspace_no_overlap' ptr ?sz64 s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr ?sz73 (objBitsKO KOUserDataDevice + 4) n \<and> pspace_no_overlap' ptr ?sz73 s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr ?sz82 (objBitsKO KOUserDataDevice + 8) n \<and> pspace_no_overlap' ptr ?sz82 s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr ?sz91 (objBitsKO KOUserDataDevice + 12) n \<and> pspace_no_overlap' ptr ?sz91 s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz96 s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz108 s \<and> makeObject = ARM_H.InvalidPDE \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> range_cover ptr sz (APIType_capBits PageDirectoryObject us) n)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) (objBitsKO (KOTCB makeObject)) n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) (objBitsKO (KOEndpoint makeObject)) n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) (objBitsKO (KONotification makeObject)) n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (objBitsKO (KOCTE makeObject) + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))) \<and> (\<not> d \<longrightarrow> (toAPIType ty = None \<longrightarrow> (ty = SmallPageObject \<longrightarrow> range_cover ptr ?sz64 (objBitsKO KOUserData) n \<and> pspace_no_overlap' ptr ?sz64 s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr ?sz73 (objBitsKO KOUserData + 4) n \<and> pspace_no_overlap' ptr ?sz73 s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr ?sz82 (objBitsKO KOUserData + 8) n \<and> pspace_no_overlap' ptr ?sz82 s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr ?sz91 (objBitsKO KOUserData + 12) n \<and> pspace_no_overlap' ptr ?sz91 s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr ?sz96 (objBitsKO (KOArch (KOPTE makeObject)) + (ptBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz96 s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr ?sz108 (objBitsKO (KOArch (KOPDE makeObject)) + (pdBits - objBits makeObject)) n \<and> pspace_no_overlap' ptr ?sz108 s \<and> makeObject = ARM_H.InvalidPDE \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> range_cover ptr sz (APIType_capBits PageDirectoryObject us) n)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) (objBitsKO (KOTCB makeObject)) n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) (objBitsKO (KOEndpoint makeObject)) n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) (objBitsKO (KONotification makeObject)) n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (objBitsKO (KOCTE makeObject) + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)))
flex-flex pairs:
?sz201 (ds_id ArchTypes_H.apiobject_type.CapTableObject) \<equiv>\<^sup>? ?sz199 (ds_id ArchTypes_H.apiobject_type.CapTableObject) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case ty of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us | SmallPageObject \<Rightarrow> pageBitsForSize ARMSmallPage | LargePageObject \<Rightarrow> pageBitsForSize ARMLargePage | SectionObject \<Rightarrow> pageBitsForSize ARMSection | SuperSectionObject \<Rightarrow> pageBitsForSize ARMSuperSection | PageTableObject \<Rightarrow> 10 | PageDirectoryObject \<Rightarrow> 14) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> (toAPIType ty = None \<longrightarrow> (ty = SmallPageObject \<longrightarrow> range_cover ptr ?sz64 12 n \<and> pspace_no_overlap' ptr ?sz64 s) \<and> (ty = LargePageObject \<longrightarrow> range_cover ptr ?sz73 16 n \<and> pspace_no_overlap' ptr ?sz73 s) \<and> (ty = SectionObject \<longrightarrow> range_cover ptr ?sz82 20 n \<and> pspace_no_overlap' ptr ?sz82 s) \<and> (ty = SuperSectionObject \<longrightarrow> range_cover ptr ?sz91 24 n \<and> pspace_no_overlap' ptr ?sz91 s) \<and> (ty = PageTableObject \<longrightarrow> range_cover ptr ?sz96 (pteBits + (ptBits - pteBits)) n \<and> pspace_no_overlap' ptr ?sz96 s) \<and> (ty = PageDirectoryObject \<longrightarrow> range_cover ptr ?sz108 (pdeBits + 12) n \<and> pspace_no_overlap' ptr ?sz108 s \<and> makeObject = ARM_H.InvalidPDE \<and> is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits) \<and> range_cover ptr sz 14 n)) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
flex-flex pairs:
?sz201 (ds_id ArchTypes_H.apiobject_type.CapTableObject) \<equiv>\<^sup>? ?sz199 (ds_id ArchTypes_H.apiobject_type.CapTableObject) proof (prove)
goal (7 subgoals):
 1. \<And>s x1. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<forall>x. toAPIType (APIObjectType x1) = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)
 2. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 12 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> (toAPIType SmallPageObject = None \<longrightarrow> range_cover ptr ?sz64 12 n \<and> pspace_no_overlap' ptr ?sz64 s) \<and> (\<forall>x. toAPIType SmallPageObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 3. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 16 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = LargePageObject\<rbrakk> \<Longrightarrow> (toAPIType LargePageObject = None \<longrightarrow> range_cover ptr ?sz73 16 n \<and> pspace_no_overlap' ptr ?sz73 s) \<and> (\<forall>x. toAPIType LargePageObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 4. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 20 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SectionObject\<rbrakk> \<Longrightarrow> (toAPIType SectionObject = None \<longrightarrow> range_cover ptr ?sz82 20 n \<and> pspace_no_overlap' ptr ?sz82 s) \<and> (\<forall>x. toAPIType SectionObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 5. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 24 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> (toAPIType SuperSectionObject = None \<longrightarrow> range_cover ptr ?sz91 24 n \<and> pspace_no_overlap' ptr ?sz91 s) \<and> (\<forall>x. toAPIType SuperSectionObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 6. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 10 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = PageTableObject\<rbrakk> \<Longrightarrow> (toAPIType PageTableObject = None \<longrightarrow> range_cover ptr ?sz96 (pteBits + (ptBits - pteBits)) n \<and> pspace_no_overlap' ptr ?sz96 s) \<and> (\<forall>x. toAPIType PageTableObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 7. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 14 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> (toAPIType PageDirectoryObject = None \<longrightarrow> range_cover ptr ?sz108 (pdeBits + 12) n \<and> pspace_no_overlap' ptr ?sz108 s \<and> makeObject = ARM_H.InvalidPDE \<and> is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits)) \<and> (\<forall>x. toAPIType PageDirectoryObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
flex-flex pairs:
?sz201 (ds_id ArchTypes_H.apiobject_type.CapTableObject) \<equiv>\<^sup>? ?sz199 (ds_id ArchTypes_H.apiobject_type.CapTableObject) proof (prove)
goal (7 subgoals):
 1. \<And>s apiobject_type. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = APIObjectType apiobject_type\<rbrakk> \<Longrightarrow> \<forall>x. toAPIType (APIObjectType apiobject_type) = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)
 2. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 12 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> (toAPIType SmallPageObject = None \<longrightarrow> range_cover ptr ?sz64 12 n \<and> pspace_no_overlap' ptr ?sz64 s) \<and> (\<forall>x. toAPIType SmallPageObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 3. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 16 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = LargePageObject\<rbrakk> \<Longrightarrow> (toAPIType LargePageObject = None \<longrightarrow> range_cover ptr ?sz73 16 n \<and> pspace_no_overlap' ptr ?sz73 s) \<and> (\<forall>x. toAPIType LargePageObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 4. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 20 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SectionObject\<rbrakk> \<Longrightarrow> (toAPIType SectionObject = None \<longrightarrow> range_cover ptr ?sz82 20 n \<and> pspace_no_overlap' ptr ?sz82 s) \<and> (\<forall>x. toAPIType SectionObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 5. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 24 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> (toAPIType SuperSectionObject = None \<longrightarrow> range_cover ptr ?sz91 24 n \<and> pspace_no_overlap' ptr ?sz91 s) \<and> (\<forall>x. toAPIType SuperSectionObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 6. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 10 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = PageTableObject\<rbrakk> \<Longrightarrow> (toAPIType PageTableObject = None \<longrightarrow> range_cover ptr ?sz96 (pteBits + (ptBits - pteBits)) n \<and> pspace_no_overlap' ptr ?sz96 s) \<and> (\<forall>x. toAPIType PageTableObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 7. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 14 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> (toAPIType PageDirectoryObject = None \<longrightarrow> range_cover ptr ?sz108 (pdeBits + 12) n \<and> pspace_no_overlap' ptr ?sz108 s \<and> makeObject = ARM_H.InvalidPDE \<and> is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits)) \<and> (\<forall>x. toAPIType PageDirectoryObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
flex-flex pairs:
?sz201 (ds_id ArchTypes_H.apiobject_type.CapTableObject) \<equiv>\<^sup>? ?sz199 (ds_id ArchTypes_H.apiobject_type.CapTableObject) proof (prove)
goal (11 subgoals):
 1. \<And>s apiobject_type. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<forall>x. toAPIType (APIObjectType apiobject_type) = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)
 2. \<And>s apiobject_type. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<forall>x. toAPIType (APIObjectType apiobject_type) = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)
 3. \<And>s apiobject_type. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<forall>x. toAPIType (APIObjectType apiobject_type) = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)
 4. \<And>s apiobject_type. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<forall>x. toAPIType (APIObjectType apiobject_type) = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)
 5. \<And>s apiobject_type. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us) n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<forall>x. toAPIType (APIObjectType apiobject_type) = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s)
 6. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 12 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> (toAPIType SmallPageObject = None \<longrightarrow> range_cover ptr ?sz64 12 n \<and> pspace_no_overlap' ptr ?sz64 s) \<and> (\<forall>x. toAPIType SmallPageObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 7. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 16 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = LargePageObject\<rbrakk> \<Longrightarrow> (toAPIType LargePageObject = None \<longrightarrow> range_cover ptr ?sz73 16 n \<and> pspace_no_overlap' ptr ?sz73 s) \<and> (\<forall>x. toAPIType LargePageObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 8. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 20 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SectionObject\<rbrakk> \<Longrightarrow> (toAPIType SectionObject = None \<longrightarrow> range_cover ptr ?sz82 20 n \<and> pspace_no_overlap' ptr ?sz82 s) \<and> (\<forall>x. toAPIType SectionObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 9. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 24 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> (toAPIType SuperSectionObject = None \<longrightarrow> range_cover ptr ?sz91 24 n \<and> pspace_no_overlap' ptr ?sz91 s) \<and> (\<forall>x. toAPIType SuperSectionObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
 10. \<And>s. \<lbrakk>valid_pde_mappings' s; range_cover ptr sz 10 n; 0 < n; valid_arch_state' s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ty = PageTableObject\<rbrakk> \<Longrightarrow> (toAPIType PageTableObject = None \<longrightarrow> range_cover ptr ?sz96 (pteBits + (ptBits - pteBits)) n \<and> pspace_no_overlap' ptr ?sz96 s) \<and> (\<forall>x. toAPIType PageTableObject = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) tcbBlockSizeBits n \<and> pspace_no_overlap' ptr (?sz173 ArchTypes_H.apiobject_type.TCBObject) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) epSizeBits n \<and> pspace_no_overlap' ptr (?sz179 ArchTypes_H.apiobject_type.EndpointObject) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) ntfnSizeBits n \<and> pspace_no_overlap' ptr (?sz185 ArchTypes_H.apiobject_type.NotificationObject) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr (?sz201 ArchTypes_H.apiobject_type.CapTableObject) (cteSizeBits + us) n \<and> pspace_no_overlap' ptr (?sz199 ArchTypes_H.apiobject_type.CapTableObject) s))
A total of 11 subgoals...
flex-flex pairs:
?sz201 (ds_id ArchTypes_H.apiobject_type.CapTableObject) \<equiv>\<^sup>? ?sz199 (ds_id ArchTypes_H.apiobject_type.CapTableObject) proof (prove)
goal:
No subgoals!