theory Orphanage

lemma createNewCaps_no_orphans:
  "\<lbrace> (\<lambda>s. no_orphans s
         \<and>  pspace_aligned' s \<and> pspace_distinct' s
         \<and>  pspace_no_overlap' ptr sz s
         \<and>  (tp = APIObjectType CapTableObject \<longrightarrow> us > 0))
         and K (range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n) \<rbrace>
   createNewCaps tp ptr n us d
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (clarsimp simp: createNewCaps_def toAPIType_def
    split del: if_split cong: option.case_cong) apply (cases tp, simp_all split del: if_split) apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all) apply (wp mapM_x_wp' threadSet_no_orphans
                   | clarsimp simp: is_active_thread_state_def makeObject_tcb
                                    projectKO_opt_tcb isRunning_def isRestart_def
                                    APIType_capBits_def Arch_createNewCaps_def
                                    objBits_if_dev
                          split del: if_split
                   | simp add: objBits_simps
                   | fastforce simp:pageBits_def pteBits_def archObjSize_def ptBits_def pdBits_def
                                    pdeBits_def objBits_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n)\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and (\<lambda>y. 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 <- Arch_createNewCaps tp ptr 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 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. no_orphans\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. tp = APIObjectType x1 \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and (\<lambda>y. range_cover ptr sz (APIType_capBits (APIObjectType x1) us) n \<and> 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. no_orphans\<rbrace>
 2. tp = SmallPageObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SmallPageObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. tp = LargePageObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits LargePageObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. tp = SectionObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SectionObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. tp = SuperSectionObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SuperSectionObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. tp = PageTableObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits PageTableObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. tp = PageDirectoryObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits PageDirectoryObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>apiobject_type. tp = APIObjectType apiobject_type \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (apiobject_type = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and (\<lambda>y. range_cover ptr sz (APIType_capBits (APIObjectType apiobject_type) us) n \<and> 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. no_orphans\<rbrace>
 2. tp = SmallPageObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SmallPageObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. tp = LargePageObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits LargePageObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. tp = SectionObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SectionObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. tp = SuperSectionObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SuperSectionObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. tp = PageTableObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits PageTableObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. tp = PageDirectoryObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits PageDirectoryObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type. \<lbrakk>tp = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) us) n \<and> 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. no_orphans\<rbrace>
 2. \<And>apiobject_type. \<lbrakk>tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.TCBObject) us) n \<and> 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. no_orphans\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) us) n \<and> 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. no_orphans\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) us) n \<and> 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. no_orphans\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> 0 < us) and (\<lambda>y. range_cover ptr sz (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) us) n \<and> 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 Some us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. tp = SmallPageObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SmallPageObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. tp = LargePageObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits LargePageObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 8. tp = SectionObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SectionObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 9. tp = SuperSectionObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits SuperSectionObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 10. tp = PageTableObject \<Longrightarrow> \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>y. range_cover ptr sz (APIType_capBits PageTableObject us) n \<and> 0 < n)\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
A total of 11 subgoals... proof (prove)
goal:
No subgoals!