theory Untyped_R

lemma createNewCaps_idlethread[wp]:
  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> createNewCaps tp ptr sz us d \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>" apply (simp add: createNewCaps_def toAPIType_def
            split: ARM_H.object_type.split
                   apiobject_type.split) apply safe apply (wp mapM_x_wp' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> createNewCaps tp ptr sz us d \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>x1. (x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>)) \<and> (tp = SmallPageObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (tp = LargePageObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (tp = SectionObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (tp = SuperSectionObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (tp = PageTableObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) \<and> (tp = PageDirectoryObject \<longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>) proof (prove)
goal (10 subgoals):
 1. \<And>x1. tp = APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 2. \<And>x1. tp = APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 3. \<And>x1. tp = APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 4. \<And>x1. tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do addrs <- createObjects ptr sz (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Just us else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 5. tp = SmallPageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 6. tp = LargePageObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 7. tp = SectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 8. tp = SuperSectionObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 9. tp = PageTableObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 10. tp = PageDirectoryObject \<Longrightarrow> \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr sz us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace> proof (prove)
goal:
No subgoals!