theory Untyped_R

lemma createNewCaps_range_helper:
  "\<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace>
     createNewCaps tp ptr n us d
   \<lbrace>\<lambda>rv s. \<exists>capfn.
        rv = map capfn (map (\<lambda>p. ptr_add ptr (p * 2 ^ (APIType_capBits tp us)))
                               [0 ..< n])
          \<and> (\<forall>p. capClass (capfn p) = PhysicalClass
                 \<and> capUntypedPtr (capfn p) = p
                 \<and> capBits (capfn p) = (APIType_capBits tp us))\<rbrace>" apply (simp add: createNewCaps_def toAPIType_def Arch_createNewCaps_def
               split del: if_split cong: option.case_cong) apply (rule hoare_grab_asm)+ apply (frule range_cover.range_cover_n_less) apply (frule range_cover.unat_of_nat_n) apply (cases tp, simp_all split del: if_split) apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split) apply (rule hoare_pre, wp) apply (frule range_cover_not_zero[rotated -1],simp) apply (clarsimp simp: APIType_capBits_def objBits_simps archObjSize_def ptr_add_def o_def) apply (subst upto_enum_red') apply unat_arith apply (clarsimp simp: o_def fromIntegral_def toInteger_nat fromInteger_nat) apply fastforce apply (rule hoare_pre,wp createObjects_ret2) apply (clarsimp simp: APIType_capBits_def word_bits_def
                objBits_simps archObjSize_def ptr_add_def o_def) apply (fastforce simp: objBitsKO_def objBits_def) apply (rule hoare_pre,wp createObjects_ret2) apply (clarsimp simp: APIType_capBits_def word_bits_def
                                  objBits_simps archObjSize_def ptr_add_def o_def) apply (fastforce simp: objBitsKO_def  objBits_def) apply (rule hoare_pre,wp createObjects_ret2) apply (clarsimp simp:  APIType_capBits_def word_bits_def
              objBits_simps archObjSize_def ptr_add_def o_def) apply (fastforce simp: objBitsKO_def  objBits_def) apply (rule hoare_pre,wp createObjects_ret2) apply (clarsimp simp: APIType_capBits_def word_bits_def
             objBits_simps archObjSize_def ptr_add_def o_def) apply (fastforce simp: objBitsKO_def  objBits_def) apply (wp createObjects_ret2
          | clarsimp simp: APIType_capBits_def objBits_if_dev archObjSize_def
                        word_bits_def pdBits_def pageBits_def ptBits_def
                        pteBits_def pdeBits_def
                        split del: if_split
          | simp add: objBits_simps
          | (rule exI, fastforce))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map capfn (map (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits tp us)) [0..<n]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace> case case tp of APIObjectType a \<Rightarrow> Just a | _ \<Rightarrow> Nothing of None \<Rightarrow> do archCaps <- case tp of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits tp us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (APIType_capBits tp us) n \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> case case tp of APIObjectType a \<Rightarrow> Just a | _ \<Rightarrow> Nothing of None \<Rightarrow> do archCaps <- case tp of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits tp us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> case case tp of APIObjectType a \<Rightarrow> Just a | _ \<Rightarrow> Nothing of None \<Rightarrow> do archCaps <- case tp of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits tp us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; n < 2 ^ LENGTH(32); unat (word_of_nat n) = n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> case case tp of APIObjectType a \<Rightarrow> Just a | _ \<Rightarrow> Nothing of None \<Rightarrow> do archCaps <- case tp of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr n Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr n (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits tp us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType x1) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType x1) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType x1) us)\<rbrace>
 2. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType apiobject_type) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType apiobject_type\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType apiobject_type) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType apiobject_type) us)\<rbrace>
 2. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> return (map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1]) \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us)\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type s. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped; 0 < n\<rbrakk> \<Longrightarrow> \<exists>capfn. map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1] = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type s. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped; 0 < n; word_of_nat n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>capfn. map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1] = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; 0 < n; word_of_nat n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>capfn. map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ us) us 0) [0 .e. word_of_nat n - 1] = map (\<lambda>x. capfn (ptr + word_of_nat x * 2 ^ us)) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = us)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>capfn. \<lbrakk>range_cover ptr sz us n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; 0 < n; word_of_nat n \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n
 2. \<lbrakk>range_cover ptr sz us n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; 0 < n; word_of_nat n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>capfn. map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ us) us 0) (map word_of_nat [0..<unat (word_of_nat n)]) = map (\<lambda>x. capfn (ptr + word_of_nat x * 2 ^ us)) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = us)
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 6. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; 0 < n; word_of_nat n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>capfn. map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ us) us 0) (map word_of_nat [0..<unat (word_of_nat n)]) = map (\<lambda>x. capfn (ptr + word_of_nat x * 2 ^ us)) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = us)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; 0 < n; word_of_nat n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>capfn. (\<forall>x\<in>{0..<n}. capability.UntypedCap d (ptr + word_of_nat x * 2 ^ us) us 0 = capfn (ptr + word_of_nat x * 2 ^ us)) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = us)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>apiobject_type s. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>capfn. map capability.ThreadCap (map (\<lambda>p. ptr_add ptr (p * 2 ^ (objBitsKO (KOTCB makeObject) + 0))) [0..<n]) = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us)) and K (n < 2 ^ word_bits \<and> n \<noteq> 0)) s
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<lbrakk>range_cover ptr sz tcbBlockSizeBits n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; 0 < n\<rbrakk> \<Longrightarrow> \<exists>capfn. (\<forall>x\<in>{0..<n}. capability.ThreadCap (ptr + word_of_nat x * 2 ^ tcbBlockSizeBits) = capfn (ptr + word_of_nat x * 2 ^ tcbBlockSizeBits)) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = tcbBlockSizeBits)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 10. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>apiobject_type s. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>capfn. map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) (map (\<lambda>p. ptr_add ptr (p * 2 ^ (objBitsKO (KOEndpoint makeObject) + 0))) [0..<n]) = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us)) and K (n < 2 ^ word_bits \<and> n \<noteq> 0)) s
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<lbrakk>range_cover ptr sz epSizeBits n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; 0 < n\<rbrakk> \<Longrightarrow> \<exists>capfn. (\<forall>x\<in>{0..<n}. capability.EndpointCap (ptr + word_of_nat x * 2 ^ epSizeBits) 0 True True True True = capfn (ptr + word_of_nat x * 2 ^ epSizeBits)) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = epSizeBits)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 9. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>apiobject_type s. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>capfn. map (\<lambda>addr. capability.NotificationCap addr 0 True True) (map (\<lambda>p. ptr_add ptr (p * 2 ^ (objBitsKO (KONotification makeObject) + 0))) [0..<n]) = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us)) and K (n < 2 ^ word_bits \<and> n \<noteq> 0)) s
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<lbrakk>range_cover ptr sz ntfnSizeBits n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; 0 < n\<rbrakk> \<Longrightarrow> \<exists>capfn. (\<forall>x\<in>{0..<n}. capability.NotificationCap (ptr + word_of_nat x * 2 ^ ntfnSizeBits) 0 True True = capfn (ptr + word_of_nat x * 2 ^ ntfnSizeBits)) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = ntfnSizeBits)
 2. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 8. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>apiobject_type. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)\<rbrace>
 2. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>apiobject_type s. \<lbrakk>range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>capfn. map (\<lambda>addr. capability.CNodeCap addr us 0 0) (map (\<lambda>p. ptr_add ptr (p * 2 ^ (objBitsKO (KOCTE makeObject) + us))) [0..<n]) = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us)) and K (n < 2 ^ word_bits \<and> n \<noteq> 0)) s
 2. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrakk>range_cover ptr sz (cteSizeBits + us) n; n < 4294967296; unat (word_of_nat n) = n; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; 0 < n\<rbrakk> \<Longrightarrow> \<exists>capfn. (\<forall>x\<in>{0..<n}. capability.CNodeCap (ptr + word_of_nat x * 2 ^ (cteSizeBits + us)) us 0 0 = capfn (ptr + word_of_nat x * 2 ^ (cteSizeBits + us))) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = cteSizeBits + us)
 2. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 7. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits SmallPageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSmallPage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SmallPageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SmallPageObject us)\<rbrace>
 2. \<lbrakk>range_cover ptr sz (APIType_capBits LargePageObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMLargePage None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits LargePageObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits LargePageObject us)\<rbrace>
 3. \<lbrakk>range_cover ptr sz (APIType_capBits SectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SectionObject us)\<rbrace>
 4. \<lbrakk>range_cover ptr sz (APIType_capBits SuperSectionObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (if d then KOUserDataDevice else KOUserData) 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap d n VMReadWrite ARMSuperSection None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits SuperSectionObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits SuperSectionObject us)\<rbrace>
 5. \<lbrakk>range_cover ptr sz (APIType_capBits PageTableObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do addrs <- createObjects ptr n (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (map (capability.ArchObjectCap \<circ> (\<lambda>pt. arch_capability.PageTableCap pt None)) addrs)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageTableObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageTableObject us)\<rbrace>
 6. \<lbrakk>range_cover ptr sz (APIType_capBits PageDirectoryObject us) n; n < 4294967296; unat (word_of_nat n) = n; tp = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 0 < n\<rbrace> do archCaps <- do addrs <- createObjects ptr n (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
y <- do y <- mapM_x copyGlobalMappings addrs;
doMachineOp (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + word_of_nat (shiftL (Suc 0) pdBits) - 1) (addrFromPPtr x)) addrs)
od;
return (map (\<lambda>pt. arch_capability.PageDirectoryCap pt None) addrs)
od;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. \<exists>capfn. rv = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits PageDirectoryObject us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits PageDirectoryObject us)\<rbrace> proof (prove)
goal:
No subgoals!