theory Detype_R

lemma createNewCaps_pspace_no_overlap':
  "\<lbrace>\<lambda>s. range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (Suc n)) \<and>
        pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and>
        ptr \<noteq> 0\<rbrace>
   createNewCaps ty ptr (Suc n) us d
   \<lbrace>\<lambda>r s. pspace_no_overlap'
             (ptr + (1 + of_nat n << Types_H.getObjectSize ty us))
             (Types_H.getObjectSize ty us) s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: createNewCaps_def) apply (subgoal_tac "pspace_no_overlap' (ptr + (1 + of_nat n << (Types_H.getObjectSize ty us)))
                                         (Types_H.getObjectSize ty us) s") prefer 2 apply (rule pspace_no_overlap'_le[where sz = sz]) apply (rule pspace_no_overlap'_tail) apply simp+ apply (simp add:range_cover_def) apply (simp add:range_cover.sz(1)[where 'a=32, folded word_bits_def]) apply (rule_tac Q = "\<lambda>r. pspace_no_overlap' (ptr + (1 + of_nat n << Types_H.getObjectSize ty us))
                                              (Types_H.getObjectSize ty us) and
                           pspace_aligned' and pspace_distinct'" in hoare_strengthen_post) apply (case_tac ty) apply (simp_all add: apiGetObjectSize_def
                              ARM_H.toAPIType_def tcbBlockSizeBits_def
                              ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
                              cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
                              createObjects_def) apply (rule hoare_pre) apply wpc apply (clarsimp simp: apiGetObjectSize_def  curDomain_def
                          ARM_H.toAPIType_def tcbBlockSizeBits_def
                          ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
                          cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
                          createObjects_def Arch_createNewCaps_def
                    split: apiobject_type.splits
           | wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap[where sz = sz]
                createObjects'_psp_aligned[where sz = sz] createObjects'_psp_distinct[where sz = sz]
                copyGlobalMappings_pspace_aligned' mapM_x_wp_inv
                copyGlobalMappings_pspace_no_overlap'[where sz = sz] | assumption)+ apply (intro conjI range_cover_le[where n = "Suc n"] | simp)+ apply ((simp add:objBits_simps pageBits_def range_cover_def word_bits_def)+)[5] by ((clarsimp simp: apiGetObjectSize_def
                              ARM_H.toAPIType_def tcbBlockSizeBits_def
                              ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
                              cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
                              createObjects_def Arch_createNewCaps_def
                              pteBits_def pdeBits_def
                              unless_def
                        split: apiobject_type.splits
               | wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap
                    createObjects'_psp_aligned createObjects'_psp_distinct
                    copyGlobalMappings_pspace_aligned' mapM_x_wp_inv
                    copyGlobalMappings_pspace_no_overlap'
               | assumption | clarsimp simp: word_bits_def
               | intro conjI range_cover_le[where n = "Suc n"] range_cover.aligned)+)[6]

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0\<rbrace> createNewCaps ty ptr (Suc n) us d \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr (Suc n) us d \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) sz s
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> sz
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sz < word_bits
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (getObjectSize ty us) (Suc (Suc n))
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_aligned' s
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_distinct' s
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s
 5. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 6. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> sz
 7. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sz < word_bits
 8. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> getObjectSize ty us \<le> sz
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sz < word_bits
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 2. \<And>s rv sa. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; (pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct') sa\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) sa proof (prove)
goal (8 subgoals):
 1. \<And>s x1. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s rv sa. \<lbrakk>range_cover ptr sz (getObjectSize ty us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) s; (pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) and pspace_aligned' and pspace_distinct') sa\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << getObjectSize ty us)) (getObjectSize ty us) sa proof (prove)
goal (7 subgoals):
 1. \<And>s x1. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) and pspace_aligned' and pspace_distinct'\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz 12 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 and pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz 16 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 s; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 and pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz 20 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 s; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 and pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz 24 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 and pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (8 + pteBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) s; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) and pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. \<lbrakk>range_cover ptr sz (12 + pdeBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) s; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) and pspace_aligned' and pspace_distinct'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s x1. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 s x1\<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 (Suc n) - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 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 (Suc 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 (Suc 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 (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) and pspace_aligned' and pspace_distinct'\<rbrace>
 2. \<And>s x1 sa. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1; s = sa\<rbrakk> \<Longrightarrow> ?Q22 s x1 sa
 3. \<And>s. \<lbrakk>range_cover ptr sz 12 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 and pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz 16 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 s; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 and pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz 20 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 s; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 and pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz 24 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 and pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. \<lbrakk>range_cover ptr sz (8 + pteBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) s; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) and pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s. \<lbrakk>range_cover ptr sz (12 + pdeBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) s; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) and pspace_aligned' and pspace_distinct'\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>s x1. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R36 s x1\<rbrace> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc n) - 1] \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) and pspace_aligned' and pspace_distinct'\<rbrace>
 2. \<And>s x1. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 s x1\<rbrace> do addrs <- createObjects ptr (Suc n) (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) and pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<And>s x1. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 s x1\<rbrace> do addrs <- createObjects ptr (Suc n) (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) and pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s x1. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 s x1\<rbrace> do addrs <- createObjects ptr (Suc n) (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) and pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<And>s x1. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R32 s x1\<rbrace> do addrs <- createObjects ptr (Suc 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>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) and pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s x1 sa. \<lbrakk>range_cover ptr sz (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us))) (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> tcbBlockSizeBits | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> epSizeBits | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> ntfnSizeBits | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> cteSizeBits + us) s; ty = APIObjectType x1; s = sa\<rbrakk> \<Longrightarrow> (x1 = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> ?R36 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> ?R35 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> ?R34 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> ?R33 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R32 s x1 sa)
 7. \<And>s. \<lbrakk>range_cover ptr sz 12 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 and pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s. \<lbrakk>range_cover ptr sz 16 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 s; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 and pspace_aligned' and pspace_distinct'\<rbrace>
 9. \<And>s. \<lbrakk>range_cover ptr sz 20 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 s; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 and pspace_aligned' and pspace_distinct'\<rbrace>
 10. \<And>s. \<lbrakk>range_cover ptr sz 24 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 and pspace_aligned' and pspace_distinct'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 9)) 9 sa; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; range_cover ptr sz 9 (Suc (Suc n))\<rbrakk> \<Longrightarrow> range_cover ptr sz 9 (Suc n) \<and> is_aligned ptr 9 \<and> 9 < word_bits
 2. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 4)) 4 sa; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; range_cover ptr sz 4 (Suc (Suc n))\<rbrakk> \<Longrightarrow> range_cover ptr sz 4 (Suc n) \<and> is_aligned ptr 4 \<and> 4 < word_bits
 3. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 4)) 4 sa; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; range_cover ptr sz 4 (Suc (Suc n))\<rbrakk> \<Longrightarrow> range_cover ptr sz 4 (Suc n) \<and> is_aligned ptr 4 \<and> 4 < word_bits
 4. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 4 + us)) (4 + us) sa; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; range_cover ptr sz (4 + us) (Suc (Suc n))\<rbrakk> \<Longrightarrow> range_cover ptr sz (4 + us) (Suc n) \<and> is_aligned ptr (4 + us) \<and> 4 + us < word_bits
 5. \<And>s. \<lbrakk>range_cover ptr sz 12 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 and pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz 16 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 s; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 and pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. \<lbrakk>range_cover ptr sz 20 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 s; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 and pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s. \<lbrakk>range_cover ptr sz 24 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 and pspace_aligned' and pspace_distinct'\<rbrace>
 9. \<And>s. \<lbrakk>range_cover ptr sz (8 + pteBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) s; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) and pspace_aligned' and pspace_distinct'\<rbrace>
 10. \<And>s. \<lbrakk>range_cover ptr sz (12 + pdeBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) s; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) and pspace_aligned' and pspace_distinct'\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 9)) 9 sa; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; range_cover ptr sz 9 (Suc (Suc n))\<rbrakk> \<Longrightarrow> is_aligned ptr 9
 2. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 9)) 9 sa; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; range_cover ptr sz 9 (Suc (Suc n))\<rbrakk> \<Longrightarrow> 9 < word_bits
 3. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 4)) 4 sa; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; range_cover ptr sz 4 (Suc (Suc n))\<rbrakk> \<Longrightarrow> range_cover ptr sz 4 (Suc n) \<and> is_aligned ptr 4 \<and> 4 < word_bits
 4. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 4)) 4 sa; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; range_cover ptr sz 4 (Suc (Suc n))\<rbrakk> \<Longrightarrow> range_cover ptr sz 4 (Suc n) \<and> is_aligned ptr 4 \<and> 4 < word_bits
 5. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 4 + us)) (4 + us) sa; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; range_cover ptr sz (4 + us) (Suc (Suc n))\<rbrakk> \<Longrightarrow> range_cover ptr sz (4 + us) (Suc n) \<and> is_aligned ptr (4 + us) \<and> 4 + us < word_bits
 6. \<And>s. \<lbrakk>range_cover ptr sz 12 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 and pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. \<lbrakk>range_cover ptr sz 16 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 s; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 and pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s. \<lbrakk>range_cover ptr sz 20 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 s; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 and pspace_aligned' and pspace_distinct'\<rbrace>
 9. \<And>s. \<lbrakk>range_cover ptr sz 24 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 and pspace_aligned' and pspace_distinct'\<rbrace>
 10. \<And>s. \<lbrakk>range_cover ptr sz (8 + pteBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) s; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) and pspace_aligned' and pspace_distinct'\<rbrace>
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz 12 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 s; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12)) 12 and pspace_aligned' and pspace_distinct'\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz 16 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 s; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 16)) 16 and pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz 20 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 s; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 20)) 20 and pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. \<lbrakk>range_cover ptr sz 24 (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 s; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 24)) 24 and pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz (8 + pteBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) s; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 8 + pteBits)) (8 + pteBits) and pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (12 + pdeBits) (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) s; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr (Suc n) us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>r. pspace_no_overlap' (ptr + (1 + word_of_nat n << 12 + pdeBits)) (12 + pdeBits) and pspace_aligned' and pspace_distinct'\<rbrace>